awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DualNumber
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 : M
⊢ IsNilpotent (R := TrivSqZeroExt R M) (inr x)

Tactic:
refine ⟨2, by simp [pow_two]⟩
-- Module: Mathlib.RingTheory.DualNumber
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
rw : IsUnit a.fst ∨ IsNilpotent a.fst
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
rw [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst]

Premises used: TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst, TrivSqZeroExt.isUnit_iff_isUnit_fst
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
(em _).imp_right fun ha ↦ ?_

Premises used: em, Or.imp_right
-- Module: Mathlib.RingTheory.DualNumber
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
refine : ∀ (ha : ¬IsUnit a.fst), IsNilpotent a.fst
⊢ IsUnit a.fst ∨ IsNilpotent a.fst

Tactic:
refine (em _).imp_right fun ha ↦ ?_

Premises used: em, Or.imp_right
-- Module: Mathlib.RingTheory.DualNumber
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
obtain : ∀ (I : Ideal R) (hI : I.IsMaximal) (haI : a.fst ∈ I), IsNilpotent a.fst
⊢ IsNilpotent a.fst

Tactic:
obtain ⟨I, hI, haI⟩ := exists_max_ideal_of_mem_nonunits (mem_nonunits_iff.mpr ha)

Premises used: Iff.mpr, mem_nonunits_iff, exists_max_ideal_of_mem_nonunits
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
(h _ hI).imp fun n hn ↦ ?_

Premises used: Exists.imp, IsNilpotent
-- Module: Mathlib.RingTheory.DualNumber
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
refine : ∀ (n : ℕ) (hn : I ^ n = 0), a.fst ^ n = 0
⊢ IsNilpotent a.fst

Tactic:
refine (h _ hI).imp fun n hn ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.RingTheory.DualNumber
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
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0

Tactic:
hn.le (Ideal.pow_mem_pow haI _)

Premises used: Set.Mem, setOf, Eq.le, Set.singleton, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.DualNumber
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
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0

Tactic:
exact hn.le (Ideal.pow_mem_pow haI _)

Premises used: Eq.le, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
M : Type u_2
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
simp [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst, em']

Premises used: TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst, TrivSqZeroExt.isUnit_iff_isUnit_fst, em'
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
simp_rw : TrivSqZeroExt.fst x = 0 → ∃ (x_1 : R[ε]), TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1
⊢ TrivSqZeroExt.fst x = 0 ↔ ε ∣ x

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]

Premises used: dvd_def, MulZeroClass.zero_mul, iff_self_and, exists_and_left, zero_add, TrivSqZeroExt.ext_iff, zero_smul, TrivSqZeroExt.snd_mul, DualNumber.fst_eps, DualNumber.snd_eps, MulOpposite.unop_op, TrivSqZeroExt.fst_mul, MulOpposite.smul_eq_mul_unop, one_mul
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
h : TrivSqZeroExt.fst x = 0
⊢ ∃ (x_1 : R[ε]), TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
⟨.inl x.snd, rfl⟩

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.inl, Exists.intro, rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
h : TrivSqZeroExt.fst x = 0
⊢ ∃ (x_1 : R[ε]), TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
exact ⟨.inl x.snd, rfl⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
inst : Semiring R
⊢ IsNilpotent.{u_1} (R := R[ε]) ε

Tactic:
TrivSqZeroExt.isNilpotent_inr 1

Premises used: TrivSqZeroExt.isNilpotent_inr, OfNat.ofNat, DualNumber.eps
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
inst : DivisionSemiring R
x : R[ε]
⊢ IsNilpotent x ↔ ε ∣ x

Tactic:
simp only [isNilpotent_iff_isNilpotent_fst, isNilpotent_iff_eq_zero, fst_eq_zero_iff_eps_dvd]

Premises used: TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst, DualNumber.fst_eq_zero_iff_eps_dvd, isNilpotent_iff_eq_zero
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ b = 1 - a

