-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → split o = (scale 1 o', m)
  | 0, o', m, _, p => by injection p; substs o' m; rfl
  | oadd e n a, o', m, h, p => by
    by_cases e0 : e = 0 <;> simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢
    · rcases p with ⟨rfl, rfl⟩
      exact ⟨rfl, rfl⟩
    · revert p
      rcases h' : split' a with ⟨a', m'⟩
      haveI := h.fst
      haveI := h.snd
      simp only [split_eq_scale_split' h', and_imp]
      have : 1 + (e - 1) = e

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
haveI := h.snd

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Proof state:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ 0 = scale 1 o' ∧ ↑n = m

Tactic:
rcases p with ⟨rfl, rfl⟩

Result:
case pos.intro
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ 0 = scale 1 0 ∧ ↑n = ↑n

Proof state:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e.repr - 1) = e.repr

Tactic:
have := mt repr_inj.1 e0

Result:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : ¬e.repr = repr 0
⊢ 1 + (e.repr - 1) = e.repr

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Tactic:
have : 1 + (e - 1) = e := by
  refine repr_inj.1 ?_
  simp only [repr_add, repr_one, Nat.cast_one, repr_sub]
  have := mt repr_inj.1 e0
  exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Proof state:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
revert p

Result:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Proof state:
case neg.mk
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
⊢ e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'

Tactic:
simp [scale, this]

Result:
no goals

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Tactic:
intros

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Proof state:
x✝ : NF 0
⊢ split 0 = (scale 1 0, 0)

Tactic:
rfl

Result:
no goals

Proof state:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ split 0 = (scale 1 o', m)

Tactic:
substs o' m

Result:
x✝ : NF 0
⊢ split 0 = (scale 1 0, 0)

Proof state:
case pos.intro
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ 0 = scale 1 0 ∧ ↑n = ↑n

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
haveI := h.fst

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Proof state:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e - 1) = e

Tactic:
refine repr_inj.1 ?_

Result:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (1 + (e - 1)).repr = e.repr

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
simp only [split_eq_scale_split' h', and_imp]

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Proof state:
o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ split 0 = (scale 1 o', m)

Tactic:
injection p

Result:
o' : ONote
m : ℕ
x✝ : NF 0
fst_eq✝ : 0 = o'
snd_eq✝ : 0 = m
⊢ split 0 = (scale 1 o', m)

Proof state:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
by_cases e0 : e = 0 <;> simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢

Result:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ 0 = scale 1 o' ∧ ↑n = m

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Proof state:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (1 + (e - 1)).repr = e.repr

Tactic:
simp only [repr_add, repr_one, Nat.cast_one, repr_sub]

Result:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e.repr - 1) = e.repr

Proof state:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Tactic:
substs o' m

Result:
case neg.mk
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : 1 + (e - 1) = e
⊢ e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'

Proof state:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
rcases h' : split' a with ⟨a', m'⟩

Result:
case neg.mk
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m