case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup' (Finset.range (Nat.zero + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.zero + 1)) f

case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
induction' n with n ih
no goals
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup' (Finset.range (Nat.zero + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.zero + 1)) f
simp
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ 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)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
dsimp [partialSups] at ih⊢
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (insert (Nat.succ n) (Finset.range (Nat.succ n)))
      (_ : Finset.Nonempty (insert (Nat.succ n) (Finset.range (Nat.succ n)))) fun x => f x
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ 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)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
simp_rw [@Finset.range_succ n.succ]
no goals
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (insert (Nat.succ n) (Finset.range (Nat.succ n)))
      (_ : Finset.Nonempty (insert (Nat.succ n) (Finset.range (Nat.succ n)))) fun x => f x
rw [ih, Finset.sup'_insert, sup_comm]