mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : AddCommMonoid M''
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
inst✝¹¹ : Module A M'
inst✝¹⁰ : IsLocalization S A
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R M''
inst✝⁶ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ : M →ₗ[R] M''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = (RingHom.id R) r • lift S f (g ∘ₗ h) ⋯

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Goal state after:
R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : AddCommMonoid M''
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
inst✝¹¹ : Module A M'
inst✝¹⁰ : IsLocalization S A
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R M''
inst✝⁶ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ : M →ₗ[R] M''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ ∘ₗ f = ((RingHom.id R) r • lift S f (g ∘ₗ h) ⋯) ∘ₗ f
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 ⥤ Over X
F : C ⥤ D
t✝ t : Cone K
x✝ : star ⟶ star
⊢ (((Functor.const (WithTerminal J)).obj t.pt.left).map x✝ ≫
      match star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) =
    (match star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) ≫
      (liftFromOver.obj K).map x✝

Tactic:
aesop

Goal state after:
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 ⥤ Over X
F : C ⥤ D
t✝ t : Cone K
a : J
x✝ : of a ⟶ star
⊢ (((Functor.const (WithTerminal J)).obj t.pt.left).map x✝ ≫
      match star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) =
    (match of a with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) ≫
      (liftFromOver.obj K).map x✝

Tactic:
aesop

