mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₂)) f₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WithInitial C
⊢ ∀ (a : star ⟶ X),
    a =
      match X with
      | of _x => PUnit.unit
      | star => PUnit.unit

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ ((Functor.const C).obj (F.obj star)).map f ≫ F.map (starInitial.to (of y)) =
    F.map (starInitial.to (of x)) ≫ ((𝟭 (C ⥤ D)).obj (incl ⋙ F)).map f

Tactic:
dsimp
        rw [Category.id_comp, ← F.map_comp]
        congr 1

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ Function.LeftInverse
    (fun h ↦
      (ofπ f.op.unop ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoUnopPushout f f).symm (Iso.refl (Opposite.unop (Opposite.op X))) (Iso.refl (ofπ f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.op ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) h) (Fork.ofι f.op ⋯)
      (Iso.refl (Opposite.op X)) (pullbackIsoUnopPushout f f).op.symm (Iso.refl (Fork.ofι f.op ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ Function.RightInverse
    (fun h ↦
      (ofπ f.op.unop ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoUnopPushout f f).symm (Iso.refl (Opposite.unop (Opposite.op X))) (Iso.refl (ofπ f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.op ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) h) (Fork.ofι f.op ⋯)
      (Iso.refl (Opposite.op X)) (pullbackIsoUnopPushout f f).op.symm (Iso.refl (Fork.ofι f.op ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ Function.LeftInverse
    (fun h ↦
      (ofπ f.unop.op ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoOpPushout f f).symm (Iso.refl (Opposite.op (Opposite.unop X))) (Iso.refl (ofπ f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.unop ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitUnop f f ⋯ ⋯ ⋯) h) (Fork.ofι f.unop ⋯)
      (Iso.refl (Opposite.unop X)) (pullbackIsoOpPushout f f).unop.symm (Iso.refl (Fork.ofι f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ Function.RightInverse
    (fun h ↦
      (ofπ f.unop.op ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoOpPushout f f).symm (Iso.refl (Opposite.op (Opposite.unop X))) (Iso.refl (ofπ f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.unop ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitUnop f f ⋯ ⋯ ⋯) h) (Fork.ofι f.unop ⋯)
      (Iso.refl (Opposite.unop X)) (pullbackIsoOpPushout f f).unop.symm (Iso.refl (Fork.ofι f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ Function.LeftInverse
    (fun h ↦
      (ofι f.op.unop ⋯).isLimitOfIsos ((Cofork.isColimitOfπEquivIsLimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofι f ⋯)
        (Iso.refl (Opposite.unop (Opposite.op Y))) (pushoutIsoUnopPullback f f).symm (Iso.refl (ofι f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Cofork.ofπ f.op ⋯).isColimitOfIsos ((isLimitOfιEquivIsColimitOp f f ⋯ ⋯ ⋯) h) (Cofork.ofπ f.op ⋯)
      ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯) (Iso.refl (Opposite.op Y)) (Iso.refl (Cofork.ofπ f.op ⋯).pt) ⋯
      ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ Function.RightInverse
    (fun h ↦
      (ofι f.op.unop ⋯).isLimitOfIsos ((Cofork.isColimitOfπEquivIsLimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofι f ⋯)
        (Iso.refl (Opposite.unop (Opposite.op Y))) (pushoutIsoUnopPullback f f).symm (Iso.refl (ofι f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Cofork.ofπ f.op ⋯).isColimitOfIsos ((isLimitOfιEquivIsColimitOp f f ⋯ ⋯ ⋯) h) (Cofork.ofπ f.op ⋯)
      ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯) (Iso.refl (Opposite.op Y)) (Iso.refl (Cofork.ofπ f.op ⋯).pt) ⋯
      ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ Function.LeftInverse
    (fun h ↦
      (ofι f.unop.op ⋯).isLimitOfIsos ((Cofork.isColimitOfπEquivIsLimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofι f ⋯)
        (Iso.refl (Opposite.op (Opposite.unop Y))) (pushoutIsoOpPullback f f).symm (Iso.refl (ofι f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Cofork.ofπ f.unop ⋯).isColimitOfIsos ((isLimitOfιEquivIsColimitUnop f f ⋯ ⋯ ⋯) h) (Cofork.ofπ f.unop ⋯)
      ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯) (Iso.refl (Opposite.unop Y))
      (Iso.refl (Cofork.ofπ f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ Function.RightInverse
    (fun h ↦
      (ofι f.unop.op ⋯).isLimitOfIsos ((Cofork.isColimitOfπEquivIsLimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofι f ⋯)
        (Iso.refl (Opposite.op (Opposite.unop Y))) (pushoutIsoOpPullback f f).symm (Iso.refl (ofι f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Cofork.ofπ f.unop ⋯).isColimitOfIsos ((isLimitOfιEquivIsColimitUnop f f ⋯ ⋯ ⋯) h) (Cofork.ofπ f.unop ⋯)
      ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯) (Iso.refl (Opposite.unop Y))
      (Iso.refl (Cofork.ofπ f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
this : Inhabited (StructuredArrow c' (fromPUnit c)) := { default := StructuredArrow.mk (hc.from c') }
i j : StructuredArrow c' (fromPUnit c)
⊢ i.right = j.right

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsInitial c
c' : C
this : Inhabited (CostructuredArrow (fromPUnit c) c') := { default := CostructuredArrow.mk (hc.to c') }
i j : CostructuredArrow (fromPUnit c) c'
⊢ i.left = j.left

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
⊢ ∀ (j_1 : Over j),
    (Cone.whisker (Over.forget j) c).π.app j_1 ≫
        (Functor.whiskerRight (Over.forgetCocone j).ι D ≫
              (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom).app
          j_1 =
      c.π.app j

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cocone D
hc : IsColimit c
j : J
inst✝ : (Under.forget j).Final
this : Nonempty (Under j)
⊢ ∀ (j_1 : Under j),
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D).app j_1 ≫
        (Cocone.whisker (Under.forget j) c).ι.app j_1 =
      c.ι.app j

Tactic:
by cat_disch

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

Goal state before:
pp: case refl
C : Type u
inst✝ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f

Tactic:
exact h.mono_of_eq_fst_snd'

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).symm.hom ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'

Tactic:
have : HasPushout f g := sq.flip.hasPushout
    let e := sq.flip.isoPushout
    rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]
    exact hP₂ _ _ _ f g hf

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m =
    ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
        (t₁.lift
          { pt := s.pt,
            π :=
              Discrete.natTrans fun x ↦
                match x with
                | { as := i } => s.π.app { as := i.succ } }))

Tactic:
apply BinaryFan.IsLimit.hom_ext t₂

Goal state after:
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m ≫ c₂.fst =
    ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      c₂.fst

case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m ≫ c₂.snd =
    ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      c₂.snd
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : Nonempty J
F✝ : J ⥤ C
inst✝ : HasLimit F✝
h : ∀ (j : J), ⊥ (F✝.obj j)
⊢ ⊥ (limit F✝)

Tactic:
exact h (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
X : C
toLimitPresentation✝ : LimitPresentation J X
h : ∀ (j : J), ⊥ (toLimitPresentation✝.diag.obj j)
⊢ ⊥ X

Tactic:
exact h (Classical.arbitrary J)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ c₁'.ι.app j ≫ h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = c₁'.ι.app j ≫ g

Tactic:
by
        rw [h₁'.fac]
        simp [fac, c₁', c₂']

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
by
    obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le.{w} P
    let α := Σ (X : Subtype Q), { p : X.1 ⟶ X.1 // p ≫ p = p }
    let g {X Y : C} (h : Retract Y X) (hX : Q X) : α := ⟨⟨X, hX⟩, h.r ≫ h.i, by simp⟩
    let R (a : α) : Prop := ∃ (X Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
    choose X Y h hX using fun (a : Subtype R) ↦ a.2
    refine ⟨.ofObj Y, inferInstance, (monotone_retractClosure h₂).trans ?_⟩
    rw [retractClosure_isoClosure]
    rintro y ⟨x, hx, ⟨r⟩⟩
    obtain ⟨a, h₁, h₂⟩ : ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx := by
      obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
      exact ⟨_, _, hr⟩
    obtain rfl : x = X a := Subtype.ext_iff.1 (congr_arg Sigma.fst h₂.symm)
    have hri : (h a).r ≫ (h a).i = r.r ≫ r.i := by
      rw [Sigma.ext_iff, heq_eq_eq] at h₂
      exact Subtype.ext_iff.1 h₂.2
    exact ⟨_, ⟨a.1, a.2⟩, ⟨{
      hom := r.i ≫ (h a).r
      inv := (h a).i ≫ r.r
      hom_inv_id := by simp [reassoc_of% hri]
      inv_hom_id := by simp [← reassoc_of% hri]
    }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : Nonempty J
F✝ : J ⥤ C
inst✝ : HasColimit F✝
h : ∀ (j : J), ⊥ (F✝.obj j)
⊢ ⊥ (colimit F✝)

Tactic:
exact h (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
X : C
toColimitPresentation✝ : ColimitPresentation J X
h : ∀ (j : J), ⊥ (toColimitPresentation✝.diag.obj j)
⊢ ⊥ X

Tactic:
exact h (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape Jᵒᵖ ≤ P ↔ P.op.limitsOfShape J ≤ P.op

Tactic:
limitsOfShape_op,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape Jᵒᵖ ≤ P ↔ (P.colimitsOfShape Jᵒᵖ).op ≤ P.op
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
T X Y : C
⊢ Function.LeftInverse (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) fun f ↦ lift f.1 f.2

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
T X Y : C
⊢ Function.RightInverse (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) fun f ↦ lift f.1 f.2

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ lift (snd X Y) (fst X Y) = (β_ X Y).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (snd W Y ≫ g') (fst W Y ≫ g) = (β_ W Y).hom ≫ (g' ⊗ₘ g)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y = CartesianMonoidalCategory.prodComparison F X Y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ ∀ (x y : G ⟶ G), { unop' := x + y } = { unop' := x } + { unop' := y }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : G ⟶ G), { unop' := m • x } = (RingHom.id (End G)ᵐᵒᵖ) m • { unop' := x }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | { unop' := f } => f)
    fun f ↦ { unop' := f }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | { unop' := f } => f)
    fun f ↦ { unop' := f }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
⊢ Module.rank R ↥(Submodule.map (comap f p).subtype f'.ker) ≤ Module.rank R ↥f.ker

Tactic:
exact rank_mono fun x hx ↦ by aesop (add simp Subtype.ext_iff)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ ↑(finrank R ↥(f.domRestrict L).ker) = 0

Tactic:
Nat.cast_eq_zero

Goal state after:
R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ finrank R ↥(f.domRestrict L).ker = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Projective R M
inst✝² : Module.Finite R M
inst✝¹ : Projective R N
inst✝ : Module.Finite R N
⊢ ↑(homTensorHomEquiv R M N P Q) = homTensorHomMap (RingHom.id R) M N P Q

Tactic:
ext m n
  simp only [homTensorHomEquiv, compr₂ₛₗ_apply, mk_apply, LinearEquiv.coe_toLinearMap,
    LinearEquiv.trans_apply, lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm,
    LinearEquiv.refl_apply, rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply,
    lTensorHomToHomLTensor_apply, rTensorHomToHomRTensor_apply, homTensorHomMap_apply,
    map_tmul]

Goal state after: