English
If split'(o) = (o', m), then split(o) = (scale(1, o'), m) for NF o and corresponding equality; i.e., splitting after normalizing by scale yields the scaled result.
Русский
Если split'(o) = (o', m), тогда split(o) = (scale(1, o'), m) при NF o; то же верно для соответствующего равенства.
LaTeX
$$$\forall o,o',m\ [\mathrm{NF}\,o]\;\text{split'}(o)=(o',m)\Rightarrow \text{split}(o)=(\mathrm{scale}(1,o'),m).$$$
Lean4
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 := 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
intros
substs o' m
simp [scale, this]
