-- 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 : ¬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)

Tactic:
split_ifs <;> simp [add_comm]

Result:
no goals

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

Tactic:
cases sr.2.2.size_eq_zero.1 this.2

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 (node rs nil rx nil) = nil.balance x (node rs nil rx nil)

Proof state:
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
this : rl.size = 0 ∧ rr.size = 0
⊢ nil.balanceL x (node rs rl rx rr) = nil.balance x (node rs rl rx rr)

Tactic:
cases sr.2.1.size_eq_zero.1 this.1

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

Proof state:
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)

Tactic:
have : size rl = 0 ∧ size rr = 0 := by
  have := H1 rfl
  rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

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
this : rl.size = 0 ∧ rr.size = 0
⊢ nil.balanceL x (node rs rl rx rr) = nil.balance x (node rs rl rx rr)