-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
case case₁ :
  ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.eq, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
case₂ case₃ :
  ∀ (IHe : e₁ = e₂),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
case₄ :
  ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).NF),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_2)
case₅ case₆ :
  ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).NF),
    (Ordering.eq.then ((cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares
      (namedPattern o₁ (e₁.oadd n₁ a₁) h) (namedPattern o₂ (e₁.oadd n₂ a₂) h_2)
case₇ :
  ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).NF)
    (nh :
      (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt ∨
        (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_2)
⊢ ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.eq, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
have eq : ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).NF)
  (nh :
    (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.eq ∨
      (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq),
  (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_2)
Tactic: case eq =>
      intro IHe; dsimp at IHe; subst IHe
      unfold _root_.cmp; cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂ <;>
      rw [cmpUsing, ite_eq_iff, not_lt] at nh
      case lt =>
        rcases nh with nh | nh
        · exact oadd_lt_oadd_2 h₁ nh.left
        · rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction
      case gt =>
        rcases nh with nh | nh
        · cases nh; contradiction
        · obtain ⟨_, nh⟩ := nh
          rw [ite_eq_iff] at nh; rcases nh with nh | nh
          · exact oadd_lt_oadd_2 h₂ nh.left
          · cases nh; contradiction
      rcases nh with nh | nh
      · cases nh; contradiction
      obtain ⟨nhl, nhr⟩ := nh
      rw [ite_eq_iff] at nhr
      rcases nhr with nhr | nhr
      · cases nhr; contradiction
      obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)
      have IHa := @cmp_compares _ _ h₁.snd h₂.snd
      revert IHa; cases cmp a₁ a₂ <;> intro IHa <;> dsimp at IHa
      case lt => exact oadd_lt_oadd_3 IHa
      case gt => exact oadd_lt_oadd_3 IHa
      subst IHa; exact rfl
Cleared hypotheses: e₂, h_1, h₂