-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
No : (a0.oadd n a').NF
zero :
  let R' := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr;
  (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑0 : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (Order.succ (↑0 : Ordinal.{0}))
succ :
  ∀ (k : ℕ)
    (IH :
      let R' := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr;
      (k ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑k : Ordinal.{0}))) ∧
        HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) *
              (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
            R' =
          HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
            (Order.succ (↑k : Ordinal.{0}))),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr;
    (k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑(k + 1) : Ordinal.{0}))) ∧
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑(k + 1) : Ordinal.{0}) *
            (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
          R' =
        HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
          (Order.succ (↑(k + 1) : Ordinal.{0}))
⊢ (k ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (Order.succ (↑k : Ordinal.{0}))

Tactic:
induction k with
  | zero => cases m <;> simp [R', opowAux]
  | succ k IH =>
  -- rename R => R'
  let R := repr (opowAux 0 a0 (oadd a0 n a' * ofNat m) k m)
  let ω0 := ω ^ repr a0
  let α' := ω0 * n + repr a'
  change (k ≠ 0 → R < (ω0 ^ succ (k : Ordinal))) ∧ (ω0 ^ (k : Ordinal)) * α' + R
    = (α' + m) ^ (succ ↑k : Ordinal) at IH
  have RR : R' = ω0 ^ (k : Ordinal) * (α' * m) + R := by
    by_cases h : m = 0
    · simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr, mul_zero,
        ONote.opowAux, add_zero]
    · simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux,
        ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add]
  have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
  have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
  have Rl : R < ω ^ (repr a0 * succ ↑k) := by
    by_cases k0 : k = 0
    · simp only [k0, Nat.cast_zero, succ_eq_add_one, _root_.zero_add, mul_one, R]
      refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))
      rcases m with - | m
      · simp [opowAux, omega0_pos]
      · simpa [opowAux] using natCast_lt_omega0 (m + 1)
    · rw [opow_mul]
      exact IH.1 k0
  refine ⟨fun _ => ?_, ?_⟩
  · rw [RR, ← opow_mul _ _ (succ k.succ)]
    have e0 := pos_iff_ne_zero.2 e0
    have rr0 : 0 < repr a0 + repr a0 := lt_of_lt_of_le e0 le_add_self
    apply isPrincipal_add_omega0_opow
    · simp only [Nat.cast_add_one, opow_add_one, opow_mul, opow_succ, mul_assoc]
      gcongr ?_ * ?_
      rw [← Ordinal.opow_add]
      have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
      · exact mul_lt_omega0_opow rr0 this (natCast_lt_omega0 _)
      · simpa using (add_lt_add_iff_left (repr a0)).2 e0
    · exact
        lt_of_lt_of_le Rl
          (opow_le_opow_right omega0_pos <|
            mul_le_mul_right (succ_le_succ_iff.2 (Nat.cast_le.2 (le_of_lt k.lt_succ_self))) _)
  calc
    (ω0 ^ (k.succ : Ordinal)) * α' + R'
    _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := by
        rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
    _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_
    _ = (α' + m) ^ succ (k.succ : Ordinal) := by
        rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
  congr 1
  · have αd : ω ∣ α' :=
      dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
    have α0 : ¬IsMin α' := by
      rw [isMin_iff_eq_bot]
      exact α0.ne'
    rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ,
      add_mul_of_isSuccLimit _ ⟨α0, isSuccPrelimit_iff_omega0_dvd.2 αd⟩, mul_assoc,
      @mul_omega0_dvd n (Nat.cast_pos'.2 n.pos) (natCast_lt_omega0 _) _ αd]
    apply @add_of_omega0_opow_le _ (repr a0 * succ ↑k)
    · refine isPrincipal_add_omega0_opow _ ?_ Rl
      rw [opow_mul, opow_succ]
      gcongr
      exact No.snd'.repr_lt
    · have := mul_le_mul_right (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))
      rw [opow_mul]
      simpa
  · cases m
    · have : R = 0 := by cases k <;> simp [R, opowAux]
      simp [this]
    · rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]
      apply add_of_omega0_opow_le Rl
      rw [opow_mul, opow_succ]
      gcongr
      simpa [repr] using omega0_le_oadd a0 n a'

Premises used: Ordinal.opow_mul, Iff.mpr, Order.succ, Order.succ_eq_add_one, Ordinal.opow_add, add_assoc, mul_assoc, Ordinal.add_of_omega0_opow_le, ONote.zero, ONote.omega0_le_oadd, Nat.cast, ONote.repr, Ordinal.opow_add_one, Ordinal.add_mul_succ, Ordinal.opow_succ, ONote.opowAux, Nat.cast_add_one, Ordinal.isPrincipal_add_omega0_opow, Nat.succ, ONote.NF.snd', add_lt_add_iff_left, ONote.NFBelow.repr_lt