mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (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:
rfl

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

Goal state before:
pp: case of.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ : Discrete J
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl

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

Goal state before:
pp: case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some y ⟶ some y)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
a✝ : α
⊢ π a✝ ≫ m₂ = π a✝ ≫ m₂

Tactic:
rfl

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 G : C ⥤ D
η : F ⟶ G
X Y : WithInitial C
f : X ⟶ Y
x : C
x✝ : star ⟶ of x
⊢ ((map F).map x✝ ≫
      match of x with
      | of x => η.app x
      | star => 𝟙 star) =
    (match star with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x✝

Tactic:
rfl

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 G : C ⥤ D
η : F ⟶ G
X Y : WithInitial C
f : X ⟶ Y
x✝ : star ⟶ star
⊢ ((map F).map x✝ ≫
      match star with
      | of x => η.app x
      | star => 𝟙 star) =
    (match star with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x✝

Tactic:
rfl

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 : 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
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ F.map f.left ≫ j₂.hom = j₁.hom

Tactic:
convert! f.w

Goal state after:
case e'_3
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
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
e_1✝ : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ (fromPUnit d).obj j₂.right)
⊢ j₁.hom = j₁.hom ≫ (fromPUnit d).map f.right
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
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
⊢ F.map f.left ≫ j₂.hom = j₁.hom

Tactic:
convert! f.w

Goal state after:
case e'_3
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
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
e_1✝ : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ (fromPUnit d).obj j₂.right)
⊢ j₁.hom = j₁.hom ≫ (fromPUnit d).map f.right
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom (prelaxfunctor.map h✝) ≫
              (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv).toNatTrans.app
      star

Tactic:
rfl

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 : C
⊢ F.map (starInitial.to (incl.obj x)) = F.map (starInitial.to (of x))

Tactic:
rfl

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

Tactic:
rfl

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

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ op f = WithInitial.down (down f).op

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
a✝ : C
⊢ (match 𝟙 (op (of a✝)) with
    | op f =>
      match op (of a✝), op (of a✝), f, 𝟙 (op (of a✝)) 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 (of a✝) with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
⊢ (match 𝟙 (op star) with
    | op f =>
      match op star, op star, f, 𝟙 (op star) 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 star with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
rfl

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

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match WithTerminal.of a✝, WithTerminal.of a✝, 𝟙 (WithTerminal.of a✝) 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 WithTerminal.of a✝ with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match WithTerminal.star, WithTerminal.star, 𝟙 WithTerminal.star 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 WithTerminal.star with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
rfl

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

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:
rw [Category.assoc, s.condition, Category.assoc]

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)
⊢ f =
    down
      (match f with
      | op f => (WithTerminal.down f).op)

Tactic:
rfl

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
x : C
⊢ (match 𝟙 (op (of x)) with
    | op f => (WithTerminal.down f).op) =
    𝟙 (WithTerminal.of (op x))

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hg' : (ker g.toRingHom).FG
g' : MvPolynomial (Fin n) R →+* S := g.toRingHom
hg : Surjective ⇑g'
⊢ Q R S f

Tactic:
change (ker g').FG at hg'

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : MvPolynomial (Fin n) R →+* S := g.toRingHom
hg : Surjective ⇑g'
hg' : (ker g').FG
⊢ Q R S f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (Ideal.comap MvPolynomial.C (ker g')).FG

Tactic:
convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap MvPolynomial.C (ker g') = Ideal.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom (ker g')
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (gr.left ≫ f) ≫ h = (gr.right ≫ f) ≫ h

Tactic:
by rw [Category.assoc, Category.assoc, comm]; simp only [← Category.assoc, eq_whisker gr.w]

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₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ =
    pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)

Tactic:
trans l₁' ≫ pullback.fst _ _
  · rw [← Category.assoc]
    congr 1
    exact IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left
  · exact pullback.lift_fst _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
g'✝ : Y'✝ ⟶ X✝
h : IsPullback f'✝ g'✝ g✝ f✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : Y✝ ⟶ w✝⁴
w✝ : S✝ ⟶ w✝³
hp : P w✝²
hq : IsPullback w✝¹ g✝ w✝² w✝
⊢ P.pullbacks g'✝

Tactic:
exact P.pullbacks_mk (h.paste_horiz hq) hp

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'
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
have : HasPullbacksAlong (Over.mk f).hom := by cat_disch
  have : pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁)
        ((Category.comp_id _).trans e₂) =
      ((pullbackSymmetry _ _).hom ≫
          ((Over.pullback _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
        (pullbackSymmetry _ _).hom ≫
          ((Over.pullback g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := by
    ext <;> simp
  rw [this]
  apply P.comp_mem <;> rw [P.cancel_left_of_respectsIso]
  exacts [overPullbackMap _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
    overPullbackMap _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]

Goal state after: