-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
refine_2 refine_2₁ refine_2₂ refine_2₃ : (¬∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → False
refine_2₄ refine_2₅ refine_2₆ refine_2₇ refine_2₈ refine_2₉ refine_2₁₀ :
  ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)), False
refine_2₁₁ : ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)), False
refine_2₁₂ :
  ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)),
    let f : α → ℂ := fun (b : α) ↦ if a = b then 1 else 0;
    ∀
      (h₀ :
        (∑ i : AddChar α ℂ,
              HSMul.hSMul (α := ℂ) (β := α → ℂ)
                ((((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) f : AddChar α ℂ →₀ ℂ) :
                      (a : AddChar α ℂ) → ℂ)
                    i :
                  ℂ)
                ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) i : α → ℂ))
            0 =
          f 0),
      False
refine_2₁₃ :
  ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)),
    let f : α → ℂ := fun (b : α) ↦ if a = b then 1 else 0;
    ∀
      (h₀ :
        (∑ i : AddChar α ℂ,
              HSMul.hSMul (α := ℂ) (β := α → ℂ)
                ((((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) f : AddChar α ℂ →₀ ℂ) :
                      (a : AddChar α ℂ) → ℂ)
                    i :
                  ℂ)
                ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) i : α → ℂ))
            0 =
          f 0)
      (h₁ :
        (∑ i : AddChar α ℂ,
              HSMul.hSMul (α := ℂ) (β := α → ℂ)
                ((((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) f : AddChar α ℂ →₀ ℂ) :
                      (a : AddChar α ℂ) → ℂ)
                    i :
                  ℂ)
                ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) i : α → ℂ))
            a =
          f a),
      False
refine_2₁₄ :
  ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ))
    (h₀ :
      Eq (α := ℂ)
        (∑ x : AddChar α ℂ,
          (((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) fun (b : α) ↦ if a = b then 1 else 0 :
                AddChar α ℂ →₀ ℂ) :
              (a : AddChar α ℂ) → ℂ)
            x)
        0)
    (h₁ :
      Eq (α := ℂ)
        (∑ x : AddChar α ℂ,
          (((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) fun (b : α) ↦ if a = b then 1 else 0 :
                AddChar α ℂ →₀ ℂ) :
              (a : AddChar α ℂ) → ℂ)
            x)
        1),
    False
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)

Tactic:
classical
  by_contra! h
  let f : α → ℂ := fun b ↦ if a = b then 1 else 0
  have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
  have h₁ := congr_fun ((complexBasis α).sum_repr f) a
  simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
    map_zero_eq_one, if_pos rfl, if_neg ha, f] at h₀ h₁
  exact one_ne_zero (h₁.symm.trans h₀)

Premises used: AddChar.map_zero_eq_one, if_pos, smul_eq_mul, mul_one, AddChar.complexBasis_apply, Fintype.sum_apply, if_neg, rfl, Pi.smul_apply