AddChar.expect_iInf_ker_eq_zero_of_not_mem_closure

lemma expect_iInf_ker_eq_zero_of_not_mem_closure (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker)    (hψ : ψ ∉ AddSubgroup.closure Δ) : 𝔼 x ∈ Set.toFinset V, ψ x = 0 := by  obtain ⟨x, hxΔ, hxψ⟩ : ∃ x, (∀ γ ∈ Δ, γ x = 1) ∧ ψ x ≠ 1 := by    simpa [AddChar.mem_closure_iff] using hψ  let ψV : AddChar V ℂ := ψ.compAddMonoidHom V.subtype  calc    𝔼 x ∈ Set.toFinset V, ψ x      = (∑ x ∈ Set.toFinset V, ψ x) / #(Set.toFinset V) := by rw [Finset.expect_eq_sum_div_card]    _ = (∑ x, ψV x) / Fintype.card V := by      have hsum : ∑ x ∈ Set.toFinset (V : Set G), ψ x = ∑ x : V, ψ x :=        Finset.sum_subtype (Set.toFinset (V : Set G)) (by intro x; simp) fun x ↦ ψ x      simp [hsum, ψV]    _ = 0 := by      simp only [div_eq_zero_iff, sum_eq_zero_iff_ne_zero, ne_eq, Nat.cast_eq_zero,        Fintype.card_ne_zero, or_false]      intro hzero      apply hxψ      simpa [ψV] using DFunLike.congr_fun hzero ⟨x, by simpa [hV] using hxΔ⟩