-- Mathlib/RingTheory/DualNumber.lean
lemma exists_mul_left_or_mul_right [DivisionRing K] (a b : K[ε]) :
    ∃ c, a * c = b ∨ b * c = a

Proof state:
case inr.inr.intro.intro.inl
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ fst y * fst ε = fst x

Tactic:
simp [hx]

Result:
no goals

Proof state:
case inr.inr.intro.intro
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
rcases eq_or_ne (fst x) 0 with hx|hx

Result:
case inr.inr.intro.intro.inl
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

case inr.inr.intro.intro.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Proof state:
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
this : ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ c, ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
simpa [TrivSqZeroExt.ext_iff] using this

Result:
no goals

Proof state:
case inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rcases isUnit_or_isNilpotent b with hb|hb

Result:
case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ ∃ c, a * c = b ∨ b * c = a

case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ↑a * (↑a⁻¹ * b) = b ∨ b * (↑a⁻¹ * b) = ↑a

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rw [isNilpotent_iff_eps_dvd] at ha hb

Result:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rcases isUnit_or_isNilpotent a with ha|ha

Result:
case inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ ∃ c, a * c = b ∨ b * c = a

case inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
case inr.inr.intro.intro.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩

Result:
case inr.inr.intro.intro.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ fst x * (inl ((fst x)⁻¹ * fst y)).fst = fst y ∨ fst y * (inl ((fst x)⁻¹ * fst y)).fst = fst x

Proof state:
case inr.inl.intro
K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ ∃ c, a * c = ↑b ∨ ↑b * c = a

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

Result:
no goals

Proof state:
case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
lift b to K[ε]ˣ using hb

Result:
case inr.inl.intro
K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ ∃ c, a * c = ↑b ∨ ↑b * c = a

Proof state:
case inr.inr.intro.intro.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ fst x * (inl ((fst x)⁻¹ * fst y)).fst = fst y ∨ fst y * (inl ((fst x)⁻¹ * fst y)).fst = fst x

Tactic:
simp [← inl_mul, ← mul_assoc, mul_inv_cancel₀ hx]

Result:
no goals

Proof state:
case inr.inr.intro
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
hb : ε ∣ b
x : K[ε]
⊢ ∃ c, ε * x * c = b ∨ b * c = ε * x

Tactic:
obtain ⟨y, rfl⟩ := hb

Result:
case inr.inr.intro.intro
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
⊢ ∃ c, ε * x * c = ε * y ∨ ε * y * c = ε * x

Proof state:
case inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
lift a to K[ε]ˣ using ha

Result:
case inl.intro
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ∃ c, ↑a * c = b ∨ b * c = ↑a

Proof state:
case inr.inr.intro.intro.inl
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
refine ⟨ε, Or.inr ?_⟩

Result:
case inr.inr.intro.intro.inl
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ fst y * fst ε = fst x

Proof state:
case inl.intro
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ∃ c, ↑a * c = b ∨ b * c = ↑a

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

Result:
no goals

Proof state:
K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ a * (↑b⁻¹ * a) = ↑b ∨ ↑b * (↑b⁻¹ * a) = a

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.intro.intro
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
⊢ ∃ c, ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
suffices ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x by
  simpa [TrivSqZeroExt.ext_iff] using this

Result:
case inr.inr.intro.intro
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
⊢ ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Proof state:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨x, rfl⟩ := ha

Result:
case inr.inr.intro
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
hb : ε ∣ b
x : K[ε]
⊢ ∃ c, ε * x * c = b ∨ b * c = ε * x