awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : Fintype G
inst_2 : Semifield R
inst_3 : IsDomain R
inst_4 : CharZero R
ψ : AddChar G R
rw : Eq.{u_3 + 1} (α := R) (if ψ = 0 then 1 else 0) 0 ↔ ψ ≠ 0
rw₁ rw₂ : ¬ψ = 0 ↔ ψ ≠ 0
⊢ Eq.{u_3 + 1} (α := R) (𝔼 x : G, (ψ : (a : G) → R) x) 0 ↔ ψ ≠ 0

Tactic:
rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, one_ne_zero, AddChar.expect_eq_ite
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : Fintype G
inst_2 : Semifield R
inst_3 : IsDomain R
inst_4 : CharZero R
ψ : AddChar G R
⊢ Ne.{u_3 + 1} (α := R) (𝔼 x : G, (ψ : (a : G) → R) x) 0 ↔ ψ = 0

Tactic:
expect_eq_zero_iff_ne_zero.not_left

Premises used: AddChar.expect_eq_zero_iff_ne_zero, Iff.not_left
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ : AddChar G R
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ : (a : G) → R) (⇑ψ : (a : G) → R)) 1

Tactic:
simp [wInner_cWeight_eq_expect, ψ.norm_apply]

Premises used: RCLike.wInner_cWeight_eq_expect, AddChar.norm_apply
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
pos :
  ∀ (h : ψ₁ = ψ₂),
    Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
neg :
  ∀ (h : ¬ψ₁ = ψ₂),
    Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R))
    (if ψ₁ = ψ₂ then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
pos : Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₂ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
pos₁ pos₂ : Eq.{u_3 + 1} (α := R) 1 1
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1

Tactic:
rw [h, wInner_cWeight_self]

Premises used: AddChar.wInner_cWeight_self
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
rwa : ¬ψ₂ * ψ₁⁻¹ = 1
rwa₁ : ¬ψ₂ = ψ₁
rwa₂ rwa₃ rwa₄ rwa₅ : ¬ψ₁ = ψ₂
⊢ ψ₂ * ψ₁⁻¹ ≠ 1

Tactic:
rwa [Ne, mul_inv_eq_one, eq_comm]

Premises used: mul_inv_eq_one, Ne, eq_comm
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ψ₂ * ψ₁⁻¹ ≠ 1

Tactic:
have : ψ₂ * ψ₁⁻¹ ≠ 1 := by rwa [Ne, mul_inv_eq_one, eq_comm]
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₂ * ψ₁⁻¹ ≠ 1
neg :
  Eq.{u_3 + 1} (α := R) (𝔼 i : G, HMul.hMul (α := R) (β := R) ((ψ₂ : (a : G) → R) i : R) (((ψ₁ : (a : G) → R) i)⁻¹ : R))
    0
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0

Tactic:
simp_rw [wInner_cWeight_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]

Premises used: RCLike.wInner_cWeight_eq_expect, RCLike.inner_apply, AddChar.inv_apply_eq_conj
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₂ * ψ₁⁻¹ ≠ 1
⊢ Eq.{u_3 + 1} (α := R) (𝔼 i : G, HMul.hMul (α := R) (β := R) ((ψ₂ : (a : G) → R) i : R) (((ψ₁ : (a : G) → R) i)⁻¹ : R))
    0

Tactic:
simpa [map_neg_eq_inv] using expect_eq_zero_iff_ne_zero.2 this

Premises used: Iff.mpr, AddChar.map_neg_eq_inv, AddChar.expect_eq_zero_iff_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 0 ↔ ψ₁ ≠ ψ₂
rw₁ rw₂ : ¬ψ₁ = ψ₂ ↔ ψ₁ ≠ ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0 ↔ ψ₁ ≠ ψ₂

Tactic:
rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, AddChar.wInner_cWeight_eq_boole, one_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 1 ↔ ψ₁ = ψ₂
rw₁ rw₂ : ψ₁ = ψ₂ ↔ ψ₁ = ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1 ↔ ψ₁ = ψ₂

Tactic:
rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]

Premises used: Ne.ite_eq_left_iff, AddChar.wInner_cWeight_eq_boole, one_ne_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Finite G
intro :
  ∀ (val : Fintype G), LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))
