awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ 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:
⟨circleEquivComplex.injective.comp zmod_injective, rfl⟩

Premises used: Function.Injective.comp, AddChar.circleEquivComplex, And.intro, AddEquiv.injective, AddChar.zmod_injective, rfl
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ 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:
exact ⟨circleEquivComplex.injective.comp zmod_injective, rfl⟩
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ Eq (α := AddChar (ZMod n) ℂ) ((zmodAddEquiv : (a : ZMod n) → AddChar (ZMod n) ℂ) x : AddChar (ZMod n) ℂ)
    ((circleEquivComplex : (a : AddChar (ZMod n) Circle) → AddChar (ZMod n) ℂ) (zmod n x) : AddChar (ZMod n) ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
intro : ∀ (val : Fintype α), Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)
⊢ Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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} ℂ (α → ℂ)
intro₁ intro₂ : Fintype.card α = Fintype.card α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = finrank.{0, u_1} ℂ (α → ℂ)

Tactic:
rw [card_eq, Module.finrank_fintype_fun_eq_card]

Premises used: AddChar.card_eq, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
rw :
  Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) : (a : AddChar α ℂ) → α → ℂ)
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := (a : AddChar α ℂ) → α → ℂ) (DFunLike.coe (β := fun (x : α) ↦ ℂ))
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))
⊢ Eq (α := (a : AddChar α ℂ) → α → ℂ) (⇑(complexBasis α) : (a : AddChar α ℂ) → α → ℂ)
    (DFunLike.coe (β := fun (x : α) ↦ ℂ))

Tactic:
rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]

Premises used: coe_basisOfLinearIndependentOfCardEqFinrank, AddChar.complexBasis
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
ψ : AddChar α ℂ
rw rw₁ : Eq (α := α → ℂ) (⇑ψ : (a : α) → ℂ) (⇑ψ : (a : α) → ℂ)
⊢ Eq (α := α → ℂ) ((complexBasis α : (a : AddChar α ℂ) → α → ℂ) ψ : α → ℂ) ((⇑ψ : (a : α) → ℂ) : (a : α) → ℂ)

Tactic:
rw [coe_complexBasis]

Premises used: AddChar.coe_complexBasis
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) ↔ a ≠ 0

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

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
refine_1 : (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) → a ≠ 0
refine_2 : ∀ (ha : a ≠ 0), ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)
⊢ (∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) ↔ a ≠ 0

Tactic:
refine ⟨?_, fun ha ↦ ?_⟩
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
ψ : AddChar α ℂ
hψ : Ne (α := ℂ) ((ψ : (a : α) → ℂ) 0 : ℂ) (1 : ℂ)
⊢ False

Tactic:
hψ ψ.map_zero_eq_one

Premises used: AddChar.map_zero_eq_one
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
ψ : AddChar α ℂ
hψ : Ne (α := ℂ) ((ψ : (a : α) → ℂ) 0 : ℂ) (1 : ℂ)
⊢ False

Tactic:
exact hψ ψ.map_zero_eq_one

Premises used: AddChar.map_zero_eq_one
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
ha : a ≠ 0
refine_2 : ∀ (h : ∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)), False
⊢ ∃ (ψ : AddChar α ℂ), Ne (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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
⊢ (∑ 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
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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
⊢ (∑ 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
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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
⊢ 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₁

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
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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
⊢ 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₁

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
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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₀ :
  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:
one_ne_zero (h₁.symm.trans h₀)

Premises used: one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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₀ :
  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:
exact one_ne_zero (h₁.symm.trans h₀)

Premises used: one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ (∀ (ψ : AddChar α ℂ), Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)) ↔ a = 0

Tactic:
simpa using exists_apply_ne_zero.not

Premises used: Iff.not, AddChar.exists_apply_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
a : α
ha : Membership.mem (γ := AddSubgroup α) (AddMonoidHom.ker (M := AddChar (AddChar α ℂ) ℂ) doubleDualEmb) a
ψ : AddChar α ℂ
⊢ Eq (α := ℂ) ((ψ : (a : α) → ℂ) a : ℂ) (1 : ℂ)

Tactic:
simpa using DFunLike.congr_fun ha (Additive.ofMul ψ)

Premises used: DFunLike.congr_fun, Additive.ofMul, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
intro :
  ∀ (val : Fintype α),
    Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
      (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
val : Fintype α
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)

Tactic:
(Fintype.bijective_iff_injective_and_card _).2
    ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩

Premises used: Iff.mpr, AddChar.doubleDualEmb_injective, AddChar.card_eq, Fintype.bijective_iff_injective_and_card, And.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
val : Fintype α
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)

Tactic:
exact (Fintype.bijective_iff_injective_and_card _).2
    ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩

Premises used: Iff.mpr, AddChar.doubleDualEmb_injective, AddChar.card_eq, Fintype.bijective_iff_injective_and_card, And.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a b : α
inst_1 : Finite α
⊢ Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) b : AddChar (AddChar α ℂ) ℂ) ↔
    a = b

Tactic:
doubleDualEmb_injective.eq_iff

Premises used: AddChar.doubleDualEmb_injective, Function.Injective.eq_iff
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ Eq (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      (0 : AddChar (AddChar α ℂ) ℂ) ↔
    a = 0

Tactic:
rw [← map_zero doubleDualEmb, doubleDualEmb_inj]

Premises used: map_zero, AddChar.doubleDualEmb, AddChar.doubleDualEmb_inj
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Ne (α := AddChar (AddChar α ℂ) ℂ) ((doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ) a : AddChar (AddChar α ℂ) ℂ)
      (0 : AddChar (AddChar α ℂ) ℂ) ↔
    a ≠ 0

Tactic:
doubleDualEmb_eq_zero.not

Premises used: Iff.not, AddChar.doubleDualEmb_eq_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
⊢ Eq.{u_1 + 1} (α := (a : α) → AddChar (AddChar α ℂ) ℂ) (⇑doubleDualEquiv : (a : α) → AddChar (AddChar α ℂ) ℂ)
    (⇑doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
a : AddChar (AddChar α ℂ) ℂ
⊢ (doubleDualEmb : (a : α) → AddChar (AddChar α ℂ) ℂ)
      ((AddEquiv.symm doubleDualEquiv : (a : AddChar (AddChar α ℂ) ℂ) → α) a : α) =
    a

Tactic:
doubleDualEquiv.apply_symm_apply _

Premises used: AddEquiv.apply_symm_apply, AddChar.doubleDualEquiv
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
a : AddChar (AddChar α ℂ) ℂ
⊢ (AddEquiv.symm doubleDualEquiv : (a : AddChar (AddChar (AddChar (AddChar α ℂ) ℂ) ℂ) ℂ) → AddChar (AddChar α ℂ) ℂ)
      ((doubleDualEmb : (a : AddChar (AddChar α ℂ) ℂ) → AddChar (AddChar (AddChar (AddChar α ℂ) ℂ) ℂ) ℂ) a :
        AddChar (AddChar (AddChar (AddChar α ℂ) ℂ) ℂ) ℂ) =
    a

Tactic:
doubleDualEquiv.symm_apply_apply _

Premises used: AddEquiv.symm_apply_apply, AddChar.doubleDualEquiv
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
inst_2 : DecidableEq α
a : α
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) (if a = 0 then (↑(Fintype.card α) : ℂ) else 0)

Tactic:
simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

Premises used: AddChar.sum_eq_ite, AddChar.doubleDualEmb, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Finite α
inst_2 : DecidableEq α
a : α
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) (if a = 0 then 1 else 0)

Tactic:
simpa using expect_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

Premises used: AddChar.doubleDualEmb, DFunLike.coe, AddChar.expect_eq_ite
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
intro : Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0
⊢ Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0

Tactic:
rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, AddChar.sum_apply_eq_ite
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
⊢ Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0

Tactic:
Nat.cast_ne_zero.2 Fintype.card_ne_zero

Premises used: Iff.mpr, Fintype.card_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
⊢ Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0

Tactic:
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Premises used: Iff.mpr, Fintype.card_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
intro : ∀ (val : Fintype α), Eq (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0
intro₁ : ∀ (val : Fintype α), Ne (α := ℂ) (↑(Fintype.card α) : ℂ) 0
⊢ 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

Premises used: Iff.mpr, Ne.ite_eq_right_iff, AddChar.sum_apply_eq_ite, Fintype.card_ne_zero, nonempty_fintype, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Ne (α := ℂ) (∑ ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a = 0

Tactic:
sum_apply_eq_zero_iff_ne_zero.not_left

Premises used: AddChar.sum_apply_eq_zero_iff_ne_zero, Iff.not_left
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
val : Fintype α
intro : Eq (α := ℂ) (if a = 0 then 1 else 0) 0 ↔ a ≠ 0
intro₁ intro₂ : ¬a = 0 ↔ a ≠ 0
⊢ Eq (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a ≠ 0

Tactic:
rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, one_ne_zero, AddChar.expect_apply_eq_ite
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
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

Tactic:
classical
  cases nonempty_fintype α
  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, nonempty_fintype, one_ne_zero, AddChar.expect_apply_eq_ite
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
a : α
inst_1 : Finite α
⊢ Ne (α := ℂ) (𝔼 ψ : AddChar α ℂ, (ψ : (a : α) → ℂ) a) 0 ↔ a = 0

Tactic:
expect_apply_eq_zero_iff_ne_zero.not_left

Premises used: AddChar.expect_apply_eq_zero_iff_ne_zero, Iff.not_left
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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₂
h : ∀ (x : W), fourierIntegral e μ L f₁ x = fourierIntegral e μ L f₂ x
⊢ fourierIntegral e μ L f₁ = fourierIntegral e μ L f₂

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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₂
x : W
h :
  EventuallyEq.{u_2, u_4} (β := E) (ae μ)
    (fun (a : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
        (f₁ a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)
⊢ fourierIntegral e μ L f₁ x = fourierIntegral e μ L f₂ x

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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₂
x : W
h :
  ∀ (a : V) (hf' : f₁ a = f₂ a),
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₁ a) =
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae μ)
    (fun (a : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
        (f₁ a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f₂ a)

Tactic:
filter_upwards [hf] with _ hf'