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

case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : m ≤ Nat.succ n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ f m ≤ ↑(partialSups f) n
induction' n with n ih
no goals
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h✝ : m ≤ n
h : m ≤ Nat.zero
⊢ f m ≤ ↑(partialSups f) Nat.zero
rw [nonpos_iff_eq_zero.mp h, partialSups_zero]
case succ.refl
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ n : ℕ
h : Nat.succ n ≤ n✝
ih : Nat.succ n ≤ n → f (Nat.succ n) ≤ ↑(partialSups f) n
⊢ f (Nat.succ n) ≤ ↑(partialSups f) (Nat.succ n)

case succ.step
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : Nat.le m n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : m ≤ Nat.succ n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
cases' h with h h
no goals
case succ.refl
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ n : ℕ
h : Nat.succ n ≤ n✝
ih : Nat.succ n ≤ n → f (Nat.succ n) ≤ ↑(partialSups f) n
⊢ f (Nat.succ n) ≤ ↑(partialSups f) (Nat.succ n)
exact le_sup_right
no goals
case succ.step
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : Nat.le m n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
exact (ih h).trans le_sup_left