-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) ↔ a ≠ 0

Tactic:
refine ⟨?_, fun ha ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0

case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
⊢ ∃ ψ, ψ a ≠ 1

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
⊢ False

Tactic:
let f : α → ℂ := fun b ↦ if a = b then 1 else 0

Result:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
⊢ False

Tactic:
have h₁ := congr_fun ((complexBasis α).sum_repr f) a

Result:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
h₁ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) a = f a
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0

Tactic:
rintro ⟨ψ, hψ⟩ rfl

Result:
case refine_1.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
hψ : ψ 0 ≠ 1
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
⊢ ∃ ψ, ψ a ≠ 1

Tactic:
by_contra! h

Result:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
⊢ False

Tactic:
have h₀ := congr_fun ((complexBasis α).sum_repr f) 0

Result:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
⊢ ∃ ψ, ψ 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₀)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
h₁ : (∑ i : AddChar α ℂ, ((complexBasis α).repr f) i • (complexBasis α) i) a = f a
⊢ False

Tactic:
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₁

Result:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : ∑ x : AddChar α ℂ, ((complexBasis α).repr fun b => if a = b then 1 else 0) x = 0
h₁ : ∑ x : AddChar α ℂ, ((complexBasis α).repr fun b => if a = b then 1 else 0) x = 1
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b => if a = b then 1 else 0
h₀ : ∑ x : AddChar α ℂ, ((complexBasis α).repr fun b => if a = b then 1 else 0) x = 0
h₁ : ∑ x : AddChar α ℂ, ((complexBasis α).repr fun b => if a = b then 1 else 0) x = 1
⊢ False

Tactic:
exact one_ne_zero (h₁.symm.trans h₀)

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
hψ : ψ 0 ≠ 1
⊢ False

Tactic:
exact hψ ψ.map_zero_eq_one

Result:
no goals