mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ inl f g ≫ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
    inl f g ≫ map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ inr f g ≫ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
    inr f g ≫ map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ t.inl ≫ desc ht h k w = h ∧ t.inr ≫ desc ht h k w = k

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.flip.inl ≫ (Iso.refl t.flip.flip.pt).hom = t.inl

Tactic:
simp

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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.flip.flip.inr ≫ (Iso.refl t.flip.flip.pt).hom = t.inr

Tactic:
simp

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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ g ≫ 𝟙 Z = 𝟙 X ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inr ≫ ht.desc s.flip = s.inl

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inl ≫ ht.desc s.flip = s.inr

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inl f g ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inr f g ≫ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app none ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app none

Tactic:
simp

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.left) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.left)

Tactic:
simp

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

Goal state before:
pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app (some WalkingPair.right) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
    (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app (some WalkingPair.right)

Tactic:
simp

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V W : Over X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ Hom.left (homMk (f ≫ g) ⋯) = Hom.left (homMk f w_f ≫ homMk g w_g)

Tactic:
simp

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
S : T
X Y : Over S
f : X ⟶ Y
⊢ ∃ (hg : Hom.left f ≫ Y.hom = X.hom), f = homMk (Hom.left f) ⋯

Tactic:
simp

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 : Over X
φ : f✝ ⟶ g
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : T ⥤ D
G : D ⥤ E
X✝ Y✝ : Over X
f : X✝ ⟶ Y✝
⊢ Hom.left ((post (F ⋙ G)).map f) ≫ 𝟙 ((post (F ⋙ G)).obj Y✝).left =
    𝟙 ((post (F ⋙ G)).obj X✝).left ≫ Hom.left ((post F ⋙ post G).map f)

Tactic:
simp

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 : Over X✝¹
φ : f✝ ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝ : Category.{v_1, u_1} J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ D.map f ≫ (mk (s.app Y✝)).hom = (mk (s.app X✝)).hom

Tactic:
simp

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
S : T
X Y : Under S
f : X ⟶ Y
⊢ ∃ (hg : X.hom ≫ Hom.right f = Y.hom), homMk (Hom.right f) ⋯ = f

Tactic:
simp

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

Goal state before:
pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ Hom.right ((map (f ≫ g)).map k) = Hom.right (eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯)

Tactic:
simp

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
S : C ⥤ D
T : D
X Y : CostructuredArrow S T
f : X ⟶ Y
⊢ S.map f.left ≫ Y.hom = X.hom

Tactic:
simp

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) ≫ (mk f).hom) = mk f

Tactic:
simp

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 : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f.hom) = mk (S.map g' ≫ (mk (S.map g ≫ f.hom)).hom)

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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✝
⊢ Hom.right ((post (F ⋙ G)).map f) ≫ 𝟙 ((post (F ⋙ G)).obj Y✝).right =
    𝟙 ((post (F ⋙ G)).obj X✝).right ≫ Hom.right ((post F ⋙ post G).map f)

Tactic:
simp

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 (mk f.hom) = mk f.hom

Tactic:
simp

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 (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))

Tactic:
simp

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:
simp

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.fst f prod.fst =
    𝟙 (pullback f prod.fst) ≫ pullback.fst f prod.fst

Tactic:
simp

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:
simp

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:
simp

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
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
⊢ ∀ {X Y : CostructuredArrow S T} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.left) ⋯).hom = (isoMk (e₁.app X.left) ⋯).hom ≫ (map₂ α' β').map f

Tactic:
simp

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.snd prod.snd f =
    𝟙 (pullback prod.snd f) ≫ pullback.snd prod.snd f

Tactic:
simp

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
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow X (proj Y F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫ (Under.forget X ⋙ F).map (((proj X (proj Y F) ⋙ proj Y F).toUnder X (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
simp

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
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫
        (proj Y F).map
          (((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).toStructuredArrow Y F (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
simp

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
F : D ⥤ T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow X (proj Y F)} (f : X_1 ⟶ Y_1),
    (𝟭 (StructuredArrow X (proj Y F))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj Y_1)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj X_1)).hom ≫
        (ofStructuredArrowProjEquivalence.functor F Y X ⋙ ofStructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app none = g

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.snd f g = 𝟙 (pullback f g) ≫ pullback.snd f g

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app none = f

Tactic:
simp

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

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

Tactic:
simp

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 × T
⊢ ∀ {X_1 Y : StructuredArrow X (Functor.diag T)} (f : X_1 ⟶ Y),
    (𝟭 (StructuredArrow X (Functor.diag T))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj Y)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) ≫ pullback.fst f g = 𝟙 (pullback f g) ≫ pullback.fst f g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ f ≫ inv f ≫ g = g ≫ 𝟙 Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ (pushoutCoconeOfLeftIso f g).ι.app none = g

Tactic:
simp

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
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : StructuredArrow c (Comma.fst F G)
f : X✝ ⟶ Y✝
⊢ (Under.forget c ⋙ F).map (Under.homMk (Hom.right f).left ⋯) ≫
      { left := Under.mk Y✝.hom, right := Y✝.right.right, hom := Y✝.right.hom }.hom =
    { left := Under.mk X✝.hom, right := X✝.right.right, hom := X✝.right.hom }.hom ≫ G.map (Hom.right f).right

Tactic:
simp

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

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

Tactic:
simp

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
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Under.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ Y✝.left.hom ≫ (Comma.fst F G).map ((Comma.preLeft (Under.forget c) F G).map x✝) = Z✝.left.hom

Tactic:
simp

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
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (proj F Y) X} (g : Y_1 ⟶ Z),
    (Over.forget X ⋙ F).map (((proj (proj F Y) X ⋙ proj F Y).toOver X (fun g ↦ g.hom) ⋯).map g) ≫ Z.left.hom =
      Y_1.left.hom

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ f ≫ 𝟙 Y = g ≫ inv g ≫ f

Tactic:
simp

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
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y} (g : Y_1 ⟶ Z),
    (proj F Y).map (((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).toCostructuredArrow F Y (fun g ↦ g.hom) ⋯).map g) ≫
        Z.left.hom =
      Y_1.left.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app none = f

Tactic:
simp

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
F : T ⥤ D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (proj F Y) X} (f : X_1 ⟶ Y_1),
    (𝟭 (CostructuredArrow (proj F Y) X)).map f ≫ (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj Y_1)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj X_1)).hom ≫
        (ofCostructuredArrowProjEquivalence.functor F Y X ⋙ ofCostructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
simp

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

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

Tactic:
simp

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 × T
⊢ ∀ {X_1 Y : CostructuredArrow (Functor.diag T) X} (f : X_1 ⟶ Y),
    (𝟭 (CostructuredArrow (Functor.diag T) X)).map f ≫
        (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj Y)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inl f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = pushout.inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp

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
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : CostructuredArrow (Comma.fst F G) c
f : X✝ ⟶ Y✝
⊢ (Over.forget c ⋙ F).map (Over.homMk f.left.left ⋯) ≫
      { left := Over.mk Y✝.hom, right := Y✝.left.right, hom := Y✝.left.hom }.hom =
    { left := Over.mk X✝.hom, right := X✝.left.right, hom := X✝.left.hom }.hom ≫ G.map f.left.right

Tactic:
simp

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
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Over.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ (Comma.fst F G).map ((Comma.preLeft (Over.forget c) F G).map x✝) ≫ Z✝.left.hom = Y✝.left.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ f
⊢ (hf.p.op ≫ hf.i.op).unop = f.op.unop

Tactic:
simp

Goal state after: