-- Mathlib/Data/Ordmap/Ordset.lean
theorem balanceL_eq_balance {l x r} (sl : Sized l) (sr : Sized r) (H1 : size l = 0 → size r ≤ 1)
    (H2 : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l) :
    @balanceL α l x r = balance l x r

Proof state:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Tactic:
replace H2 : ¬rs > delta * ls := not_lt_of_le (H2 sl.pos sr.pos)

Result:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Proof state:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (node rs nil rx nil) = nil.balance x (node rs nil rx nil)

Tactic:
rw [sr.eq_node']

Result:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
H1 : l.size = 0 → r.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
⊢ l.balanceL x r = l.balance x r

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r

Result:
case nil
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
sr : nil.Sized
H1 : l.size = 0 → nil.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ nil.size → nil.size ≤ delta * l.size
⊢ l.balanceL x nil = l.balance x nil

case node
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
H1 : l.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * l.size
⊢ l.balanceL x (node rs rl rx rr) = l.balance x (node rs rl rx rr)

Proof state:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
have := H1 rfl

Result:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : (node rs rl rx rr).size ≤ 1
⊢ rl.size = 0 ∧ rr.size = 0

Proof state:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : (node rs rl rx rr).size ≤ 1
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Result:
no goals

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
H1 : l.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * l.size
⊢ l.balanceL x (node rs rl rx rr) = l.balance x (node rs rl rx rr)

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l

Result:
case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
⊢ nil.balanceL x (node rs rl rx rr) = nil.balance x (node rs rl rx rr)

case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Proof state:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
sr : nil.Sized
H1 : l.size = 0 → nil.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ nil.size → nil.size ≤ delta * l.size
⊢ l.balanceL x nil = l.balance x nil

Tactic:
rfl

Result:
no goals

Proof state:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Tactic:
simp [balanceL, balance, H2]

Result:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l x_2 r l_ih r_ih =>
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l x_2 r l_ih r_ih =>
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)