Tactic:
rw [add_comm, ← eq_sub_iff_add_eq] at h

Premises used: eq_sub_iff_add_eq, add_comm
-- Module: Mathlib.RingTheory.DualNumber
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
inr : ∀ (ha : fst a ≠ 0), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rcases eq_or_ne (fst a) 0 with ha | ha

Premises used: TrivSqZeroExt.fst, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : b = 1 - a
ha : fst a = 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp [isUnit_iff_isUnit_fst, h, ha]

Premises used: TrivSqZeroExt.isUnit_iff_isUnit_fst
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
a b : K[ε]
h : b = 1 - a
ha : fst a ≠ 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp [isUnit_iff_isUnit_fst, h, ha]

Premises used: TrivSqZeroExt.isUnit_iff_isUnit_fst
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
(eq_or_ne I ⊥).imp_right fun hb ↦ ?_

Premises used: Bot.bot, eq_or_ne, Or.imp_right
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
refine : ∀ (hb : I ≠ ⊥), I = Ideal.span {ε} ∨ I = ⊤
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
refine (eq_or_ne I ⊥).imp_right fun hb ↦ ?_

Premises used: Bot.bot, eq_or_ne, Or.imp_right
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
⊢ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
(eq_or_ne I ⊤).symm.imp_left fun ht ↦ ?_

Premises used: Or.imp_left, Or.symm, eq_or_ne, Top.top
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
refine : ∀ (ht : I ≠ ⊤), I = Ideal.span {ε}
⊢ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
refine (eq_or_ne I ⊤).symm.imp_left fun ht ↦ ?_

Premises used: Or.imp_left, Or.symm, eq_or_ne, Top.top
-- Module: Mathlib.RingTheory.DualNumber
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
inr : ∀ (hx : IsNilpotent x), ε ∣ x
⊢ ε ∣ x

Tactic:
rcases isUnit_or_isNilpotent x with hx | hx

Premises used: TrivSqZeroExt.isUnit_or_isNilpotent
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsUnit x
⊢ ε ∣ x

Tactic:
absurd (Ideal.eq_top_of_isUnit_mem _ hxI hx) ht

Premises used: Ideal.eq_top_of_isUnit_mem, absurd
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsUnit x
⊢ ε ∣ x

Tactic:
exact absurd (Ideal.eq_top_of_isUnit_mem _ hxI hx) ht

Premises used: Ideal.eq_top_of_isUnit_mem, absurd
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
inr inr₁ inr₂ inr₃ : IsNilpotent x
⊢ ε ∣ x

Tactic:
rwa [← isNilpotent_iff_eps_dvd]

Premises used: DualNumber.isNilpotent_iff_eps_dvd
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
⊢ ∀ 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]
-- Module: Mathlib.RingTheory.DualNumber
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
obtain : ∀ (r : K[ε]) (hxI : ε * r ∈ I) (hx0 : ε * r ≠ 0), ∃ (r_1 : K[ε]), ε = r_1 * (ε * r)
⊢ ∃ (r : K[ε]), ε = r * x

Tactic:
obtain ⟨r, rfl⟩ := hd _ hxI

Premises used: rfl
-- Module: Mathlib.RingTheory.DualNumber
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) ε)
h2 : snd (ε * r) = snd (HSMul.hSMul (β := K[ε]) (fst r) ε)
⊢ ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε

Tactic:
ext
-- Module: Mathlib.RingTheory.DualNumber
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
⊢ fst (ε * r) = fst (HSMul.hSMul (β := K[ε]) (fst r) ε)

Tactic:
simp
-- Module: Mathlib.RingTheory.DualNumber
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
⊢ snd (ε * r) = snd (HSMul.hSMul (β := K[ε]) (fst r) ε)

Tactic:
simp
-- Module: Mathlib.RingTheory.DualNumber
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) ε

Tactic:
have : ε * r = (fst r) • ε := by ext <;> simp
-- Module: Mathlib.RingTheory.DualNumber
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) ε
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) ε
⊢ ∃ (r_1 : K[ε]), ε = r_1 * (ε * r)

