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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
m : s.pt ⟶ (constCone J X).pt
hm : ∀ (j : J), m ≫ (constCone J X).π.app j = s.π.app j
⊢ m = s.π.app (Classical.arbitrary J)

Tactic:
simpa using hm (Classical.arbitrary _)

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
m : (constCocone J X).pt ⟶ s.pt
hm : ∀ (j : J), (constCocone J X).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app (Classical.arbitrary J)

Tactic:
simpa using hm (Classical.arbitrary _)

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

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

pp: case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).left.app
      x✝ =
    (𝟙 (mkCommaObject x)).left.app x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).right =
    (𝟙 (mkCommaObject x)).right

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).left.app
      x✝ =
    (𝟙 (mkCommaObject x)).left.app x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).right =
    (𝟙 (mkCommaObject x)).right
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        none) =
    none

pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
val✝ : J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        (some val✝)) =
    some val✝

Tactic:
<;>

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        none) =
    none

case some
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
val✝ : J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        (some val✝)) =
    some val✝
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
a✝ : Discrete J
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        (of a✝)) =
    of a✝

pp: case star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        star) =
    star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
a✝ : Discrete J
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        (of a✝)) =
    of a✝

case star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        star) =
    star
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 : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
⊢ {j₁ j₂ : CostructuredArrow F d} → (j₁ ⟶ j₂) → Z j₁.left j₁.hom → Z j₂.left j₂.hom

Tactic:
intro j₁ j₂ f a
    fapply h₁ _ _ _ _ f.left _ a
    convert! f.w
    simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.zero) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.zero))

Tactic:
simp [opParallelPairIso]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.one) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.one))

Tactic:
simp [opParallelPairIso]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).inv.app (op WalkingParallelPair.zero) =
    𝟙 ((walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op).obj (op WalkingParallelPair.zero))

Tactic:
simp [opParallelPairIso]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).inv.app (op WalkingParallelPair.one) =
    𝟙 ((walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op).obj (op WalkingParallelPair.one))

Tactic:
simp [opParallelPairIso]

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

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

pp: case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).left =
    (𝟙 (mkCommaObject x)).left

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).right.app
      x✝ =
    (𝟙 (mkCommaObject x)).right.app x✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).left =
    (𝟙 (mkCommaObject x)).left

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).right.app
      x✝ =
    (𝟙 (mkCommaObject x)).right.app x✝
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
          (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).fiber =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.fiber

pp: case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
        (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).base =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.base

Tactic:
<;>

Goal state after:
case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
          (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).fiber =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.fiber

case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
        (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).base =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.base
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
⊢ r.left ≫ s.π = r.right ≫ s.π

Tactic:
by rw [← ht, assoc, s.condition, reassoc_of% kt]

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

Goal state before:
pp: case refine_3.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.fst f g =
    s.fst ≫ pullback.fst f g

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.snd f g =
    s.fst ≫ pullback.snd f g

Tactic:
<;>

Goal state after:
case refine_3.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.fst f g =
    s.fst ≫ pullback.fst f g

case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.snd f g =
    s.fst ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inl g₁ g₂ ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯

Tactic:
congr 1
    exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inr g₁ g₂ ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯

Tactic:
congr 1
    exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f → P.pushouts f

Tactic:
(_ : IsIso f)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
⊢ P.pushouts f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom g)

Tactic:
convert! hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom