awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
r_1 : R
m : M
mem : m ∈ r • P
h : m ∈ N
⊢ r_1 • m ∈ N

Tactic:
exact N.smul_mem _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x x_1 y : M
hx_1 : x_1 ∈ r • P
hy_1 : y ∈ r • P
hx : x_1 ∈ N
hy : y ∈ N
⊢ x_1 + y ∈ N

Tactic:
N.add_mem hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x x_1 y : M
hx_1 : x_1 ∈ r • P
hy_1 : y ∈ r • P
hx : x_1 ∈ N
hy : y ∈ N
⊢ x_1 + y ∈ N

Tactic:
exact N.add_mem hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
⊢ 0 ∈ N

Tactic:
N.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
⊢ 0 ∈ N

Tactic:
exact N.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
smul₀ : ∀ (p : M) (hp : p ∈ P), r • p ∈ N
smul₁ : ∀ (r_1 : R), ∀ m ∈ r • P, ∀ (h : m ∈ N), r_1 • m ∈ N
add : ∀ (x y : M), x ∈ r • P → y ∈ r • P → ∀ (hx : x ∈ N) (hy : y ∈ N), x + y ∈ N
zero : 0 ∈ N
⊢ x ∈ N

Tactic:
induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem

Premises used: Submodule.Quotient.mk_smul, Submodule.zero_mem, Submodule.smul_inductionOn_pointwise, Submodule.zero, Submodule.add, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
apply : N ≤ N' ⊔ I • N
⊢ N ≤ N'