Tactic:
rw [this] at hxI hx0 ⊢
-- Module: Mathlib.RingTheory.DualNumber
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) ε
contrapose : ∀ (hx0 : fst r = 0), HSMul.hSMul (β := K[ε]) (fst r) ε = 0
⊢ fst r ≠ 0

Tactic:
contrapose hx0
-- Module: Mathlib.RingTheory.DualNumber
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
this : ε * r = HSMul.hSMul (β := K[ε]) (fst r) ε
hx0 : fst r = 0
⊢ HSMul.hSMul (β := K[ε]) (fst r) ε = 0

Tactic:
simp [hx0]
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
have hr : fst r ≠ 0 := by
      contrapose hx0
      simp [hx0]
-- Module: Mathlib.RingTheory.DualNumber
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) ε

Tactic:
⟨r⁻¹, ?_⟩

Premises used: Inv.inv, Exists.intro
-- Module: Mathlib.RingTheory.DualNumber
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
refine : ε = r⁻¹ * HSMul.hSMul (β := K[ε]) (fst r) ε
⊢ ∃ (r_1 : K[ε]), ε = r_1 * HSMul.hSMul (β := K[ε]) (fst r) ε

Tactic:
refine ⟨r⁻¹, ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
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⁻¹ * HSMul.hSMul (β := K[ε]) (fst r) ε

Tactic:
simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr]

Premises used: TrivSqZeroExt.ext_iff, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ ∀ 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]
-- Module: Mathlib.RingTheory.DualNumber
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 {ε}

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DualNumber
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 {ε}
refine_2 : Ideal.span {ε} ≤ I
⊢ I = Ideal.span {ε}

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DualNumber
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[ε]
refine_1 : x ∈ I → ε ∣ x
⊢ x ∈ I → Membership.mem (γ := Submodule K[ε] K[ε]) (Ideal.span {ε}) x

Tactic:
simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]

Premises used: Ideal.mem_span_singleton', dvd_def, eq_comm, DualNumber.commute_eps_right, Commute.eq
-- Module: Mathlib.RingTheory.DualNumber
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[ε]
refine_2 : ε ∣ x → x ∈ I
⊢ Membership.mem (γ := Submodule K[ε] K[ε]) (Ideal.span {ε}) x → x ∈ I

Tactic:
simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]

Premises used: Ideal.mem_span_singleton', dvd_def, eq_comm, DualNumber.commute_eps_right, Commute.eq
-- Module: Mathlib.RingTheory.DualNumber
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 ∈ I
⊢ ε ∣ x

Tactic:
simp_rw [hd _ hx]
-- Module: Mathlib.RingTheory.DualNumber
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
refine_2 : ∀ (p : K[ε]), ε * p ∈ I
⊢ x ∈ I

Tactic:
obtain ⟨p, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.DualNumber
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
p : K[ε]
refine_2 : ∀ (y : K[ε]) (hyI : y ∈ I) (hy0 : y ≠ 0), ε * p ∈ I
⊢ ε * p ∈ I

Tactic:
obtain ⟨y, hyI, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.DualNumber
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
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
refine_2 : ∀ (r : K[ε]) (hr : ε = r * y), ε * p ∈ I
⊢ ε * p ∈ I

Tactic:
obtain ⟨r, hr⟩ := hd' _ hyI hy0
-- Module: Mathlib.RingTheory.DualNumber
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
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
refine_2 : p * r * y ∈ I
⊢ ε * p ∈ I

Tactic:
rw [(commute_eps_left _).eq, hr, ← mul_assoc]

Premises used: mul_assoc, DualNumber.commute_eps_left, Commute.eq
-- Module: Mathlib.RingTheory.DualNumber
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
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ p * r * y ∈ I

Tactic:
Ideal.mul_mem_left _ _ hyI

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DualNumber
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
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ p * r * y ∈ I

Tactic:
exact Ideal.mul_mem_left _ _ hyI

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
⊢ Ideal.IsMaximal (α := K[ε]) (Ideal.span {ε})

Tactic:
⟨?_, fun I hI ↦ ?_⟩

Premises used: Ideal.IsMaximal.mk, And.intro
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
refine_1 : Ne (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
refine_2 : ∀ (I : Ideal K[ε]) (hI : Ideal.span {ε} < I), I = ⊤
⊢ Ideal.IsMaximal (α := K[ε]) (Ideal.span {ε})

Tactic:
refine ⟨?_, fun I hI ↦ ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
⊢ Ne (α := Ideal K[ε]) (Ideal.span {ε}) ⊤

Tactic:
simp [ne_eq, Ideal.eq_top_iff_one, Ideal.mem_span_singleton', TrivSqZeroExt.ext_iff]

Premises used: Ideal.mem_span_singleton', ne_eq, Ideal.eq_top_iff_one, TrivSqZeroExt.ext_iff
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
refine_2 : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤
refine_2₁ : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) (Ideal.span {ε})), Eq (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
refine_2₂ : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊤), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊤ ⊤
⊢ I = ⊤

Tactic:
rcases ideal_trichotomy I with rfl | rfl | rfl

Premises used: DualNumber.ideal_trichotomy, rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥
⊢ Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤

Tactic:
simp at hI
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥
⊢ Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤

Tactic:
first | simp at hI | simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) (Ideal.span {ε})
⊢ Eq (α := Ideal K[ε]) (Ideal.span {ε}) ⊤

Tactic:
simp at hI
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) (Ideal.span {ε})
⊢ Eq (α := Ideal K[ε]) (Ideal.span {ε}) ⊤

Tactic:
first | simp at hI | simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
⊢ Eq.{u_2 + 1} (α := Ideal K[ε]) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
⊢ Eq.{u_2 + 1} (α := Ideal K[ε]) ⊤ ⊤

Tactic:
first | simp at hI | simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := Ideal K[ε]) (IsLocalRing.maximalIdeal K[ε]) (Ideal.span {ε})

Tactic:
(IsLocalRing.eq_maximalIdeal isMaximal_span_singleton_eps).symm

Premises used: Eq.symm, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
inl : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥
inr : Submodule.IsPrincipal (R := K[ε]) (Ideal.span {ε})
inr₁ : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊤
⊢ Submodule.IsPrincipal I

Tactic:
rcases ideal_trichotomy I with rfl | rfl | rfl

Premises used: DualNumber.ideal_trichotomy, rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥

Tactic:
bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥

Tactic:
exact bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal (R := K[ε]) (Ideal.span {ε})

Tactic:
⟨_, rfl⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal (R := K[ε]) (Ideal.span {ε})

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊤

Tactic:
top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.RingTheory.DualNumber
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊤

Tactic:
exact top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
inl : ∀ (ha : IsUnit a), ∃ (c : K[ε]), a * c = b ∨ b * c = a
inr : ∀ (ha : IsNilpotent a), ∃ (c : K[ε]), a * c = b ∨ b * c = a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a

Tactic:
rcases isUnit_or_isNilpotent a with ha | ha

Premises used: TrivSqZeroExt.isUnit_or_isNilpotent
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ IsUnit a

Tactic:
ha
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsUnit a
inl : ∀ (a : K[ε]ˣ), ∃ (c : K[ε]), (↑a : K[ε]) * c = b ∨ b * c = (↑a : K[ε])
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a

Tactic:
lift a to K[ε]ˣ using ha
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ (↑a : K[ε]) * ((↑a⁻¹ : K[ε]) * b) = b ∨ b * ((↑a⁻¹ : K[ε]) * b) = (↑a : K[ε])

Tactic:
simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ∃ (c : K[ε]), (↑a : K[ε]) * c = b ∨ b * c = (↑a : K[ε])

Tactic:
exact ⟨a⁻¹ * b, by simp⟩