α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l
α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂
refine' or_iff_not_imp_left.2 fun h => _
α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂
α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l
refine' ⟨_, h₂.resolve_left h⟩
case inl.zero
α : Type ?u.9339
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ Nat.zero
h₂ : l + Nat.zero ≤ 1 ∨ Nat.zero ≤ delta * l
h : ¬l + Nat.zero ≤ 1
⊢ l ≤ delta * Nat.zero

case inl.succ
α : Type ?u.9339
l r₁ : ℕ
H : l + r₁ ≤ 1
n✝ : ℕ
h₁ : r₁ ≤ Nat.succ n✝
h₂ : l + Nat.succ n✝ ≤ 1 ∨ Nat.succ n✝ ≤ delta * l
h : ¬l + Nat.succ n✝ ≤ 1
⊢ l ≤ delta * Nat.succ n✝
case inl
α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
⊢ l ≤ delta * r₂
cases r₂
no goals
case inl.zero
α : Type ?u.9339
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ Nat.zero
h₂ : l + Nat.zero ≤ 1 ∨ Nat.zero ≤ delta * l
h : ¬l + Nat.zero ≤ 1
⊢ l ≤ delta * Nat.zero
cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
no goals
case inl.succ
α : Type ?u.9339
l r₁ : ℕ
H : l + r₁ ≤ 1
n✝ : ℕ
h₁ : r₁ ≤ Nat.succ n✝
h₂ : l + Nat.succ n✝ ≤ 1 ∨ Nat.succ n✝ ≤ delta * l
h : ¬l + Nat.succ n✝ ≤ 1
⊢ l ≤ delta * Nat.succ n✝
exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
no goals
case inr
α : Type ?u.9339
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l
⊢ l ≤ delta * r₂
exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)