shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249)

Commit

5 years ago

feat(category_theory/limits/shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249) Decompose `(pullback_cone.mk _ _ _).fst` into its first component (+symmetrical and dual versions)

Author

b-mehta

Parents

06256910

mathlib a40be987 - feat(category_theory/limits/shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249)

mathlib
a40be987 - feat(category_theory/limits/shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249)