Tactic:
apply le_of_le_smul_of_le_jacobson_bot hN hIjac

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
apply_fun : ∀ (hmaple : comap (I • N).mkQ (map (I • N).mkQ N) ≤ comap (I • N).mkQ (map (I • N).mkQ N')), N ≤ N' ⊔ I • N
apply_fun₁ : Monotone (comap (I • N).mkQ)
⊢ N ≤ N' ⊔ I • N

Tactic:
apply_fun comap (I • N).mkQ at hmaple

Premises used: Submodule.comap, Submodule.mkQ, HSMul.hSMul
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ Monotone (comap (I • N).mkQ)

Tactic:
apply Submodule.comap_mono

Premises used: Submodule.comap_mono
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ Monotone (comap (I • N).mkQ)

Tactic:
on_goal 2 => apply Submodule.comap_mono

Premises used: Submodule.comap_mono
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : comap (I • N).mkQ (map (I • N).mkQ N) ≤ comap (I • N).mkQ (map (I • N).mkQ N')
⊢ N ≤ I • N ⊔ N'

Tactic:
simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at hmaple

Premises used: Submodule.smul_le_right, sup_of_le_right, Submodule.comap_map_mkQ
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : N ≤ I • N ⊔ N'
grw : N ≤ I • N ⊔ N'
grw₁ grw₂ : N ≤ N
⊢ N ≤ N' ⊔ I • N

Tactic:
grw [sup_comm, ← hmaple]

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
a : N ≤ N'
a₁ : N' ≤ N
⊢ N = N'

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N ≤ N'

Tactic:
le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot hN hIjac hmaple.le

Premises used: Eq.le, Submodule.le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N ≤ N'

Tactic:
exact le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot hN hIjac hmaple.le

Premises used: Eq.le, Submodule.le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ comap (I • N).mkQ (map (I • N).mkQ N) = comap (I • N).mkQ (map (I • N).mkQ N')

Tactic:
apply_fun comap (I • N).mkQ at hmaple

Premises used: Submodule.comap, Submodule.mkQ, HSMul.hSMul
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : comap (I • N).mkQ (map (I • N).mkQ N) = comap (I • N).mkQ (map (I • N).mkQ N')
⊢ N = I • N ⊔ N'

Tactic:
simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at hmaple

Premises used: Submodule.smul_le_right, sup_of_le_right, Submodule.comap_map_mkQ
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : N = I • N ⊔ N'
a : N' ≤ I • N ⊔ N'
⊢ N' ≤ N

Tactic:
rw [hmaple]
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : N = I • N ⊔ N'
⊢ N' ≤ I • N ⊔ N'

Tactic:
apply le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h :
  Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
    (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N
⊢ ∃ (t : Set M),
    Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) t ∧
      (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' t = s ∧ span R t = N

Tactic:
use Quotient.out '' s

Premises used: Quotient.out
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h : Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s)
h₁ : (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s
h₂ : span R (Quotient.out '' s) = N
⊢ Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
    (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N

Tactic:
split_ands
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s)

Tactic:
simp [Set.InjOn]

Premises used: Set.InjOn
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s

Tactic:
simp [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h : N = span R (Quotient.out '' s)
⊢ span R (Quotient.out '' s) = N

Tactic:
symm
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h : map (I • N).mkQ N = map (I • N).mkQ (span R (Quotient.out '' s))
⊢ N = span R (Quotient.out '' s)

Tactic:
apply eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot hN hIjac

Premises used: Submodule.eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ map (I • N).mkQ N = map (I • N).mkQ (span R (Quotient.out '' s))

Tactic:
simp [← hsspan, map_span, Set.image_image]

Premises used: Set.image_image, Submodule.map_span
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x : R
inst : Ring R
h : IsNilpotent x
obtain : ∀ (n : ℕ) (hn : x ^ n = 0), IsNilpotent (-x)
⊢ IsNilpotent (-x)

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
h : (-x) ^ n = 0
⊢ IsNilpotent (-x)

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
h : HPow.hPow (α := R) (-1) n * x ^ n = 0
h₁ : HPow.hPow (α := R) (-1) n * 0 = 0
h₂ h₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (-x) ^ n = 0

Tactic:
rw [neg_pow, hn, mul_zero]

Premises used: MulZeroClass.mul_zero, neg_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x : R
inst : Ring R
⊢ IsNilpotent (-x) ↔ IsNilpotent x

Tactic:
⟨fun h => neg_neg x ▸ h.neg, fun h => h.neg⟩

Premises used: IsNilpotent.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
ha : IsNilpotent a
t : R
obtain : ∀ (k : ℕ) (ha : a ^ k = 0), IsNilpotent (t • a)
⊢ IsNilpotent (t • a)

Tactic:
obtain ⟨k, ha⟩ := ha
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
h : (t • a) ^ k = 0
⊢ IsNilpotent (t • a)

Tactic:
use k
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
h : t ^ k • a ^ k = 0
h₁ : HSMul.hSMul (β := S) (t ^ k) 0 = 0
h₂ h₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ (t • a) ^ k = 0

Tactic:
rw [smul_pow, ha, smul_zero]

Premises used: smul_zero, smul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
obtain : ∀ (n : ℕ) (hn : r ^ n = 0), IsUnit (r - 1)
⊢ IsUnit (r - 1)

Tactic:
obtain ⟨n, hn⟩ := hnil
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)

Tactic:
⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩

Premises used: HSub.hSub, IsUnit, Finset.range, HPow.hPow, Units.mk, Exists.intro, OfNat.ofNat, Finset.sum, Neg.neg, rfl
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
refine_1 : (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1
refine_2 : (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1
⊢ IsUnit (r - 1)

Tactic:
refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1

Tactic:
simp [mul_geom_sum, hn]

Premises used: mul_geom_sum
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1

Tactic:
simp [geom_sum_mul, hn]

Premises used: geom_sum_mul
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
rw : IsUnit (r - 1)
⊢ IsUnit (1 - r)

Tactic:
rw [← IsUnit.neg_iff, neg_sub]

Premises used: neg_sub, IsUnit.neg_iff
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
isUnit_sub_one hnil

Premises used: IsNilpotent.isUnit_sub_one
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
exact isUnit_sub_one hnil

Premises used: IsNilpotent.isUnit_sub_one
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
rw : IsUnit (-r - 1)
⊢ IsUnit (r + 1)

Tactic:
rw [← IsUnit.neg_iff, neg_add']

Premises used: IsUnit.neg_iff, neg_add'
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)

Tactic:
isUnit_sub_one hnil.neg

Premises used: IsNilpotent.isUnit_sub_one, IsNilpotent.neg
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)

Tactic:
exact isUnit_sub_one hnil.neg

Premises used: IsNilpotent.isUnit_sub_one, IsNilpotent.neg
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 + r)

Tactic:
add_comm r 1 ▸ isUnit_add_one hnil

Premises used: IsNilpotent.isUnit_add_one, Eq.rec, add_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
rw : IsUnit (1 + r * (↑hu.unit⁻¹ : R))
⊢ IsUnit (u + r)

Tactic:
rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]

Premises used: add_mul, IsUnit.mul_val_inv, Inv.inv, Units.isUnit_mul_units, IsUnit.unit
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ Commute r (↑hu.unit⁻¹ : R)

Tactic:
replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r (↑hu.unit⁻¹ : R)
⊢ IsUnit (1 + r * (↑hu.unit⁻¹ : R))

Tactic:
IsNilpotent.isUnit_one_add ?_

Premises used: IsNilpotent.isUnit_one_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r (↑hu.unit⁻¹ : R)
refine : IsNilpotent (r * (↑hu.unit⁻¹ : R))
⊢ IsUnit (1 + r * (↑hu.unit⁻¹ : R))

Tactic:
refine IsNilpotent.isUnit_one_add ?_

Premises used: IsNilpotent.isUnit_one_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r (↑hu.unit⁻¹ : R)
⊢ IsNilpotent (r * (↑hu.unit⁻¹ : R))

Tactic:
(hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

Premises used: Iff.mpr, Inv.inv, IsUnit.isNilpotent_mul_unit_of_commute_iff, IsUnit.unit, Units.isUnit
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r (↑hu.unit⁻¹ : R)
⊢ IsNilpotent (r * (↑hu.unit⁻¹ : R))

Tactic:
exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

Premises used: Iff.mpr, Inv.inv, IsUnit.isNilpotent_mul_unit_of_commute_iff, IsUnit.unit, Units.isUnit
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (r + u)

Tactic:
add_comm r u ▸ hnil.isUnit_add_left_of_commute hu h_comm

Premises used: Eq.rec, add_comm, IsNilpotent.isUnit_add_left_of_commute, Eq.symm
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ Commute x (-x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False

Tactic:
simpa using H.isUnit_add_right_of_commute hx.neg (by simp)

Premises used: IsUnit.neg, IsNilpotent.isUnit_add_right_of_commute
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
x : R
hx : IsNilpotent x
⊢ ¬¬IsNilpotent x

Tactic:
simpa only [not_not] using hx

Premises used: Classical.not_not
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
zero : ∀ (hn : HPow.hPow (β := ℕ) e 0 = 0), e = 0
succ : ∀ (n : ℕ) (hn : e ^ (n + 1) = 0), e = 0
⊢ e = 0

Tactic:
obtain ⟨rfl | n, hn⟩ := nilp

Premises used: rfl
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : HPow.hPow (β := ℕ) e 0 = 0
⊢ Eq.{u_1 + 1} (α := R) 1 0

Tactic:
rw [pow_zero] at hn

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : Eq.{u_1 + 1} (α := R) 1 0
zero : 1 * e = 0
zero₁ : 0 * e = 0
zero₂ zero₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ e = 0

Tactic:
rw [← one_mul e, hn, zero_mul]

Premises used: MulZeroClass.zero_mul, one_mul
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
succ : e = e ^ (n + 1)
succ₁ succ₂ : e = e
⊢ e = 0

Tactic:
rw [← hn, idem.pow_succ_eq]

Premises used: IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
y : R
hy : Prime y
⊢ IsRadical y

Tactic:
fun _ _ ↦ hy.dvd_of_dvd_pow

Premises used: IsRadical, Prime.dvd_of_dvd_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
simp_rw : IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x
⊢ IsRadical.{u_1} (R := R) 0 ↔ IsReduced R

Tactic:
simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]

Premises used: isReduced_iff, zero_dvd_iff, exists_imp, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
⊢ IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x

Tactic:
forall_comm

Premises used: IsRadical, forall_comm
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
⊢ IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
k : ℕ
hk : 1 < k
simp_rw : IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R), x ^ k = 0 → x = 0
simp_rw₁ : (∀ (x : R), 0 ∣ x ^ k → 0 ∣ x) ↔ ∀ (x : R), x ^ k = 0 → x = 0
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0

Tactic:
simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]

Premises used: zero_dvd_iff, zero_isRadical_iff, isRadical_iff_pow_one_lt
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
obtain : ∀ (z : R) (hy : IsRadical (x * z)) (h0 : x * z ≠ 0) (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1
⊢ ∀ (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1

Tactic:
obtain ⟨z, rfl⟩ := hxy

Premises used: rfl
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1

Tactic:
fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)

Premises used: HMul.hMul, mul_dvd_mul_iff_right, right_ne_zero_of_mul, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
refine : ∀ (w : R) (dvd : x ∣ HPow.hPow (β := ℕ) w 2), x * z ∣ HPow.hPow (β := ℕ) (w * z) 2
⊢ ∀ (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1

Tactic:
refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)

Premises used: HMul.hMul, mul_dvd_mul_iff_right, right_ne_zero_of_mul, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ HPow.hPow (β := ℕ) w 2
rw : x * z ∣ HPow.hPow (β := ℕ) w 2 * HPow.hPow (β := ℕ) z 2
⊢ x * z ∣ HPow.hPow (β := ℕ) (w * z) 2

Tactic:
rw [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ HPow.hPow (β := ℕ) w 2
a : z ∣ HPow.hPow (β := ℕ) z 2
⊢ x * z ∣ HPow.hPow (β := ℕ) w 2 * HPow.hPow (β := ℕ) z 2

Tactic:
gcongr