mathlib-initiative/mathlib-tactics huggingface dataset:
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
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
⊢ LiftableCone G H c

Tactic:
by

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

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

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 : IsLimit (ofι f ⋯)
⊢ (pushout.inl f f).unop ≫ f.unop = (pushout.inr f f).unop ≫ f.unop

Tactic:
by

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 : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.fst f.unop f.unop =
    (pushout.inl f f).unop ≫ (Iso.refl (Opposite.unop Y)).hom

Tactic:
by

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 : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.snd f.unop f.unop =
    (pushout.inr f f).unop ≫ (Iso.refl (Opposite.unop Y)).hom

Tactic:
by

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 : IsLimit (ofι f ⋯)
⊢ (Iso.refl (Opposite.unop Y)).inv ≫ (Cofork.ofπ f.unop ⋯).π ≫ (Iso.refl (Cofork.ofπ f.unop ⋯).pt).hom =
    (Cofork.ofπ f.unop ⋯).π

Tactic:
by

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.unop ⋯)
⊢ f.unop.op ≫ (pullback.fst f.unop f.unop).op = f.unop.op ≫ (pullback.snd f.unop f.unop).op

Tactic:
by

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.unop ⋯)
⊢ (Iso.refl (ofι f.unop.op ⋯).pt).hom ≫ (ofι f ⋯).ι =
    (ofι f.unop.op ⋯).ι ≫ (Iso.refl (Opposite.op (Opposite.unop Y))).hom

Tactic:
by

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.unop ⋯)
⊢ IsLimit (ofι f ⋯)

Tactic:
by

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

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
x : WithInitial C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Fork (𝟙 Y) (𝟙 Y)), (s.ι ≫ e.inv) ≫ (Fork.ofι e.hom ⋯).ι = s.ι

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
s : Fork (𝟙 Y) (𝟙 Y)
m : s.pt ⟶ (Fork.ofι e.hom ⋯).pt
w : m ≫ (Fork.ofι e.hom ⋯).ι = s.ι
⊢ m = s.ι ≫ e.inv

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularMono f
⊢ g ≫ Arrow.Hom.right e.inv ≫ h.left = g ≫ Arrow.Hom.right e.inv ≫ h.right

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y W : C
f : X ⟶ Y
inst✝ : IsRegularMono f
k : W ⟶ Y
h : k ≫ left f = k ≫ right f
m : W ⟶ X
hm : m ≫ f = k
⊢ lift f k h ≫ (Fork.ofι f ⋯).ι = k

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
⊢ ∀ (s : Fork g h), limit.lift (parallelPair g h) s ≫ (Fork.ofι (equalizer.ι g h) ⋯).ι = s.ι

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (equalizer.ι g h) ⋯).pt
w : m ≫ (Fork.ofι (equalizer.ι g h) ⋯).ι = s.ι
⊢ m = limit.lift (parallelPair g h) s

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y z : (WithInitial C)ᵒᵖ
f✝ : unop y ⟶ unop x
g✝ : unop z ⟶ unop y
x✝³ x✝² : (WithInitial C)ᵒᵖ
f : unop x✝² ⟶ unop x✝³
g : unop (op star) ⟶ unop x✝²
x✝¹ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ op star
⊢ (match op f ≫ op g with
    | op f_1 =>
      match x✝³, op star, f_1, op f ≫ op g with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    (match op f with
      | op f_1 =>
        match x✝³, x✝², f_1, op f with
        | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
        | op (of a), op star, x, x_1 =>
          WithTerminal.starTerminal.from
            (match op (of a) with
            | op x =>
              match x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star)
        | op star, op star, x, x_1 =>
          𝟙
            (match op star with
            | op x =>
              match x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star)) ≫
      match op g with
      | op f =>
        match x✝², op star, f, op g with
        | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
        | op (of a), op star, x, x_1 =>
          WithTerminal.starTerminal.from
            (match op (of a) with
            | op x =>
              match x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star)
        | op star, op star, x, x_1 =>
          𝟙
            (match op star with
            | op x =>
              match x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star)

Tactic:
by

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hG : G.Final
⊢ (F ⋙ G).Final

Tactic:
by

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : G.Initial
⊢ (F ⋙ G).Initial

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithTerminal Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match x with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y z : WithTerminal Cᵒᵖ
f✝ : x ⟶ y
g✝ : y ⟶ z
x✝¹ x✝ : WithTerminal Cᵒᵖ
f : x✝¹ ⟶ x✝
g : x✝ ⟶ WithTerminal.star
⊢ (match x✝¹, WithTerminal.star, f ≫ g with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    (match x✝¹, x✝, f with
      | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
      | WithTerminal.of (op unop), WithTerminal.star, x =>
        op
          (starInitial.to
            (Opposite.unop
              (match WithTerminal.of (op unop) with
              | WithTerminal.of x => op (of (Opposite.unop x))
              | WithTerminal.star => op star)))
      | WithTerminal.star, WithTerminal.star, x =>
        𝟙
          (match WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star)) ≫
      match x✝, WithTerminal.star, g with
      | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
      | WithTerminal.of (op unop), WithTerminal.star, x =>
        op
          (starInitial.to
            (Opposite.unop
              (match WithTerminal.of (op unop) with
              | WithTerminal.of x => op (of (Opposite.unop x))
              | WithTerminal.star => op star)))
      | WithTerminal.star, WithTerminal.star, x =>
        𝟙
          (match WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ y✝ : (WithInitial C)ᵒᵖ
f✝ : x✝ ⟶ y✝
x y : C
f : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithInitial C)ᵒᵖ).map f ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                  | op (of a), op star, x, x_2 =>
                    WithTerminal.starTerminal.from
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                | WithTerminal.of (op unop), WithTerminal.star, x =>
                  op
                    (starInitial.to
                      (Opposite.unop
                        (match WithTerminal.of (op unop) with
                        | WithTerminal.of x => op (of (Opposite.unop x))
                        | WithTerminal.star => op star)))
                | WithTerminal.star, WithTerminal.star, x =>
                  𝟙
                    (match WithTerminal.star with
                    | WithTerminal.of x => op (of (unop x))
                    | WithTerminal.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hFG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
⊢ IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
replace hFG := hFG H

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG : IsIso (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
⊢ x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
by

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
⊢ G.Final

Tactic:
by

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
⊢ G.Initial

Tactic:
by

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

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
⊢ IsConnected (StructuredArrow c' (fromPUnit c))

Tactic:
by

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

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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this✝ : aeval_h.toRingHom x + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
hx : f' x = 0
this : Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
⊢ aeval_h.toRingHom x ∈ Ideal.span s'

Tactic:
by

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
⊢ IsConnected (CostructuredArrow (fromPUnit c) c')

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (Fork.ofι g ⋯)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ v ≫ h.left = v ≫ h.right

Tactic:
by

Goal state after: