no goals
α : Type u_1
⊢ 0 < 1
decide
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ size a + 1 + size b < 2 ^ max (depth a) (depth b) + 2 ^ max (depth a) (depth b)
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ size (node c✝ a v✝ b) < 2 ^ depth (node c✝ a v✝ b)
rw [size, depth, Nat.add_right_comm, Nat.pow_succ, Nat.mul_two]
case refine_1
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ depth a ≤ 2 ^ max (depth a) (depth b)

case refine_2
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ depth b ≤ 2 ^ max (depth a) (depth b)
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ size a + 1 + size b < 2 ^ max (depth a) (depth b) + 2 ^ max (depth a) (depth b)
refine Nat.add_le_add
  (Nat.lt_of_lt_of_le a.size_lt_depth ?_) (Nat.lt_of_lt_of_le b.size_lt_depth ?_)
no goals
case refine_1
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ depth a ≤ 2 ^ max (depth a) (depth b)
exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_left ..)
no goals
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 > 0
decide
no goals
case refine_2
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ depth b ≤ 2 ^ max (depth a) (depth b)
exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_right ..)
no goals
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 > 0
decide