case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n → f m ≤ a
w : ∀ (m : ℕ), m ≤ Nat.zero → f m ≤ a
⊢ ↑(partialSups f) Nat.zero ≤ a

case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n✝ → f m ≤ a
n : ℕ
ih : (∀ (m : ℕ), m ≤ n → f m ≤ a) → ↑(partialSups f) n ≤ a
w : ∀ (m : ℕ), m ≤ Nat.succ n → f m ≤ a
⊢ ↑(partialSups f) (Nat.succ n) ≤ a
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w : ∀ (m : ℕ), m ≤ n → f m ≤ a
⊢ ↑(partialSups f) n ≤ a
induction' n with n ih
no goals
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n → f m ≤ a
w : ∀ (m : ℕ), m ≤ Nat.zero → f m ≤ a
⊢ ↑(partialSups f) Nat.zero ≤ a
apply w 0 le_rfl
no goals
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n✝ → f m ≤ a
n : ℕ
ih : (∀ (m : ℕ), m ≤ n → f m ≤ a) → ↑(partialSups f) n ≤ a
w : ∀ (m : ℕ), m ≤ Nat.succ n → f m ≤ a
⊢ ↑(partialSups f) (Nat.succ n) ≤ a
exact sup_le (ih fun m p => w m (Nat.le_succ_of_le p)) (w (n + 1) le_rfl)