⊢ LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Finite G
val : Fintype G
⊢ LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))

Tactic:
linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero coe_ne_zero
    fun ψ₁ ψ₂ ↦ wInner_cWeight_eq_zero_iff_ne.2

Premises used: Iff.mpr, AddChar.wInner_cWeight_eq_zero_iff_ne, AddChar.coe_ne_zero, RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Finite G
val : Fintype G
⊢ LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))

Tactic:
exact linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero coe_ne_zero
    fun ψ₁ ψ₂ ↦ wInner_cWeight_eq_zero_iff_ne.2

Premises used: Iff.mpr, AddChar.wInner_cWeight_eq_zero_iff_ne, RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
⊢ card (AddChar G R) ≤ card G

Tactic:
simpa only [Module.finrank_fintype_fun_eq_card] using
    (AddChar.linearIndependent G R).fintype_card_le_finrank

Premises used: LinearIndependent.fintype_card_le_finrank, AddChar.linearIndependent, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
x y : ℤ
⊢ Eq (α := Circle) ((zmod n (↑x : ZMod n) : (a : ZMod n) → Circle) (↑y : ZMod n) : Circle)
    ((exp : (a : ℝ) → Circle) (2 * π * (HMul.hMul (α := ℝ) (↑x : ℝ) (↑y : ℝ) / (↑n : ℝ))) : Circle)

Tactic:
simp [zmod, ← Int.cast_mul x y, -Int.cast_mul, ZMod.toAddCircle_intCast,
    AddCircle.toCircle_apply_mk]

Premises used: AddChar.zmod, AddCircle.toCircle_apply_mk, Int.cast_mul, ZMod.toAddCircle_intCast
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
⊢ ∀ (x : ZMod n),
    Eq (α := Circle) ((zmod n 0 : (a : ZMod n) → Circle) x : Circle) ((1 : (a : ZMod n) → Circle) x : Circle)

Tactic:
simp [zmod]

Premises used: AddChar.zmod
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
⊢ ∀ (x y : ZMod n), zmod n (x + y) = zmod n x * zmod n y

Tactic:
simp [DFunLike.ext_iff, zmod, add_mul, map_add_eq_mul]

Premises used: add_mul, AddChar.map_add_eq_mul, AddChar.zmod, DFunLike.ext_iff
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
simp_rw : ∀ (x x_1 : ℤ), zmod n (↑x : ZMod n) = zmod n (↑x_1 : ZMod n) → Eq (α := ZMod n) (↑x : ZMod n) (↑x_1 : ZMod n)
⊢ Injective (zmod n)

Tactic:
simp_rw [Injective, ZMod.intCast_surjective.forall]

Premises used: Function.Surjective.forall, Function.Injective, ZMod.intCast_surjective
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
x y : ℤ
h : zmod n (↑x : ZMod n) = zmod n (↑y : ZMod n)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn : (n : ℝ) ≠ 0 := NeZero.ne _
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
x y : ℤ
h : zmod n (↑x : ZMod n) = zmod n (↑y : ZMod n)
hn : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ZMod n) (↑x : ZMod n) (↑y : ZMod n)

Tactic:
simpa [pi_ne_zero, exp_inj, hn, CharP.intCast_eq_intCast (ZMod n) n] using
    (zmod_intCast ..).symm.trans <| (DFunLike.congr_fun h ((1 : ℤ) : ZMod n)).trans <|
      zmod_intCast ..

Premises used: Int.cast, DFunLike.congr_fun, Circle.exp_inj, ZMod, CharP.intCast_eq_intCast, OfNat.ofNat, Eq.symm, AddChar.zmod_intCast, Real.pi_ne_zero, Eq.trans
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
n : ℕ
inst : NeZero n
x y : ZMod n
⊢ zmod n x = zmod n y ↔ x = y

Tactic:
zmod_injective.eq_iff

Premises used: Function.Injective.eq_iff, AddChar.zmod_injective
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ zmod n 0 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
⊢ ∀ (a b : ZMod n), zmod n (a + b) = zmod n a * zmod n b

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
ι : Type u_2
inst : DecidableEq ι
n : ι → ℕ
inst_1 : ∀ (i : ι), NeZero (n i)
f g : (i : ι) → ZMod (n i)
h :
  Eq.{max 1 (u_2 + 1)} (α := (i : ι) → AddChar (ZMod (n i)) Circle) (fun (i : ι) ↦ zmod (n i) (f i)) fun (i : ι) ↦
    zmod (n i) (g i)
