-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_inv_cancel_aux (a : Nimber) :
    (∀ b ∈ invSet a, a * b ≠ 1) ∧ (a ≠ 0 → a * invAux a = 1)

Proof state:
case inl
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
b : Nimber
hb : b ∈ a.invSet
ha : 0 < a
H : 0 * a.invAux = 1 + (a + 0) * b
⊢ False

Tactic:
rw [zero_mul, add_zero, ← add_eq_iff_eq_add, zero_add] at H

Result:
case inl
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
b : Nimber
hb : b ∈ a.invSet
ha : 0 < a
H : a * b = 1
⊢ False

Proof state:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux = 1 + (a + a') * b
hb : b ∈ a.invSet
⊢ False

Tactic:
obtain rfl | ha' := eq_or_ne a' 0

Result:
case inl
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
b : Nimber
hb : b ∈ a.invSet
ha : 0 < a
H : 0 * a.invAux = 1 + (a + 0) * b
⊢ False

case inr
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux = 1 + (a + a') * b
hb : b ∈ a.invSet
ha' : a' ≠ 0
⊢ False

Proof state:
case refine_1
a b : Nimber
hb : b ∈ a.invSet
⊢ a * 0 ≠ 1

Tactic:
rw [mul_zero]

Result:
case refine_1
a b : Nimber
hb : b ∈ a.invSet
⊢ 0 ≠ 1

Proof state:
case refine_2
a b✝ : Nimber
hb✝ : b✝ ∈ a.invSet
a' : Nimber
ha : a' < a
ha' : a' ≠ 0
b : Nimber
hb : a * b ≠ 1
⊢ a * (a'.invAux * (1 + (a + a') * b)) ≠ 1

Tactic:
rw [ne_eq, mul_comm, ← mul_right_inj' ha', ← mul_assoc, ← mul_assoc,
  (mul_inv_cancel_aux a').2 ha', one_mul, mul_one, add_mul, one_mul, ← add_left_inj a',
  add_self, mul_assoc, mul_comm b, add_assoc, add_comm _ a', ← add_assoc, ← mul_one_add,
  ← ne_eq, mul_ne_zero_iff, add_ne_zero_iff, add_ne_zero_iff]

Result:
case refine_2
a b✝ : Nimber
hb✝ : b✝ ∈ a.invSet
a' : Nimber
ha : a' < a
ha' : a' ≠ 0
b : Nimber
hb : a * b ≠ 1
⊢ a ≠ a' ∧ 1 ≠ a * b

Proof state:
case refine_2
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ a ≠ 0 ∧ a.invAux ≠ 0

Tactic:
exact ⟨ha₀, invAux_ne_zero a⟩

Result:
no goals

Proof state:
case inr
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux = 1 + (a + a') * b
hb : b ∈ a.invSet
ha' : a' ≠ 0
⊢ False

Tactic:
rw [← mul_right_inj' (invAux_ne_zero a'), ← mul_assoc, mul_comm _ a',
  (mul_inv_cancel_aux a').2 ha', one_mul] at H

Result:
case inr
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a.invAux = a'.invAux * (1 + (a + a') * b)
hb : b ∈ a.invSet
ha' : a' ≠ 0
⊢ False

Proof state:
a : Nimber
⊢ ∀ b ∈ a.invSet, a * b ≠ 1

Tactic:
refine fun b hb ↦ invSet_recOn a ?_ ?_ b hb

Result:
case refine_1
a b : Nimber
hb : b ∈ a.invSet
⊢ a * 0 ≠ 1

case refine_2
a b : Nimber
hb : b ∈ a.invSet
⊢ ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), a * b ≠ 1 → a * (a'.invAux * (1 + (a + a') * b)) ≠ 1

Proof state:
case inl
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
b : Nimber
hb : b ∈ a.invSet
ha : 0 < a
H : a * b = 1
⊢ False

Tactic:
exact H₁ _ hb H

Result:
no goals

Proof state:
case refine_2
a b : Nimber
hb : b ∈ a.invSet
⊢ ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), a * b ≠ 1 → a * (a'.invAux * (1 + (a + a') * b)) ≠ 1

Tactic:
intro a' ha ha' b hb

Result:
case refine_2
a b✝ : Nimber
hb✝ : b✝ ∈ a.invSet
a' : Nimber
ha : a' < a
ha' : a' ≠ 0
b : Nimber
hb : a * b ≠ 1
⊢ a * (a'.invAux * (1 + (a + a') * b)) ≠ 1

Proof state:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
hb : b < a.invAux
H : a' * a.invAux + a * b + a' * b = 1
⊢ False

Tactic:
replace hb := mem_invSet_of_lt_invAux hb

Result:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux + a * b + a' * b = 1
hb : b ∈ a.invSet
⊢ False

Proof state:
case refine_1
a b : Nimber
hb : b ∈ a.invSet
⊢ 0 ≠ 1

Tactic:
exact zero_ne_one

Result:
no goals

Proof state:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux + a * b + a' * b = 1
hb : b ∈ a.invSet
⊢ False

Tactic:
rw [add_assoc, ← add_mul, ← CharTwo.eq_add_iff_add_eq] at H

Result:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a' * a.invAux = 1 + (a + a') * b
hb : b ∈ a.invSet
⊢ False

Proof state:
case inr
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
H : a.invAux = a'.invAux * (1 + (a + a') * b)
hb : b ∈ a.invSet
ha' : a' ≠ 0
⊢ False

Tactic:
exact invAux_not_mem_invSet a (H ▸ cons_mem_invSet ha' ha hb)

Result:
no goals

Proof state:
case refine_1
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ a * a.invAux ≤ 1

Tactic:
apply mul_le_of_forall_ne fun a' ha b hb H ↦ ?_

Result:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
a' : Nimber
ha : a' < a
b : Nimber
hb : b < a.invAux
H : a' * a.invAux + a * b + a' * b = 1
⊢ False

Proof state:
case refine_2
a b✝ : Nimber
hb✝ : b✝ ∈ a.invSet
a' : Nimber
ha : a' < a
ha' : a' ≠ 0
b : Nimber
hb : a * b ≠ 1
⊢ a ≠ a' ∧ 1 ≠ a * b

Tactic:
exact ⟨ha.ne', hb.symm⟩

Result:
no goals

Proof state:
case refine_2
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ 1 ≤ a * a.invAux

Tactic:
rw [one_le_iff_ne_zero, mul_ne_zero_iff]

Result:
case refine_2
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ a ≠ 0 ∧ a.invAux ≠ 0

Proof state:
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
⊢ (∀ b ∈ a.invSet, a * b ≠ 1) ∧ (a ≠ 0 → a * a.invAux = 1)

Tactic:
refine ⟨H₁, fun ha₀ => le_antisymm ?_ ?_⟩

Result:
case refine_1
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ a * a.invAux ≤ 1

case refine_2
a : Nimber
H₁ : ∀ b ∈ a.invSet, a * b ≠ 1
ha₀ : a ≠ 0
⊢ 1 ≤ a * a.invAux