mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ g.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_247✝

Tactic:
← cancel_epi app₁.hom,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_247✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case «2»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨2, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

case «2»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom ≫ app₁.inv =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
app₁.hom_inv_id,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ 𝟙 (f.obj' 1 _proof_298✝) =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_298✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ g.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_299✝

Tactic:
← cancel_epi app₁.hom,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_299✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app zero = (𝟙 F).app zero

pp: case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app one = (𝟙 F).app one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app zero = (𝟙 F).app zero

case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app one = (𝟙 F).app one
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app zero = (𝟙 G).app zero

pp: case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app one = (𝟙 G).app one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app zero = (𝟙 G).app zero

case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app one = (𝟙 G).app one
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app zero = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app zero

pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app one = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app zero = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app zero

case one
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app one = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app one
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
a₁✝ : A ⧸ p
a : A
a₂✝ : A ⧸ p
b : A
hab :
  (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) a) =
    (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) b)
⊢ (algebraMap A B) (a - b) ∈ P

Tactic:
map_sub

Goal state after:
R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
a₁✝ : A ⧸ p
a : A
a₂✝ : A ⧸ p
b : A
hab :
  (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) a) =
    (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) b)
⊢ (algebraMap A B) a - (algebraMap A B) b ∈ P
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case hxs
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ OrderDual.toDual J ∈ S

pp: case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
· refine ⟨show J.IsPrime by infer_instance, e⟩

Goal state after:
case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.radical.IsMinimalPrime p} → p ∈ {p | I.IsMinimalPrime p}

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.IsMinimalPrime p} → p ∈ {p | I.radical.IsMinimalPrime p}

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.radical.IsMinimalPrime p} → p ∈ {p | I.IsMinimalPrime p}

case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.IsMinimalPrime p} → p ∈ {p | I.radical.IsMinimalPrime p}
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) → IsNilpotent a

pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulLeft R a)

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) → IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulLeft R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Tactic:
constructor <;> rintro ⟨n, hn⟩

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a

pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ a ^ n = 0

pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulLeft R a ^ n = 0

Tactic:
<;>

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ a ^ n = 0

case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulLeft R a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0

pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0

Tactic:
<;>

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0

case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) → IsNilpotent a

pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulRight R a)

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) → IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulRight R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a

Tactic:
constructor <;> rintro ⟨n, hn⟩

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a

pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ a ^ n = 0

pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulRight R a ^ n = 0

Tactic:
<;>

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ a ^ n = 0

case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulRight R a ^ n = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

pp: case h₂
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

Tactic:
<;>

Goal state after:
case h₁
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

case h₂
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

Tactic:
introv e h₁ h₂ h₃

Goal state after:
case h₂
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit ((Ideal.Quotient.mk J) x)
⊢ IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I → (algebraMap R S) x ∈ I

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
⊢ (algebraMap R S) x ∈ I → mk' S x y ∈ I

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I → (algebraMap R S) x ∈ I

case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
⊢ (algebraMap R S) x ∈ I → mk' S x y ∈ I
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h✝ : p.coeff k = 0
⊢ 0 = a * (algebraMap R A) (p.coeff k)

pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h✝ : ¬p.coeff k = 0
⊢ a * (algebraMap R A) (p.coeff k) = a * (algebraMap R A) (p.coeff k)

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h✝ : p.coeff k = 0
⊢ 0 = a * (algebraMap R A) (p.coeff k)

case neg
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h✝ : ¬p.coeff k = 0
⊢ a * (algebraMap R A) (p.coeff k) = a * (algebraMap R A) (p.coeff k)
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if (p₁ * p₂).coeff k ≠ 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k

Tactic:
Ne

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k