⊢ f = g

Tactic:
simpa [funext_iff] using h

Premises used: funext_iff
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
⊢ Eq (α := Circle)
    (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((ψ : (a : α) → ℂ) 0)
        ⋯ :
      ↥(Submonoid.unitSphere ℂ))
    (1 : Circle)

Tactic:
simp [Circle]

Premises used: Circle
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a_1 b_1 : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
a b : α
a₁ :
  (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) (a + b)) ⋯) :
      ℂ) =
    (↑(HMul.hMul (α := Circle) (β := Circle)
          (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              ((ψ : (a : α) → ℂ) a) ⋯ :
            ↥(Submonoid.unitSphere ℂ))
          (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              ((ψ : (a : α) → ℂ) b) ⋯ :
            ↥(Submonoid.unitSphere ℂ))) :
      ℂ)
⊢ Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
      ((ψ : (a : α) → ℂ) (a + b)) ⋯ =
    HMul.hMul (α := Circle) (β := Circle)
      (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) a) ⋯ :
        ↥(Submonoid.unitSphere ℂ))
      (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) b) ⋯ :
        ↥(Submonoid.unitSphere ℂ))

Tactic:
ext : 1
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a_1 b_1 : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
a b : α
⊢ (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) (a + b)) ⋯) :
      ℂ) =
    (↑(HMul.hMul (α := Circle) (β := Circle)
          (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              ((ψ : (a : α) → ℂ) a) ⋯ :
            ↥(Submonoid.unitSphere ℂ))
          (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              ((ψ : (a : α) → ℂ) b) ⋯ :
            ↥(Submonoid.unitSphere ℂ))) :
      ℂ)

Tactic:
simp [map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α Circle
h :
  ∀ (x : α),
    Eq (α := Circle)
      ((((fun (ψ : AddChar α ℂ) ↦
                  ({
                      toFun := fun (a : α) ↦
                        Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                          ((ψ : (a : α) → ℂ) a) ⋯,
                      map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
                    AddChar α Circle))
                ((fun (ψ : AddChar α Circle) ↦
                    ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ)
                        (coeHom.comp ψ.toMonoidHom) :
                      AddChar α ℂ))
                  ψ) :
              AddChar α Circle) :
            (a : α) → Circle)
          x :
        Circle)
      ((ψ : (a : α) → Circle) x : Circle)
⊢ (fun (ψ : AddChar α ℂ) ↦
        ({
            toFun := fun (a : α) ↦
              Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                ((ψ : (a : α) → ℂ) a) ⋯,
            map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
          AddChar α Circle))
      ((fun (ψ : AddChar α Circle) ↦
          ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
            AddChar α ℂ))
        ψ) =
    ψ

Tactic:
ext : 1
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α Circle
x : α
⊢ Eq (α := Circle)
    ((((fun (ψ : AddChar α ℂ) ↦
                ({
                    toFun := fun (a : α) ↦
                      Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                        ((ψ : (a : α) → ℂ) a) ⋯,
                    map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
                  AddChar α Circle))
              ((fun (ψ : AddChar α Circle) ↦
                  ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ)
                      (coeHom.comp ψ.toMonoidHom) :
                    AddChar α ℂ))
                ψ) :
            AddChar α Circle) :
          (a : α) → Circle)
        x :
      Circle)
    ((ψ : (a : α) → Circle) x : Circle)

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
h :
  ∀ (x : α),
    Eq (α := ℂ)
      (((fun (ψ : AddChar α Circle) ↦
                ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
                  AddChar α ℂ))
              ((fun (ψ : AddChar α ℂ) ↦
                  ({
                      toFun := fun (a : α) ↦
                        Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                          ((ψ : (a : α) → ℂ) a) ⋯,
                      map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
                    AddChar α Circle))
                ψ) :
            (a : α) → ℂ)
          x :
        ℂ)
      ((ψ : (a : α) → ℂ) x : ℂ)
