case zero
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup (Finset.range (Nat.zero + 1)) f

case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) = Finset.sup (Finset.range (Nat.succ n + 1)) f
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
induction' n with n ih
no goals
case zero
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup (Finset.range (Nat.zero + 1)) f
simp
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup (Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) = Finset.sup (Finset.range (Nat.succ n + 1)) f
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) = Finset.sup (Finset.range (Nat.succ n + 1)) f
dsimp [partialSups] at ih⊢
no goals
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup (Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) = Finset.sup (Finset.range (Nat.succ n + 1)) f
rw [Finset.range_succ, Finset.sup_insert, sup_comm, ih]