mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t t₁ t₂ : Cocone K
f : t₁ ⟶ t₂
⊢ { pt := t₁.pt.right,
              ι :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Under.Hom.right (t₁.ι.app a)
                    | star => t₁.pt.hom,
                  naturality := ⋯ } }.ι.app
        star ≫
      Under.Hom.right f.hom =
    { pt := t₂.pt.right,
            ι :=
              {
                app := fun x ↦
                  match x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } }.ι.app
      star

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
α : Type u₂
F : J ⥤ Discrete α
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (liftToDiscrete F ⋙ Discrete.functor F.obj).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ F.map f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ ∀ (X : ⊤.FullSubcategory),
    ⊤.ι.map ((Iso.refl (𝟭 ⊤.FullSubcategory)).hom.app X) ≫ (Iso.refl (⊤.lift (𝟭 C) ⋯ ⋙ ⊤.ι)).hom.app (⊤.ι.obj X) =
      𝟙 (⊤.ι.obj X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
constructor
  · rintro ⟨n, f, hfs, hfk⟩
    set ulift_var := MvPolynomial.renameEquiv R Equiv.ulift
    refine
      ⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
        Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩
    simpa using! Submodule.fg_bot
  · rintro ⟨ι, hfintype, f, hf⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective
    refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective
    simpa using! Submodule.fg_bot

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : LocallySmall.{w', v_1, u_1} C
⊢ (∃ J x, Nonempty (C ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
← ObjectProperty.exists_equivalence_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : LocallySmall.{w', v_1, u_1} C
⊢ (∃ J x, Nonempty (C ≌ J)) ↔ ∃ J x, Nonempty (⊤.FullSubcategory ≌ J)
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
by
  wlog hC : LocallySmall.{w} C; · simp [essentiallySmall_iff, hC]
  simp only [hC, ← exists_equivalence_iff_of_locallySmall, true_and]
  refine ⟨fun H ↦ H.1, fun H ↦ ⟨H⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
φ : F ⟶ G
p q : F.Elements
x✝ : p ⟶ q
f : p.fst ⟶ q.fst
h : (ConcreteCategory.hom (F.map f)) p.snd = q.snd
hb :
  (ConcreteCategory.hom (φ.app q.fst)) ((ConcreteCategory.hom (F.map f)) p.snd) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app p.fst)) p.snd)
⊢ (ConcreteCategory.hom (G.map f))
      (match p with
        | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd =
    (match q with
      | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
F : C ⥤ Type w
X : C
snd✝ : F.obj X
Y : C
y : F.obj Y
⊢ Function.Injective fun g ↦ ↑g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ⋯⟩ = 𝟙 A✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ⋯⟩ ≫ f = 𝟙 B✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case mk.mk.e_7
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).toFunctor.obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : base✝¹ = base✝
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ fiber✝¹ ≍ fiber✝

Tactic:
cat_disch

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithTerminal C)).map f

Tactic:
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
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithInitial C)).map f

Tactic:
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
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
cat_disch

Goal state after:
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:
cat_disch

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

Goal state before:
pp: case zero.zero.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero)

Tactic:
cat_disch

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

Goal state before:
pp: case zero.one.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.left ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.left

Tactic:
cat_disch

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

Goal state before:
pp: case zero.one.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.right ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.right

Tactic:
cat_disch

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

Goal state before:
pp: case one.one.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.one)

Tactic:
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.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:
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:
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
h : IsColimit (ofπ f ⋯)
⊢ f.unop ≫ (pullback.fst f f).unop = f.unop ≫ (pullback.snd f f).unop

Tactic:
by simp only [← unop_comp, pullback.condition]

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:
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:
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
h : IsColimit (Cofork.ofπ f.op ⋯)
⊢ f.op.unop ≫ (pullback.fst f.op f.op).unop = f.op.unop ≫ (pullback.snd f.op f.op).unop

Tactic:
by simp only [← unop_comp, pullback.condition]

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

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
⊢ colimit.ι (ι F X✝ ⋙ map α ⋙ H) d ≫
      (fiberwiseColimit (map α ⋙ H)).map f ≫
        (HasColimit.isoOfNatIso
              (((ι F Y✝).associator (map α) H).symm ≪≫
                isoWhiskerRight (ιCompMap α Y✝) H ≪≫ (α.app Y✝).toFunctor.associator (ι G Y✝) H) ≪≫
            Final.colimitIso (α.app Y✝).toFunctor (ι G Y✝ ⋙ H)).hom =
    colimit.ι (ι F X✝ ⋙ map α ⋙ H) d ≫
      (HasColimit.isoOfNatIso
              (((ι F X✝).associator (map α) H).symm ≪≫
                isoWhiskerRight (ιCompMap α X✝) H ≪≫ (α.app X✝).toFunctor.associator (ι G X✝) H) ≪≫
            Final.colimitIso (α.app X✝).toFunctor (ι G X✝ ⋙ H)).hom ≫
        (fiberwiseColimit H).map f

Tactic:
simp only [map, Cat.Hom.comp_toFunctor, comp_obj, ι_obj,
        fiberwiseColimit_map, ιNatTrans, ιCompMap, Iso.trans_hom, Category.assoc, ι_colimMap_assoc,
        NatTrans.comp_app, whiskerRight_app, Functor.comp_map, Cat.Hom₂.eqToHom_toNatTrans,
        eqToHom_app, map_id, Category.comp_id, associator_hom_app, colimit.ι_pre_assoc,
        HasColimit.isoOfNatIso_ι_hom_assoc, Iso.symm_hom, isoWhiskerRight_hom, associator_inv_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Final.ι_colimitIso_hom, Category.id_comp,
        Final.ι_colimitIso_hom_assoc, colimit.ι_pre]

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))
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:
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:
cat_disch

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:
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.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ HasPullbacksAlong (Over.mk f).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
A B : FGAlgCat R
PA : FGAlgCatSkeleton R
eA : ↑A.obj ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R PA).obj
PB : FGAlgCatSkeleton R
eB : ↑B.obj ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R PB).obj
f : (A ⟶ B) → ↑(FGAlgCatSkeleton.eval R PA).obj → ↑(FGAlgCatSkeleton.eval R PB).obj :=
  fun g x ↦ eB ((ConcreteCategory.hom g.hom) (eA.symm x))
u v : A ⟶ B
h : f u = f v
a : ↑(FGAlgCatSkeleton.eval R PA).obj
⊢ (CommAlgCat.Hom.hom u.hom) (eA.symm a) = (CommAlgCat.Hom.hom v.hom) (eA.symm a)

Tactic:
exact eB.injective (congr_fun h a)

Goal state after: