use of finset.sum_insert

Stream: new members

[Alex Zhang]

import algebra.big_operators.basic
import data.real.basic
import set_theory.cardinal

open_locale big_operators

lemma sum_of_squares_nonneg {ι : Type*} (s : finset ι) (a : ι → ℝ) :
  0 ≤ (∑ i in s, (a i)^2) :=
begin
  classical,
  apply finset.induction_on s ,
  {simp,},
  rintros j s h1 h2,
  have h3 : 0 ≤ ((a j)^2),
  {exact pow_two_nonneg (a j),},
  --have h:=finset.sum_insert h1,
end

I wanted to use finset.sum_insert h1 to close the goal, but have h:=finset.sum_insert h1gives me four new goals.
What can I do next to solve the goal?

[Eric Rodriguez]

just rw it; have is confused about some of the implicit arguments, which could be anything. if you rw, it'll be unified with what's in the goal, and then linarith should probably finish it

[Alex Zhang]

Cool! The goal is sovled. What have gave me confused me at the beginning...

[Alex Zhang]

Could you explain why I need to use classical at the beginning?

[Eric Rodriguez]

classical makes all propositions "have an answer"/be decidable; to us mathematicians, this is self-evident, but as Lean is designed as a programming language it isn't obvious what the decision procedure is, which it needs to "decide" it

[Eric Rodriguez]

in this case, the induction needs a [decidable_eq ι] argument, which you could've used instead