field_simp for Fin structures

Stream: new members

[Alex Gu]

I'm stuck figuring out how to generalize this simple example from 2 variables to n variables, getting field_simp to work. Any wisdom?

theorem inequality_2 (n : ℕ) (a : Fin 2 → ℝ) (ha : ∀ i, a i > 0) : ∑ i, √(a i) ^ 2 = ∑ i, a i := by
  simp [Fin.sum_univ_two]
  have h0 : a 0 > 0 := by exact ha 0
  have h1 : a 1 > 0 := by exact ha 1
  field_simp

theorem inequality_n (n : ℕ) (a : Fin n → ℝ) (ha : ∀ i, a i > 0) : ∑ i, √(a i) ^ 2 = ∑ i, a i := by
  ???

[Eric Wieser]

Does congr! help?

[Alex Gu]

Yeah, I can do it with congr!, but was wondering if there's a way to add some hypothesis to get field_simp to work here as well

[Alex Gu]

Completely separate, but is there a way to do congr! and have the ghost variable x✝ : Fin n be replaced with a concrete value?

[Eric Wieser]

  congr! with i
  have := ha i
  field_simp

[Alex Gu]

Is it possible without congr!? Similar to the version with 2 variables?

[Heather Macbeth]

Just a note that field_simp is a bit misleading here -- its job is to clear denominators to fractions and that's not actually what you're doing. A lighter-weight version of the field_simp line is simp (discharger := positivity).