awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ ZMod n ≃+ AddChar (ZMod n) ℂ
have refine : Bijective (α := ZMod n) (β := AddChar (ZMod n) ℂ)
  (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom circleEquivComplex) (toAddMonoidHom zmodHom)) :
    (a : ZMod n) → AddChar (ZMod n) ℂ)
Tactic: refine AddEquiv.ofBijective
    (circleEquivComplex.toAddMonoidHom.comp <| AddChar.toAddMonoidHom zmodHom) ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ Bijective (α := ZMod n) (β := AddChar (ZMod n) ℂ)
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom circleEquivComplex) (toAddMonoidHom zmodHom)) :
      (a : ZMod n) → AddChar (ZMod n) ℂ)
have rw : Injective (α := ZMod n) (β := AddChar (ZMod n) ℂ)
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom circleEquivComplex) (toAddMonoidHom zmodHom)) :
      (a : ZMod n) → AddChar (ZMod n) ℂ) ∧
  Fintype.card (ZMod n) = Fintype.card (ZMod n)
Tactic: rw [Fintype.bijective_iff_injective_and_card, card_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)
have intro : ∀ (val : Fintype α), Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
val : Fintype α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)
have intro : Fintype.card α = finrank.{0, u_1} ℂ (α → ℂ)
Tactic: rw [card_eq, Module.finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
val : Fintype α
intro : Fintype.card α = finrank.{0, u_1} ℂ (α → ℂ)
⊢ Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)
have intro₁ : Fintype.card α = Fintype.card α
Tactic: rw [card_eq, Module.finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
⊢ Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(complexBasis α) : (a : AddChar α ℂ) → α → ℂ)
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))
have rw : Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(basisOfLinearIndependentOfCardEqFinrank sorry sorry) : (a : AddChar α ℂ) → α → ℂ)
  (DFunLike.coe (β := fun (x : α) ↦ ℂ))
Tactic: rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
rw :
  Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) : (a : AddChar α ℂ) → α → ℂ)
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))
⊢ Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(complexBasis α) : (a : AddChar α ℂ) → α → ℂ)
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))
have rw₁ : Eq.{u_1 + 1} (α := (a : AddChar α ℂ) → α → ℂ) (DFunLike.coe (β := fun (x : α) ↦ ℂ))
  (DFunLike.coe (β := fun (x : α) ↦ ℂ))
Tactic: rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
ψ : AddChar α ℂ
⊢ Eq (α := α → ℂ) ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) ψ : α → ℂ) ((⇑ψ : (a : α) → ℂ) : (a : α) → ℂ)
have rw : Eq (α := α → ℂ) (⇑ψ : (a : α) → ℂ) (⇑ψ : (a : α) → ℂ)
Tactic: rw [coe_complexBasis]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) ↔ a ≠ 0
have refine_1 : (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → a ≠ 0
Tactic: refine ⟨?_, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
refine_1 : (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → a ≠ 0
⊢ (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) ↔ a ≠ 0
have refine_2 : ∀ (ha : a ≠ 0), ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
Tactic: refine ⟨?_, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have refine_2 : ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
f : α → ℂ := fun (b : α) ↦ if a = b then 1 else 0
⊢ False
have h₀ : (∑ i : AddChar α ℂ,
      HSMul.hSMul (α := ℂ) (β := α → ℂ)
        ((((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) f : AddChar α ℂ →₀ ℂ) : (a : AddChar α ℂ) → ℂ)
            i :
          ℂ)
        ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) i : α → ℂ))
    0 =
  f 0
Tactic: have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
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
have h₁ : (∑ i : AddChar α ℂ,
      HSMul.hSMul (α := ℂ) (β := α → ℂ)
        ((((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) f : AddChar α ℂ →₀ ℂ) : (a : AddChar α ℂ) → ℂ)
            i :
          ℂ)
        ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) i : α → ℂ))
    a =
  f a
Tactic: have h₁ := congr_fun ((complexBasis α).sum_repr f) a
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
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
have h₂ : Eq (α := ℂ)
  (∑ x : AddChar α ℂ,
    (((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) fun (b : α) ↦ if a = b then 1 else 0 :
          AddChar α ℂ →₀ ℂ) :
        (a : AddChar α ℂ) → ℂ)
      x)
  0
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₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
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
h₂ :
  Eq (α := ℂ)
    (∑ x : AddChar α ℂ,
      (((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) fun (b : α) ↦ if a = b then 1 else 0 :
            AddChar α ℂ →₀ ℂ) :
          (a : AddChar α ℂ) → ℂ)
        x)
    0
⊢ False
have h₃ : Eq (α := ℂ)
  (∑ x : AddChar α ℂ,
    (((Basis.repr (complexBasis α) : (a : α → ℂ) → AddChar α ℂ →₀ ℂ) fun (b : α) ↦ if a = b then 1 else 0 :
          AddChar α ℂ →₀ ℂ) :
        (a : AddChar α ℂ) → ℂ)
      x)
  1
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₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have refine_2 : (¬∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → False
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₀)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
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
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have refine_2₄ : (∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → False
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₀)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
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
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have 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
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₀)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
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
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have 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
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₀)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
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
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
have 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
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₀)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)
have intro : ∀ (val : Fintype α),
  Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      (0 : AddChar (AddChar α ℂ) ℂ) ↔
    a = 0
have rw : Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
    ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) 0 : AddChar (AddChar α ℂ) ℂ) ↔
  a = 0
Tactic: rw [← map_zero doubleDualEmb, doubleDualEmb_inj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
rw :
  Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) 0 : AddChar (AddChar α ℂ) ℂ) ↔
    a = 0
⊢ Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      (0 : AddChar (AddChar α ℂ) ℂ) ↔
    a = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [← map_zero doubleDualEmb, doubleDualEmb_inj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : ∀ (val : Fintype α), Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0
Tactic: rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : ∀ (val : Fintype α), Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
Tactic: classical
  cases nonempty_fintype α
  rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
intro : ∀ (val : Fintype α), Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro₁ : ∀ (val : Fintype α), Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0
Tactic: classical
  cases nonempty_fintype α
  rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : ∀ (val : Fintype α), Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : Eq (α := ℂ) (if a = 0 then 1 else 0) 0 ↔ a ≠ 0
Tactic: rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
intro : Eq (α := ℂ) (if a = 0 then 1 else 0) 0 ↔ a ≠ 0
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro₁ : ¬a = 0 ↔ a ≠ 0
Tactic: rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
have intro : ∀ (val : Fintype α), Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
Tactic: classical
  cases nonempty_fintype α
  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᶠ[ae μ] f₂
⊢ fourierIntegral e μ L f₁ = fourierIntegral e μ L f₂
have h : ∀ (x : W), fourierIntegral e μ L f₁ x = fourierIntegral e μ L f₂ x
Tactic: ext