⊢ (fun (ψ : AddChar α Circle) ↦
        ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
          AddChar α ℂ))
      ((fun (ψ : AddChar α ℂ) ↦
          ({
              toFun := fun (a : α) ↦
                Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                  ((ψ : (a : α) → ℂ) a) ⋯,
              map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
            AddChar α Circle))
        ψ) =
    ψ

Tactic:
ext : 1
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
x : α
⊢ Eq (α := ℂ)
    (((fun (ψ : AddChar α Circle) ↦
              ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
                AddChar α ℂ))
            ((fun (ψ : AddChar α ℂ) ↦
                ({
                    toFun := fun (a : α) ↦
                      Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                        ((ψ : (a : α) → ℂ) a) ⋯,
                    map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
                  AddChar α Circle))
              ψ) :
          (a : α) → ℂ)
        x :
      ℂ)
    ((ψ : (a : α) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
obtain :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (hn : ∀ (i : ι), 1 < n i) (e : α ≃+ ⨁ (i : ι), ZMod (n i)),
    Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α

Tactic:
obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α

Premises used: AddCommGroup.equiv_directSum_zmod_of_finite'
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
⊢ 1 < n i

Tactic:
have := hn i
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ n i ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ NeZero (n i)

Tactic:
exact ⟨by positivity⟩
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ ∀ (i : ι), NeZero (n i)

Tactic:
have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ :=
  fun (a : α) ↦
    coeHom.compAddChar
      ((mkZModAux n
            (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
              (a : ι) → ZMod (n a))).compAddMonoidHom
        (↑e : α →+ ⨁ (i : ι), ZMod (n i)))
⊢ Injective f

Tactic:
have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ :=
  fun (a : α) ↦
    coeHom.compAddChar
      ((mkZModAux n
            (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
              (a : ι) → ZMod (n a))).compAddMonoidHom
        (↑e : α →+ ⨁ (i : ι), ZMod (n i)))
hf : Injective f
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α

Tactic:
(card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)

Premises used: Fintype.card_le_of_injective, AddChar.card_addChar_le, LE.le.antisymm
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ :=
  fun (a : α) ↦
    coeHom.compAddChar
      ((mkZModAux n
            (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
              (a : ι) → ZMod (n a))).compAddMonoidHom
        (↑e : α →+ ⨁ (i : ι), ZMod (n i)))
hf : Injective f
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α

Tactic:
exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)

Premises used: Fintype.card_le_of_injective, AddChar.card_addChar_le, LE.le.antisymm
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
have : ∀ (i : ι), NeZero (n i)
have₁ : ∀ (hn' : ∀ (i : ι), NeZero (n i)), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have₂ : ∀ (i : ι), NeZero (n i)
have₃ have₄ have₅ : ∀ (hn' : ∀ (i : ι), NeZero (n i)), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have₆ :
  ∀ (hn' : ∀ (i : ι), NeZero (n i)),
    let f : α → AddChar α ℂ := fun (a : α) ↦
      coeHom.compAddChar
        ((mkZModAux n
              (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
                (a : ι) → ZMod (n a))).compAddMonoidHom
          (↑e : α →+ ⨁ (i : ι), ZMod (n i)));
    ∀ (hf : Injective f), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α

Tactic:
classical
  have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
  have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
refine :
  Bijective (α := ZMod n) (β := AddChar (ZMod n) ℂ)
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom circleEquivComplex) (toAddMonoidHom zmodHom)) :
      (a : ZMod n) → AddChar (ZMod n) ℂ)
⊢ ZMod n ≃+ AddChar (ZMod n) ℂ

Tactic:
refine AddEquiv.ofBijective
    (circleEquivComplex.toAddMonoidHom.comp <| AddChar.toAddMonoidHom zmodHom) ?_

Premises used: AddChar.toAddMonoidHom, AddEquiv.toAddMonoidHom, AddChar.circleEquivComplex, AddChar.zmodHom, AddMonoidHom.comp, AddEquiv.ofBijective
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
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)
⊢ Bijective (α := ZMod n) (β := AddChar (ZMod n) ℂ)
    (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom circleEquivComplex) (toAddMonoidHom zmodHom)) :
      (a : ZMod n) → AddChar (ZMod n) ℂ)

Tactic:
rw [Fintype.bijective_iff_injective_and_card, card_eq]

Premises used: AddChar.card_eq, Fintype.bijective_iff_injective_and_card