awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ IsNilpotent x
have mpr : x ^ (n * 2) = 0
Tactic: refine ⟨n * 2, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ x ^ (n * 2) = 0
have mpr : HPow.hPow (β := ℕ) (x ^ n) 2 = 0
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ HPow.hPow (β := ℕ) (x ^ n) 2 = 0
have mpr : (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
⊢ HPow.hPow (β := ℕ) (x ^ n) 2 = 0
have mpr₁ : (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
have mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
Tactic: rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
have mpr₁ : HPow.hPow (β := ℕ) (x.fst ^ n) 2 = fst.{u_1, u_2} (M := M) 0
Tactic: rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
mpr₁ : HPow.hPow (β := ℕ) (x.fst ^ n) 2 = fst.{u_1, u_2} (M := M) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
have mpr₂ : HPow.hPow (α := R) (β := ℕ) 0 2 = fst.{u_1, u_2} (M := M) 0
Tactic: rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
mpr₁ : HPow.hPow (β := ℕ) (x.fst ^ n) 2 = fst.{u_1, u_2} (M := M) 0
mpr₂ : HPow.hPow (α := R) (β := ℕ) 0 2 = fst.{u_1, u_2} (M := M) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
have mpr₃ : Eq.{u_1 + 1} (α := R) 0 (fst.{u_1, u_2} (M := M) 0)
Tactic: rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
mpr₁ : HPow.hPow (β := ℕ) (x.fst ^ n) 2 = fst.{u_1, u_2} (M := M) 0
mpr₂ : HPow.hPow (α := R) (β := ℕ) 0 2 = fst.{u_1, u_2} (M := M) 0
mpr₃ : Eq.{u_1 + 1} (α := R) 0 (fst.{u_1, u_2} (M := M) 0)
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
have mpr₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
    HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
  snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₄ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
  snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₅ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₅ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₆ : HAdd.hAdd (α := M) 0 0 = snd.{u_1, u_2} (R := R) 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₅ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₆ : HAdd.hAdd (α := M) 0 0 = snd.{u_1, u_2} (R := R) 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₇ : Eq.{u_2 + 1} (α := M) 0 (snd.{u_1, u_2} (R := R) 0)
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₅ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₆ : HAdd.hAdd (α := M) 0 0 = snd.{u_1, u_2} (R := R) 0
mpr₇ : Eq.{u_2 + 1} (α := M) 0 (snd.{u_1, u_2} (R := R) 0)
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
have mpr₈ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsNilpotent (R := TrivSqZeroExt R M) (inl r) ↔ IsNilpotent r
have rw : IsNilpotent (fst.{u_1, u_2} (M := M) (inl r)) ↔ IsNilpotent r
Tactic: rw [isNilpotent_iff_isNilpotent_fst, fst_inl]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
r : R
rw : IsNilpotent (fst.{u_1, u_2} (M := M) (inl r)) ↔ IsNilpotent r
⊢ IsNilpotent (R := TrivSqZeroExt R M) (inl r) ↔ IsNilpotent r
have rw₁ : IsNilpotent r ↔ IsNilpotent r
Tactic: rw [isNilpotent_iff_isNilpotent_fst, fst_inl]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a
have rw : IsUnit a.fst ∨ IsNilpotent a.fst
Tactic: rw [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a.fst ∨ IsNilpotent a.fst
have refine : ∀ (ha : ¬IsUnit a.fst), IsNilpotent a.fst
Tactic: refine (em _).imp_right fun ha ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
⊢ IsNilpotent a.fst
have obtain : ∀ (I : Ideal R) (hI : I.IsMaximal) (haI : a.fst ∈ I), IsNilpotent a.fst
Tactic: obtain ⟨I, hI, haI⟩ := exists_max_ideal_of_mem_nonunits (mem_nonunits_iff.mpr ha)
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
⊢ IsNilpotent a.fst
have refine : ∀ (n : ℕ) (hn : I ^ n = 0), a.fst ^ n = 0
Tactic: refine (h _ hI).imp fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ε ∣ x
have simp_rw : TrivSqZeroExt.fst x = 0 → ∃ (x_1 : R[ε]), TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1
Tactic: simp_rw [dvd_def, TrivSqZeroExt.ext_iff, TrivSqZeroExt.fst_mul, TrivSqZeroExt.snd_mul,
    fst_eps, snd_eps, zero_mul, zero_smul, zero_add, MulOpposite.smul_eq_mul_unop,
    MulOpposite.unop_op, one_mul, exists_and_left, iff_self_and]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ IsUnit a ∨ IsUnit b
have h₁ : b = 1 - a
Tactic: rw [add_comm, ← eq_sub_iff_add_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : b = 1 - a
⊢ IsUnit a ∨ IsUnit b
have inl : ∀ (ha : fst a = 0), IsUnit a ∨ IsUnit b
Tactic: rcases eq_or_ne (fst a) 0 with ha | ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : b = 1 - a
inl : ∀ (ha : fst a = 0), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b
have inr : ∀ (ha : fst a ≠ 0), IsUnit a ∨ IsUnit b
Tactic: rcases eq_or_ne (fst a) 0 with ha | ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤
have refine : ∀ (hb : I ≠ ⊥), I = Ideal.span {ε} ∨ I = ⊤
Tactic: refine (eq_or_ne I ⊥).imp_right fun hb ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
⊢ I = Ideal.span {ε} ∨ I = ⊤
have refine : ∀ (ht : I ≠ ⊤), I = Ideal.span {ε}
Tactic: refine (eq_or_ne I ⊤).symm.imp_left fun ht ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
⊢ ε ∣ x
have inl : ∀ (hx : IsUnit x), ε ∣ x
Tactic: rcases isUnit_or_isNilpotent x with hx | hx
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
inl : ∀ (hx : IsUnit x), ε ∣ x
⊢ ε ∣ x
have inr : ∀ (hx : IsNilpotent x), ε ∣ x
Tactic: rcases isUnit_or_isNilpotent x with hx | hx
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
⊢ I = Ideal.span {ε}
have hd : ∀ x ∈ I, ε ∣ x
Tactic: have hd : ∀ x ∈ I, ε ∣ x := by
    intro x hxI
    rcases isUnit_or_isNilpotent x with hx | hx
    · exact absurd (Ideal.eq_top_of_isUnit_mem _ hxI hx) ht
    · rwa [← isNilpotent_iff_eps_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
x : K[ε]
hxI : x ∈ I
hx0 : x ≠ 0
⊢ ∃ (r : K[ε]), ε = r * x
have obtain : ∀ (r : K[ε]) (hxI : ε * r ∈ I) (hx0 : ε * r ≠ 0), ∃ (r_1 : K[ε]), ε = r_1 * (ε * r)
Tactic: obtain ⟨r, rfl⟩ := hd _ hxI
Cleared hypotheses: x, hxI, hx0
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
have h1 : fst (ε * r) = fst (HSMul.hSMul (β := K[ε]) (fst r) ε)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
h1 : fst (ε * r) = fst (HSMul.hSMul (β := K[ε]) (fst r) ε)
⊢ ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
have h2 : snd (ε * r) = snd (HSMul.hSMul (β := K[ε]) (fst r) ε)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ∃ (r_1 : K[ε]), ε = r_1 * (ε * r)
have this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
Tactic: have : ε * r = (fst r) • ε := by ext <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
⊢ ∃ (r_1 : K[ε]), ε = r_1 * (ε * r)
have rw : ∀ (hxI : HSMul.hSMul (β := K[ε]) (fst r) ε ∈ I) (hx0 : HSMul.hSMul (β := K[ε]) (fst r) ε ≠ 0)
  (this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε), ∃ (r_1 : K[ε]), ε = r_1 * HSMul.hSMul (β := K[ε]) (fst r) ε
Tactic: rw [this] at hxI hx0 ⊢
Cleared hypotheses: hxI, hx0, this
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : HSMul.hSMul (β := K[ε]) (fst r) ε ∈ I
hx0 : HSMul.hSMul (β := K[ε]) (fst r) ε ≠ 0
this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
⊢ fst r ≠ 0
have contrapose : ∀ (hx0 : fst r = 0), HSMul.hSMul (β := K[ε]) (fst r) ε = 0
Tactic: contrapose hx0
Cleared hypotheses: hx0
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : HSMul.hSMul (β := K[ε]) (fst r) ε ∈ I
hx0 : HSMul.hSMul (β := K[ε]) (fst r) ε ≠ 0
this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
⊢ ∃ (r_1 : K[ε]), ε = r_1 * HSMul.hSMul (β := K[ε]) (fst r) ε
have hr : fst r ≠ 0
Tactic: have hr : fst r ≠ 0 := by
      contrapose hx0
      simp [hx0]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : HSMul.hSMul (β := K[ε]) (fst r) ε ∈ I
hx0 : HSMul.hSMul (β := K[ε]) (fst r) ε ≠ 0
this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
hr : fst r ≠ 0
⊢ ∃ (r_1 : K[ε]), ε = r_1 * HSMul.hSMul (β := K[ε]) (fst r) ε
have refine : ε = r⁻¹ * HSMul.hSMul (β := K[ε]) (fst r) ε
Tactic: refine ⟨r⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ I = Ideal.span {ε}
have hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
Tactic: have hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x := by
    intro x hxI hx0
    obtain ⟨r, rfl⟩ := hd _ hxI
    have : ε * r = (fst r) • ε := by ext <;> simp
    rw [this] at hxI hx0 ⊢
    have hr : fst r ≠ 0 := by
      contrapose hx0
      simp [hx0]
    refine ⟨r⁻¹, ?_⟩
    simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
⊢ I = Ideal.span {ε}
have refine_1 : I ≤ Ideal.span {ε}
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
refine_1 : I ≤ Ideal.span {ε}
⊢ I = Ideal.span {ε}
have refine_2 : Ideal.span {ε} ≤ I
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
x : K[ε]
⊢ x ∈ I → Membership.mem (γ := Submodule K[ε] K[ε]) (Ideal.span {ε}) x
have refine_1 : x ∈ I → ε ∣ x
Tactic: simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
x : K[ε]
⊢ Membership.mem (γ := Submodule K[ε] K[ε]) (Ideal.span {ε}) x → x ∈ I
have refine_2 : ε ∣ x → x ∈ I
Tactic: simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
x : K[ε]
hx : ε ∣ x
⊢ x ∈ I
have refine_2 : ∀ (p : K[ε]), ε * p ∈ I
Tactic: obtain ⟨p, rfl⟩ := hx
Cleared hypotheses: x, hx