Freiman repeated-three proof: equal child widths

import Definitions.Def_Freiman_lowerJData
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push
import Mathlib.Tactic.FinCases

open Freiman

theorem Freiman.lowerJ_equal_child_widths (hw : ∀ w : List ℕ+, lowerWidth w = (lowerBeta-lowerAlpha)/((((lowerCD w).1:ℝ)*lowerAlpha+(lowerCD w).2)*(((lowerCD w).1:ℝ)*lowerBeta+(lowerCD w).2))) (hc : (1/4:ℝ) < lowerAlpha ∧ lowerAlpha < (27/100:ℝ) ∧ (3/4:ℝ) < lowerBeta ∧ lowerBeta < (4/5:ℝ) ∧ (13243/18000:ℝ)<1 ∧ (739328/796875:ℝ)<1) (p : LowerPair) (ha : lowerAdmissible p) (hp : ¬ lowerMixed p) (hl : lowerEnds p.1 [3]) (hr : lowerEnds p.2 [3]) (hb : lowerParameterBox p) (hwide : lowerWidth p.2 ≤ lowerWidth p.1) (hratio : lowerWidth p.1 < (19/5:ℝ)*lowerWidth p.2) : lowerWidth ((lowerNormalize p).1++[2]) < lowerWidth (lowerNormalize p).2 ∧ lowerWidth ((lowerNormalize p).1++[1,1]) < lowerWidth (lowerNormalize p).2 := by
  sorry