α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised (size r₁) (size r₂)
⊢ Raised (size l + size r₁ + 1) (size l + size r₂ + 1)
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised (size r₁) (size r₂)
⊢ Raised (size (node' l x₁ r₁)) (size (node' l x₂ r₂))
rw [node', size, size]
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised (size r₁) m
⊢ Raised (size l + size r₁ + 1) (size l + m + 1)
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised (size r₁) (size r₂)
⊢ Raised (size l + size r₁ + 1) (size l + size r₂ + 1)
generalize size r₂ = m at H ⊢
case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (size l + size r₁ + 1) (size l + size r₁ + 1)

case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (size l + size r₁ + 1) (size l + (size r₁ + 1) + 1)
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised (size r₁) m
⊢ Raised (size l + size r₁ + 1) (size l + m + 1)
rcases H with (rfl | rfl)
no goals
case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (size l + size r₁ + 1) (size l + size r₁ + 1)
exact Or.inl rfl
no goals
case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (size l + size r₁ + 1) (size l + (size r₁ + 1) + 1)
exact Or.inr rfl