-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem eq_of_cmp_eq : ∀ {o₁ o₂}, cmp o₁ o₂ = Ordering.eq → o₁ = o₂
  | 0, 0, _ => rfl
  | oadd e n a, 0, h => by injection h
  | 0, oadd e n a, h => by injection h
  | oadd e₁ n₁ a₁, oadd e₂ n₂ a₂, h => by
    revert h; simp only [cmp]
    cases h₁ : cmp e₁ e₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h₁
    revert h; cases h₂ : _root_.cmp (n₁ : ℕ) n₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h
    rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂
    obtain rfl := Subtype.eq h₂
    simp

Proof state:
case eq.eq
e₁ a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
h₂ : ↑n₂ = ↑n₂
⊢ e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁

Tactic:
simp

Result:
no goals

Proof state:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
revert h

Result:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Proof state:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
obtain rfl := eq_of_cmp_eq h₁

Result:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Proof state:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
simp only [cmp]

Result:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Proof state:
case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.gt
h : Ordering.gt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h

Result:
no goals

Proof state:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ↑n₂ = ↑n₁
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
obtain rfl := Subtype.eq h₂

Result:
case eq.eq
e₁ a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
h₂ : ↑n₂ = ↑n₂
⊢ e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁

Proof state:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂

Result:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ↑n₂ = ↑n₁
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Proof state:
e : ONote
n : ℕ+
a : ONote
h : cmp 0 (e.oadd n a) = Ordering.eq
⊢ 0 = e.oadd n a

Tactic:
injection h

Result:
no goals

Proof state:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h₂ : _root_.cmp (n₁ : ℕ) n₂ <;> intro h <;> try cases h

Result:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Proof state:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h₁ : cmp e₁ e₂ <;> intro h <;> try cases h

Result:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Proof state:
case eq.gt
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.gt
h : Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h

Result:
no goals

Proof state:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
revert h

Result:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Proof state:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).cmp 0 = Ordering.eq
⊢ e.oadd n a = 0

Tactic:
injection h

Result:
no goals

Proof state:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
obtain rfl := eq_of_cmp_eq h

Result:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