rewriting through finset sum

Stream: Is there code for X?

[Dhyan Aranha]

Hi, I would like to prove the following lemma

lemma blah  (n : ℕ ) (hn : n > 0) (f : Fin n → Type) [∀ j, Fintype (f j)] (hf1 : Fintype.card (f ⟨0, Nat.zero_lt_of_lt hn⟩) = 1)
(hf2 : ∀ j : Fin n, j ≠ ⟨0, Nat.zero_lt_of_lt hn⟩ →  Fintype.card (f j) = 2) : ∑ j : Fin n , Fintype.card (f j) = 2* n -1 := by sorry

In my mind the proof should be just rewriting the terms in the summation via the hypothesis hf1 and hf2 and then doing maybe doing ring_nf. But I get stuck really quickly when I try to do this..Any help would be great!

[Bhavik Mehta]

import Mathlib

lemma blah (n : ℕ) (hn : n > 0) (f : Fin n → Type) [∀ j, Fintype (f j)]
    (hf1 : Fintype.card (f ⟨0, Nat.zero_lt_of_lt hn⟩) = 1)
    (hf2 : ∀ j : Fin n, j ≠ ⟨0, Nat.zero_lt_of_lt hn⟩ →  Fintype.card (f j) = 2) :
    ∑ j : Fin n, Fintype.card (f j) = 2 * n - 1 := by
  cases n with
  | zero => simp at hn
  | succ n =>
      replace hf1 : Fintype.card (f 0) = 1 := hf1
      replace hf2 : ∀ j : Fin n, Fintype.card (f j.succ) = 2 := by simp [hf2, Fin.ext_iff]
      simp only [Fin.sum_univ_succ, hf1, hf2, Finset.sum_const, Finset.card_univ,
        Fintype.card_fin, smul_eq_mul]
      omega

[Dhyan Aranha]

Bhavik Mehta said:

import Mathlib

lemma blah (n : ℕ) (hn : n > 0) (f : Fin n → Type) [∀ j, Fintype (f j)]
    (hf1 : Fintype.card (f ⟨0, Nat.zero_lt_of_lt hn⟩) = 1)
    (hf2 : ∀ j : Fin n, j ≠ ⟨0, Nat.zero_lt_of_lt hn⟩ →  Fintype.card (f j) = 2) :
    ∑ j : Fin n, Fintype.card (f j) = 2 * n - 1 := by
  cases n with
  | zero => simp at hn
  | succ n =>
      replace hf1 : Fintype.card (f 0) = 1 := hf1
      replace hf2 : ∀ j : Fin n, Fintype.card (f j.succ) = 2 := by simp [hf2, Fin.ext_iff]
      simp only [Fin.sum_univ_succ, hf1, hf2, Finset.sum_const, Finset.card_univ,
        Fintype.card_fin, smul_eq_mul]
      omega

Thanks!