Goal state after:
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 : Cocone K
x✝ : star ⟶ star
⊢ ((liftFromUnder.obj K).map x✝ ≫
      match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) =
    (match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      ((Functor.const (WithInitial J)).obj t.pt.right).map x✝

Tactic:
aesop

Goal state after:
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 : Cocone K
b : J
x✝ : star ⟶ of b
⊢ ((liftFromUnder.obj K).map x✝ ≫
      match of b with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) =
    (match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      ((Functor.const (WithInitial J)).obj t.pt.right).map x✝

Tactic:
aesop

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

Goal state before:
pp: case inl
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : P x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

Tactic:
aesop

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

Goal state before:
pp: case inr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : Q x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
x : (a : α) × Subtype (P a)
⊢ (⨆ a, P a) ↑x.snd

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
x✝ : Subtype (⨆ a, P a)
x : C
hx : (⨆ a, P a) x
⊢ ∃ a, (fun x ↦ ⟨↑x.snd, ⋯⟩) a = ⟨x, hx⟩

Tactic:
aesop

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P.op

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
by
  subst h
  simp

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
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ none ⟶ some y

Tactic:
by cases f

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
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ (fun x ↦
        match some y, none, x with
        | .(none), .(some j), Hom.term j => PUnit.unit
        | y, .(y), Hom.id .(y) => 𝟙 (widePullbackShapeEquivObj y))
      ((fun f ↦
          match none, some y, f with
          | some x, some y, f => cast ⋯ (Hom.id (some y))
          | none, some y, f => PEmpty.casesOn (fun t ↦ f = t → (none ⟶ some y)) f ⋯
          | some x, none, f => Hom.term x
          | none, none, f => Hom.id none)
        f) =
    f

Tactic:
by cases f

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 : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj x =
    ({ obj := ⇑widePullbackShapeEquivObj, map := fun {X Y} ↦ ⇑(widePullbackShapeEquivMap X Y), map_id := ⋯,
            map_comp := ⋯ } ⋙
          { obj := ⇑widePullbackShapeEquivObj.symm,
            map := fun {X Y} f ↦
              (widePullbackShapeEquivMap (widePullbackShapeEquivObj.symm X) (widePullbackShapeEquivObj.symm Y)).symm
                (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
            map_id := ⋯, map_comp := ⋯ }).obj
      x

Tactic:
aesop

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 : WithTerminal (Discrete J)
⊢ ({ obj := ⇑widePullbackShapeEquivObj.symm,
            map := fun {X Y} f ↦
              (widePullbackShapeEquivMap (widePullbackShapeEquivObj.symm X) (widePullbackShapeEquivObj.symm Y)).symm
                (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
            map_id := ⋯, map_comp := ⋯ } ⋙
          { obj := ⇑widePullbackShapeEquivObj, map := fun {X Y} ↦ ⇑(widePullbackShapeEquivMap X Y), map_id := ⋯,
            map_comp := ⋯ }).obj
      x =
    (𝟭 (WithTerminal (Discrete J))).obj x

Tactic:
aesop

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.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
i : H.mapCocone (liftColimit ((isColimitWhiskerEquiv F c).symm hc)) ≅ Cocone.whisker F c :=
  liftedColimitMapsToOriginal ((isColimitWhiskerEquiv F c).symm hc)
⊢ H.mapCocone (extendCocone.obj (liftColimit ((isColimitWhiskerEquiv F c).symm hc))) ≅ c

Tactic:
refine ?_ ≪≫ ((extendCocone (F := F)).mapIso i) ≪≫ ((coconesEquiv F (G ⋙ H)).counitIso.app _)

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
i : H.mapCocone (liftColimit ((isColimitWhiskerEquiv F c).symm hc)) ≅ Cocone.whisker F c :=
  liftedColimitMapsToOriginal ((isColimitWhiskerEquiv F c).symm hc)
⊢ H.mapCocone (extendCocone.obj (liftColimit ((isColimitWhiskerEquiv F c).symm hc))) ≅
    extendCocone.obj (H.mapCocone (liftColimit ((isColimitWhiskerEquiv F c).symm hc)))
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W✝
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ π a ≫ m = e a

Tactic:
exact hm a

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✝ : x ⟶ y
g✝ : y ⟶ z
x✝¹ x✝ : WithInitial Cᵒᵖ
f : WithInitial.star ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ (match WithInitial.star, x✝, f ≫ g 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, x✝¹, f 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 x✝¹, x✝, g 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)

Tactic:
by subsingleton

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

Goal state before:
pp: case refine_1
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 ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inl f f = (pushout.inl f f).op.unop

Tactic:
Quiver.Hom.unop_op,

Goal state after:
case refine_1
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 ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inl f f = pushout.inl f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_2
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 ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f = (pushout.inr f f).op.unop

Tactic:
Quiver.Hom.unop_op,

Goal state after:
case refine_2
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 ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f = pushout.inr f f
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 subsingleton

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case succ
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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he

Goal state after:
case succ
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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this✝ : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
this : Q R[X] S ((g'.comp ↑e.symm).comp MvPolynomial.C)
⊢ Q R S (g'.comp MvPolynomial.C)
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ IsRegularEpi f

Tactic:
have := isSplitEpi_of_epi f
    infer_instance

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₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ IsColimit
    (PushoutCocone.mk
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
apply rightSquareIsPushout _ rfl (pushoutIsPushout _ _)
  simpa [PushoutCocone.pasteHoriz] using PushoutCocone.mkSelfIsColimit (pushoutIsPushout _ _)

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 Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (diagonal f)

Tactic:
rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (inv (fst f f))
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f ∧ Q f
⊢ P (e.toRingHom.comp f) ∧ Q (e.toRingHom.comp f)

Tactic:
exact ⟨hP.1 f e hf.1, hQ.1 f e hf.2⟩

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ P) fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
introv R h hQ H
  let e := h.symm.equiv
  have : (e.symm : _ →+* _).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S) := by
    ext r
    simp [e]
  apply h₂ hQ
  rw [← this]
  exact h₁.1 _ _ H

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
⊢ IsPullback g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
let i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom rfl (by simp)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ IsPullback g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
⊢ f 0 ⟶ c₂.pt

pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (i : Fin n) → f i.succ ⟶ c₂.pt

Tactic:
· apply c₂.inl

Goal state after:
case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (i : Fin n) → f i.succ ⟶ c₂.pt
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : K ≅ Discrete.functor fun n_1 ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit K

Tactic:
hasColimit_iff_of_iso that

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : K ≅ Discrete.functor fun n_1 ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit (Discrete.functor fun n_1 ↦ K.obj { as := n_1 })
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (X ◁ toUnit Y ≫ (ρ_ X).hom) ≫ (ρ_ X).inv = fst X Y ≫ (ρ_ X).inv

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (toUnit X ▷ Y ≫ (λ_ Y).hom) ≫ (λ_ Y).inv = snd X Y ≫ (λ_ Y).inv

Tactic:
aesop

Goal state after: