mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ f.homMk' (g' ≫ g) = eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
this : l' = homMk m ⋯
⊢ l = m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ (mk f).hom) = mk (S.map g' ≫ (mk (S.map g ≫ f)).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ f) = mk f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y : C
S : C ⥤ D
f : S.obj Y ⟶ T
⊢ mkPrecomp f (𝟙 Y) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f) = mk (S.map g' ≫ S.map g ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
⊢ Epi (Hom.right k)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝¹ : T
f✝ g : Under X✝¹
φ : f✝ ⟶ g
X : T
F : T ⥤ D
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ (mk (F.map X✝.hom)).hom ≫ F.map (Hom.right f) = (mk (F.map Y✝.hom)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y Y' Y'' : C
S : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mkPrecomp f (g' ≫ g) = eqToHom ⋯ ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ f.right = f'.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ S.map g.hom ≫ f'.hom = f.hom ≫ (Functor.fromPUnit T).map (eqToIso ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : T ⥤ D
G : D ⥤ E
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ (post (F ⋙ G)).map f ≫ (Iso.refl ((post (F ⋙ G)).obj Y✝)).hom =
    (Iso.refl ((post (F ⋙ G)).obj X✝)).hom ≫ (post F ⋙ post G).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g = G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map f ≫ G.map (pushout.inl f g) = G.map g ≫ G.map (pushout.inr f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
F : T ⥤ D
inst✝ : F.Faithful
A B : Under X
f g : A ⟶ B
h : (post F).map f = (post F).map g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W✝ X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
x y : CostructuredArrow S T
hl : x.left = y.left
hh : S.map (eqToHom hl) ≫ y.hom = x.hom
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ F.map (A.hom ≫ a) = F.map B.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ (post F).map (homMk a ⋯) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A✝ B✝ : CostructuredArrow S T
f : A✝ ⟶ B✝
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) ⋯ = 𝟙 A✝ ∧ homMk (inv ((proj S T).map f)) ⋯ ≫ f = 𝟙 B✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushoutComparison G f g ≫ G.map (pushout.desc h k w) = pushout.desc (G.map h) (G.map k) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).hom ≫ pullback.fst g f = pullback.snd f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Under X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Under (F.obj X)
⊢ (post F).essImage B

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).hom ≫ pullback.snd g f = pullback.fst f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
h : F.FullyFaithful
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ F.map (A.hom ≫ h.preimage (Hom.right f)) = F.map B.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ pushout.inl g f ≫ (pushoutSymmetry f g).inv = pushout.inr f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
inst✝¹ : S.Full
inst✝ : S.Faithful
⊢ ∀ (s : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))) (m : s.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt),
    (∀ (j : Discrete PEmpty.{1}), m ≫ (asEmptyCone (mk (𝟙 (S.obj Y)))).π.app j = s.π.app j) →
      m = homMk (S.preimage s.pt.hom) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ pushout.inr g f ≫ (pushoutSymmetry f g).inv = pushout.inl f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
X✝ Y✝ : CostructuredArrow F S
f : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f.left ≫ (mk (G.map Y✝.hom)).hom = (mk (G.map X✝.hom)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g : Under X✝
φ : f✝ ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
x✝¹ x✝ : Under ((𝟭 T).obj X)
f : x✝¹ ⟶ x✝
⊢ (𝟭 (Under ((𝟭 T).obj X))).map f ≫ homMk (a.unit.app x✝.right) ⋯ =
    homMk (a.unit.app x✝¹.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
x✝³ x✝² : CostructuredArrow F S
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (post F G S).map x✝¹ = (post F G S).map x✝
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g : Under X✝
φ : f✝ ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
x✝¹ x✝ : Under (F.obj ((𝟭 T).obj X))
f : x✝¹ ⟶ x✝
⊢ ((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x✝.right) ⋯ =
    homMk (a.counit.app x✝¹.right) ⋯ ≫ (𝟭 (Under (F.obj ((𝟭 T).obj X)))).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Faithful
X✝ Y✝ : CostructuredArrow F S
f : (post F G S).obj X✝ ⟶ (post F G S).obj Y✝
⊢ G.map (F.map f.left ≫ Y✝.hom) = G.map X✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Faithful
X✝ Y✝ : CostructuredArrow F S
f : (post F G S).obj X✝ ⟶ (post F G S).obj Y✝
⊢ (post F G S).map (homMk f.left ⋯) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.fst =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under ((𝟭 T).obj X)
⊢ (post F).map ({ app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app A) ≫
      { app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app ((post F).obj A) =
    𝟙 ((post F).obj A)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Full
h : CostructuredArrow (F ⋙ G) (G.obj S)
⊢ (F ⋙ G).map (Iso.refl ((post F G S).obj (mk (G.preimage h.hom))).left).hom ≫ h.hom =
    ((post F G S).obj (mk (G.preimage h.hom))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.snd =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝ : F.Faithful
⊢ (map₂ α β).Faithful

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
      pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯ =
    𝟙 (pullback f prod.fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝³ : G.Faithful
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).Full

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).hom ≫ prod.fst = pullback.fst f prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under (F.obj ((𝟭 T).obj X))
⊢ { app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app ((post G ⋙ map (a.unit.app X)).obj A) ≫
      (post G ⋙ map (a.unit.app X)).map ({ app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app A) =
    𝟙 ((post G ⋙ map (a.unit.app X)).obj A)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝³ : F.EssSurj
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).EssSurj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).hom ≫ prod.snd = pullback.snd f prod.fst ≫ prod.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.fst f prod.fst = prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝⁶ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁵ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝⁴ : F.IsEquivalence
inst✝³ : G.Faithful
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
X✝¹ : T
f✝ g : Under X✝¹
φ : f✝ ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝ : Category.{v_1, u_1} J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (mk (s.app X✝)).hom ≫ D.map f = (mk (s.app Y✝)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.snd f prod.fst ≫ prod.fst = prod.fst ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (pullbackProdFstIsoProd f Z).inv ≫ pullback.snd f prod.fst ≫ prod.snd = prod.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
⊢ (liftCocone D s c p hp).pt.hom ≫ hc.desc ((forget X).mapCocone t) = t.pt.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ (liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc ((forget X).mapCocone t)) ⋯ = t.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.fst =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.snd =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = homMk (hc.desc ((forget X).mapCocone t)) ⋯

Tactic:
by

Goal state after: