-- Mathlib/RingTheory/DualNumber.lean
lemma ideal_trichotomy [DivisionRing K] (I : Ideal K[ε]) :
    I = ⊥ ∨ I = .span {ε} ∨ I = ⊤

Proof state:
case refine_2.intro.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ ε * p ∈ I

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

Result:
case refine_2.intro.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ p * r * y ∈ I

Proof state:
case intro
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 = fst r • ε
⊢ ∃ r_1, ε = r_1 * (ε * r)

Tactic:
rw [this] at hxI hx0 ⊢

Result:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
⊢ ∃ r_1, ε = r_1 * fst r • ε

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤

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

Result:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
⊢ I = Ideal.span {ε} ∨ I = ⊤

Proof state:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ ε ∣ x → x ∈ I

Tactic:
intro hx

Result:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : ε ∣ x
⊢ x ∈ I

Proof state:
case inr
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
⊢ ε ∣ x

Tactic:
rwa [← isNilpotent_iff_eps_dvd]

Result:
no goals

Proof state:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
hr : fst r ≠ 0
⊢ ∃ r_1, ε = r_1 * fst r • ε

Tactic:
refine ⟨r⁻¹, ?_⟩

Result:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
hr : fst r ≠ 0
⊢ ε = r⁻¹ * fst r • ε

Proof state:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
hr : fst r ≠ 0
⊢ ε = r⁻¹ * fst r • ε

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

Result:
no goals

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
⊢ I = Ideal.span {ε}

Tactic:
refine le_antisymm ?_ ?_ <;> intro x <;>
  simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]

Result:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ε ∣ x

case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ ε ∣ x → x ∈ I

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
this : ε * r = fst r • ε
hx0 : fst r = 0
⊢ fst r • ε = 0

Tactic:
simp [hx0]

Result:
no goals

Proof state:
case refine_2.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p : K[ε]
⊢ ε * p ∈ I

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

Result:
case refine_2.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
⊢ ε * p ∈ I

Proof state:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ε ∣ x

Tactic:
intro hx

Result:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : x ∈ I
⊢ ε ∣ x

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
⊢ ∀ x ∈ I, ε ∣ x

Tactic:
intro x hxI

Result:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
⊢ ε ∣ x

Proof state:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
⊢ ∃ r_1, ε = r_1 * fst r • ε

Tactic:
have hr : fst r ≠ 0 := by
  contrapose! hx0
  simp [hx0]

Result:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
hr : fst r ≠ 0
⊢ ∃ r_1, ε = r_1 * fst r • ε

Proof state:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : ε ∣ x
⊢ x ∈ I

Tactic:
obtain ⟨p, rfl⟩ := hx

Result:
case refine_2.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p : K[ε]
⊢ ε * p ∈ I

Proof state:
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, ε = r * x

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

Result:
case intro
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, ε = r_1 * (ε * r)

Proof state:
case inl
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

Result:
no goals

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x

Tactic:
intro x hxI hx0

Result:
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, ε = r * x

Proof state:
case refine_2.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
⊢ ε * p ∈ I

Tactic:
obtain ⟨r, hr⟩ := hd' _ hyI hy0

Result:
case refine_2.intro.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ ε * p ∈ I

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
⊢ I = Ideal.span {ε} ∨ I = ⊤

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

Result:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
⊢ I = Ideal.span {ε}

Proof state:
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 = fst r • ε

Tactic:
ext <;> simp

Result:
no goals

Proof state:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : x ∈ I
⊢ ε ∣ x

Tactic:
simp_rw [hd _ hx]

Result:
no goals