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

Goal state before:
pp: case none.some.left.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.map (init WalkingPair.left) ≫ (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map (init WalkingPair.left)

Tactic:
cat_disch

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

Goal state before:
pp: case none.some.right.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.map (init WalkingPair.right) ≫
      (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map (init WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.some.left.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.some.right.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

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
⊢ ∀ (s : PushoutCocone f g) (m : pushout f g ⟶ s.pt),
    pushout.inl f g ≫ m = s.inl → pushout.inr f g ≫ m = s.inr → m = pushout.desc s.inl s.inr ⋯

Tactic:
cat_disch

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

Goal state before:
pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pullback f₁ f₂)

Tactic:
cat_disch

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

Goal state before:
pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)

Tactic:
cat_disch

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
A✝ B✝ : Over X
f : A✝ ⟶ B✝
x✝ : IsIso ((forget X).map f)
⊢ f ≫ homMk (inv ((forget X).map f)) ⋯ = 𝟙 A✝ ∧ homMk (inv ((forget X).map f)) ⋯ ≫ f = 𝟙 B✝

Tactic:
cat_disch

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
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ (post F).map (homMk a ⋯) = f

Tactic:
cat_disch

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

Goal state before:
pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pushout f₁ f₂)

Tactic:
cat_disch

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

Goal state before:
pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y S T S' : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
i' : S ⟶ S'
inst✝³ : HasPullback f g
inst✝² : HasPullback (f ≫ i) (g ≫ i)
inst✝¹ : HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')
inst✝ : HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')
⊢ mapDesc f g (i ≫ i') = mapDesc f g i ≫ mapDesc (f ≫ i) (g ≫ i) i' ≫ (congrHom ⋯ ⋯).hom

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y S T S' : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
i' : S' ⟶ S
inst✝³ : HasPushout f g
inst✝² : HasPushout (i ≫ f) (i ≫ g)
inst✝¹ : HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)
inst✝ : HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)
⊢ mapLift f g (i' ≫ i) = (congrHom ⋯ ⋯).hom ≫ mapLift (i ≫ f) (i ≫ g) i' ≫ mapLift f g i

Tactic:
cat_disch

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
Y Z : Under X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
⊢ f ≫ homMk (inv ((forget X).map f)) ⋯ = 𝟙 Y ∧ homMk (inv ((forget X).map f)) ⋯ ≫ f = 𝟙 Z

Tactic:
cat_disch

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
⊢ mk (S.map (𝟙 f.left) ≫ f.hom) = f

Tactic:
cat_disch

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

Goal state before:
pp: case mk.mk.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
left✝ : C
right✝¹ : Discrete PUnit.{1}
hom✝¹ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝¹
right✝ : Discrete PUnit.{1}
hom✝ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝
hh :
  S.map (eqToHom ⋯) ≫ hom { left := left✝, right := right✝, hom := hom✝ } =
    hom { left := left✝, right := right✝¹, hom := hom✝¹ }
⊢ { left := left✝, right := right✝¹, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
cat_disch

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✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (proj Y F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom

Tactic:
cat_disch

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✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom

Tactic:
cat_disch

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 Y (Under.forget X ⋙ F)} (f : X_1 ⟶ Y_1),
    (ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (StructuredArrow Y (Under.forget X ⋙ F))).map f

Tactic:
cat_disch

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
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X.1).map (Hom.right m) = Z✝.hom
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)

Tactic:
cat_disch

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.2 (Under.forget X.1)} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (StructuredArrow X.2 (Under.forget X.1))).map f

Tactic:
cat_disch

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✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
this : (proj F Y).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X).map m.right
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom

Tactic:
cat_disch

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✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
this : (Over.forget X ⋙ F).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit Y).map m.right
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom

Tactic:
cat_disch

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 (Over.forget X ⋙ F) Y} (f : X_1 ⟶ Y_1),
    (ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X ⋙ F) Y)).map f

Tactic:
cat_disch

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
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).1 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).1
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1

Tactic:
cat_disch

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
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).2 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).2
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2

Tactic:
cat_disch

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
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
this : (Over.forget X.1).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X.2).map m.right
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)

Tactic:
cat_disch

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 (Over.forget X.1) X.2} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X.1) X.2)).map f

Tactic:
cat_disch

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
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
      naturality := ⋯ } =
    𝟙
      { obj := fun j ↦ (data.factorizationData (f.hom.app j)).Z,
        map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯), map_id := ⋯, map_comp := ⋯ }

Tactic:
ext j
    dsimp
    rw [← data.mapZ_id]
    congr 1

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : s.inl ≫ m✝ = t.inl
hr' : s.inr ≫ m✝ = t.inr
⊢ s.inl ≫ hs.desc (mk t.inl t.inr ⋯) = t.inl

Tactic:
exact hs.fac _ WalkingSpan.left

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
f g : Arrow C
F : MonoFactorisation f.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (inv (Arrow.Hom.left sq) ≫ F.e) ≫ F.m ≫ Arrow.Hom.right sq = g.hom

Tactic:
simp only [fac_assoc, Arrow.w, IsIso.inv_comp_eq, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map left ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map left

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map right ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map right

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ WalkingParallelPair.casesOn X✝ p q =
    WalkingParallelPair.casesOn X✝ p q ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map left ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map left

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map right ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map right

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ p q).hom =
    (WalkingParallelPair.casesOn X✝ p q).hom ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))

Tactic:
refine ⟨⟨⟨?_⟩, ?_⟩⟩

Goal state after:
case unique_to.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ F ⟶ G

case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))

Tactic:
refine ⟨⟨⟨?_⟩, ?_⟩⟩

Goal state after:
case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default
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
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
x✝¹ x✝ : CostructuredArrow (snd L R) b
f : x✝¹ ⟶ x✝
this : (snd L R).map f.left ≫ x✝.hom = x✝¹.hom
⊢ (𝟭 (CostructuredArrow (snd L R) b)).map f ≫
      CostructuredArrow.homMk { left := 𝟙 x✝.left.left, right := x✝.hom, w := ⋯ } ⋯ =
    CostructuredArrow.homMk { left := 𝟙 x✝¹.left.left, right := x✝¹.hom, w := ⋯ } ⋯ ≫
      (costructuredArrowSndProj L R b ⋙ costructuredArrowSndInclusion L R b).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
⊢ (X Y : Discrete PEmpty.{?u.10 + 1}) → Zero (X ⟶ Y)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isTerminalOfObj G X) (isTerminalObj G X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isTerminalOfObj G X) (isTerminalObj G X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.LeftInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.RightInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
h : 𝟙 X = 0 ∧ 𝟙 Y = 0
⊢ 0 ≫ 0 = 𝟙 X ∧ 0 ≫ 0 = 𝟙 Y

Tactic:
cat_disch

Goal state after: