-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_nat (a b : ℕ) : ∗a + ∗b = ∗(a ^^^ b)

Proof state:
case a.h.intro
a b : ℕ
hc : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)
c : ℕ
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
⊢ False

Tactic:
rw [hc', OrderIso.lt_iff_lt, Nat.cast_lt] at hc

Result:
case a.h.intro
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
⊢ False

Proof state:
case a.h₂
a b : ℕ
c : Nimber
hc : c < Ordinal.toNimber ↑b
⊢ Ordinal.toNimber ↑a + c ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
obtain ⟨c, rfl⟩ := eq_nat_of_le_nat hc.le

Result:
case a.h₂.intro
a b c : ℕ
hc : Ordinal.toNimber ↑c < Ordinal.toNimber ↑b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h₂.intro
a b c : ℕ
hc : Ordinal.toNimber ↑c < Ordinal.toNimber ↑b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
rw [OrderIso.lt_iff_lt] at hc

Result:
case a.h₂.intro
a b c : ℕ
hc : ↑c < ↑b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h₁
a b : ℕ
⊢ ∀ a' < Ordinal.toNimber ↑a, a' + Ordinal.toNimber ↑b ≠ Ordinal.toNimber ↑(a ^^^ b)

case a.h₂
a b : ℕ
⊢ ∀ b' < Ordinal.toNimber ↑b, Ordinal.toNimber ↑a + b' ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
all_goals
  intro c hc
  obtain ⟨c, rfl⟩ := eq_nat_of_le_nat hc.le
  rw [OrderIso.lt_iff_lt] at hc
  replace hc := Nat.cast_lt.1 hc
  rw [add_nat]
  simpa using hc.ne

Result:
no goals

Proof state:
case a.h.intro.inl
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ b < a
⊢ c ^^^ b = a

Tactic:
simpa [Nat.xor_comm, Nat.xor_cancel_left, ← hc'] using add_nat (c ^^^ b) b

Result:
no goals

Proof state:
case a
a b : ℕ
⊢ Ordinal.toNimber ↑(a ^^^ b) ≤ Ordinal.toNimber ↑a + Ordinal.toNimber ↑b

Tactic:
apply le_of_not_lt

Result:
case a.h
a b : ℕ
⊢ ¬Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h₂.intro
a b c : ℕ
hc : ↑c < ↑b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
replace hc := Nat.cast_lt.1 hc

Result:
case a.h₂.intro
a b c : ℕ
hc : c < b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h.intro.inr
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ a < b
⊢ False

Tactic:
apply h.ne

Result:
case a.h.intro.inr
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ a < b
⊢ c ^^^ a = b

Proof state:
case a.h.intro
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
⊢ False

Tactic:
obtain h | h := Nat.lt_xor_cases hc

Result:
case a.h.intro.inl
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ b < a
⊢ False

case a.h.intro.inr
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ a < b
⊢ False

Proof state:
case a.h
a b : ℕ
hc : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)
⊢ False

Tactic:
obtain ⟨c, hc'⟩ := eq_nat_of_le_nat hc.le

Result:
case a.h.intro
a b : ℕ
hc : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)
c : ℕ
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
⊢ False

Proof state:
case a.h.intro.inl
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ b < a
⊢ False

Tactic:
apply h.ne

Result:
case a.h.intro.inl
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ b < a
⊢ c ^^^ b = a

Proof state:
case a
a b : ℕ
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑b ≤ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
apply add_le_of_forall_ne

Result:
case a.h₁
a b : ℕ
⊢ ∀ a' < Ordinal.toNimber ↑a, a' + Ordinal.toNimber ↑b ≠ Ordinal.toNimber ↑(a ^^^ b)

case a.h₂
a b : ℕ
⊢ ∀ b' < Ordinal.toNimber ↑b, Ordinal.toNimber ↑a + b' ≠ Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h
a b : ℕ
⊢ ¬Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)

Tactic:
intro hc

Result:
case a.h
a b : ℕ
hc : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b < Ordinal.toNimber ↑(a ^^^ b)
⊢ False

Proof state:
case a.h.intro.inr
a b c : ℕ
hc : c < a ^^^ b
hc' : Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑c
h : c ^^^ a < b
⊢ c ^^^ a = b

Tactic:
simpa [Nat.xor_comm, Nat.xor_cancel_left, ← hc'] using add_nat a (c ^^^ a)

Result:
no goals

Proof state:
case a.h₂.intro
a b c : ℕ
hc : c < b
⊢ Ordinal.toNimber ↑(a ^^^ c) ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
simpa using hc.ne

Result:
no goals

Proof state:
a b : ℕ
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑(a ^^^ b)

Tactic:
apply le_antisymm

Result:
case a
a b : ℕ
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑b ≤ Ordinal.toNimber ↑(a ^^^ b)

case a
a b : ℕ
⊢ Ordinal.toNimber ↑(a ^^^ b) ≤ Ordinal.toNimber ↑a + Ordinal.toNimber ↑b

Proof state:
case a.h₂.intro
a b c : ℕ
hc : c < b
⊢ Ordinal.toNimber ↑a + Ordinal.toNimber ↑c ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
rw [add_nat]

Result:
case a.h₂.intro
a b c : ℕ
hc : c < b
⊢ Ordinal.toNimber ↑(a ^^^ c) ≠ Ordinal.toNimber ↑(a ^^^ b)

Proof state:
case a.h₂
a b : ℕ
⊢ ∀ b' < Ordinal.toNimber ↑b, Ordinal.toNimber ↑a + b' ≠ Ordinal.toNimber ↑(a ^^^ b)

Tactic:
intro c hc

Result:
case a.h₂
a b : ℕ
c : Nimber
hc : c < Ordinal.toNimber ↑b
⊢ Ordinal.toNimber ↑a + c ≠ Ordinal.toNimber ↑(a ^^^ b)