awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ 1 = norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) fun (x : d) ↦ 0 : ℂ)

Tactic:
simp only [mFourier, ContinuousMap.coe_mk, fourier_eval_zero, Finset.prod_const_one,
      CStarRing.norm_one]

Premises used: fourier_eval_zero, Finset.prod_const_one, UnitAddTorus.mFourier, ContinuousMap.coe_mk, CStarRing.norm_one
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
simp_rw :
  Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
⊢ Eq (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) z : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)

Tactic:
simp_rw [mFourier, ContinuousMap.coe_mk]

Premises used: UnitAddTorus.mFourier, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
⊢ HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)

Tactic:
have := Finset.prod_mul_prod_compl {i} (fun j ↦ fourier ((Pi.single i (1 : ℤ) : d → ℤ) j) (z j))
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  ∀
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)),
    Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
      ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
rw₁ :
  (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) →
    d → ℂ
rw₂ :
  ∀
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
    (j : d) (hj : Membership.mem (γ := Finset d) {i}ᶜ j),
    Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 j) : (a : AddCircle 1) → ℂ) (z j) : ℂ) (1 : ℂ)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)

Tactic:
rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this

Premises used: Finset.prod_singleton, Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this_1 :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
rw₂ :
  Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
rw₃ rw₄ : Eq (α := ℂ) ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ) ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)

Tactic:
rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]

Premises used: Finset.prod_const_one, mul_one, Pi.single_eq_same
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
j : d
hj : Membership.mem (γ := Finset d) {i}ᶜ j
⊢ ¬j = i

Tactic:
rw [Finset.mem_compl, Finset.mem_singleton] at hj

Premises used: Finset.mem_singleton, Finset.mem_compl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
j : d
hj : ¬j = i
⊢ Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 j) : (a : AddCircle 1) → ℂ) (z j) : ℂ) (1 : ℂ)

Tactic:
simp only [Pi.single_eq_of_ne hj, fourier_zero]

Premises used: fourier_zero, Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
⊢ LE.le.{u_2} (α := Subalgebra ℂ C(UnitAddTorus d, ℂ)) (adjoin ℂ (range mFourier)) (star (adjoin ℂ (range mFourier)))

Tactic:
adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
refine : range mFourier ⊆ (↑(star (adjoin ℂ (range mFourier))) : Set C(UnitAddTorus d, ℂ))
⊢ LE.le.{u_2} (α := Subalgebra ℂ C(UnitAddTorus d, ℂ)) (adjoin ℂ (range mFourier)) (star (adjoin ℂ (range mFourier)))

Tactic:
refine adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
⊢ mFourier n ∈ (↑(star (adjoin ℂ (range mFourier))) : Set C(UnitAddTorus d, ℂ))

Tactic:
subset_adjoin ⟨-n, ?_⟩

Premises used: iInf, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf, Set.preimage, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
refine : mFourier (-n) = star (mFourier n)
⊢ mFourier n ∈ (↑(star (adjoin ℂ (range mFourier))) : Set C(UnitAddTorus d, ℂ))

Tactic:
refine subset_adjoin ⟨-n, ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
h :
  ∀ (x : UnitAddTorus d),
    Eq (α := ℂ) ((mFourier (-n) : (a : UnitAddTorus d) → ℂ) x : ℂ)
      ((star (mFourier n) : (a : UnitAddTorus d) → ℂ) x : ℂ)
⊢ mFourier (-n) = star (mFourier n)

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
x : UnitAddTorus d
⊢ Eq (α := ℂ) ((mFourier (-n) : (a : UnitAddTorus d) → ℂ) x : ℂ) ((star (mFourier n) : (a : UnitAddTorus d) → ℂ) x : ℂ)

Tactic:
simp only [mFourier_neg, starRingEnd_apply, ContinuousMap.star_apply]

Premises used: UnitAddTorus.mFourier_neg, starRingEnd_apply, ContinuousMap.star_apply
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
hs :
  (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
    (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))
⊢ Eq (α := Submodule ℂ C(UnitAddTorus d, ℂ))
    ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
        (mFourierSubalgebra d).toSubalgebra :
      Submodule ℂ C(UnitAddTorus d, ℂ))
    (span ℂ (range mFourier) : Submodule ℂ C(UnitAddTorus d, ℂ))

Tactic:
apply adjoin_eq_span_of_subset

Premises used: Algebra.adjoin_eq_span_of_subset
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
    (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))

Tactic:
.trans (fun x ↦ Submonoid.closure_induction (fun _ ↦ id) ⟨0, ?_⟩ ?_) subset_span

Premises used: HasSubset.Subset.trans, Submonoid.closure_induction, Submodule.subset_span
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
hs : ∀ (x : C(UnitAddTorus d, ℂ)), Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1
hs₁ :
  ∀ (x x y : C(UnitAddTorus d, ℂ))
    (hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) x)
    (hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) y),
    Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) x →
      Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) y →
        Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) (x * y)
⊢ (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
    (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))

Tactic:
refine .trans (fun x ↦ Submonoid.closure_induction (fun _ ↦ id) ⟨0, ?_⟩ ?_) subset_span
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
hs :
  ∀ (z : UnitAddTorus d),
    Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) z : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) z : ℂ)
⊢ Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1

Tactic:
ext z
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
z : UnitAddTorus d
⊢ Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) z : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) z : ℂ)

Tactic:
simp only [mFourier, Pi.zero_apply, fourier_zero, Finset.prod_const, one_pow,
      ContinuousMap.coe_mk, ContinuousMap.one_apply]

Premises used: one_pow, fourier_zero, ContinuousMap.one_apply, Pi.zero_apply, Finset.prod_const, UnitAddTorus.mFourier, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
⊢ Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) (mFourier m * mFourier n)

Tactic:
⟨m + n, ?_⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Exists.intro, Set.range
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
hs : mFourier (m + n) = mFourier m * mFourier n
⊢ Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) (mFourier m * mFourier n)

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
hs :
  ∀ (z : UnitAddTorus d),
    Eq (α := ℂ) ((mFourier (m + n) : (a : UnitAddTorus d) → ℂ) z : ℂ)
      ((mFourier m * mFourier n : (a : UnitAddTorus d) → ℂ) z : ℂ)
⊢ mFourier (m + n) = mFourier m * mFourier n

Tactic:
ext z
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
z : UnitAddTorus d
⊢ Eq (α := ℂ) ((mFourier (m + n) : (a : UnitAddTorus d) → ℂ) z : ℂ)
    ((mFourier m * mFourier n : (a : UnitAddTorus d) → ℂ) z : ℂ)

Tactic:
simp only [mFourier, Pi.add_apply, fourier_apply, fourier_add', Finset.prod_mul_distrib,
      ContinuousMap.coe_mk, ContinuousMap.mul_apply]

Premises used: Finset.prod_mul_distrib, Pi.add_apply, fourier_apply, UnitAddTorus.mFourier, ContinuousMap.coe_mk, fourier_add', ContinuousMap.mul_apply
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
hxy : x ≠ y
⊢ ∃ (x_1 : d), ¬x x_1 = y x_1

Tactic:
rw [Ne, funext_iff, not_forall] at hxy

Premises used: funext_iff, Ne, Classical.not_forall
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
hxy : ∃ (x_1 : d), ¬x x_1 = y x_1
obtain :
  ∀ (i : d) (hi : ¬x i = y i),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y

Tactic:
obtain ⟨i, hi⟩ := hxy
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y

Tactic:
⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩

Premises used: Algebra.subset_adjoin, Pi.single, UnitAddTorus.mFourier, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
refine :
  Ne (α := ℂ)
    ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
      (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
    ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
      (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y

Tactic:
refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
rw : ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ Ne (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) x : ℂ)
    ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) y : ℂ)

Tactic:
rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]

Premises used: fourier_one, Subtype.coe_inj, Ne, UnitAddTorus.mFourier_single
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
contrapose : ∀ (hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)), x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)

Tactic:
contrapose hi
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ x i = y i

Tactic:
AddCircle.injective_toCircle one_ne_zero hi

Premises used: AddCircle.injective_toCircle, one_ne_zero
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ x i = y i

Tactic:
exact AddCircle.injective_toCircle one_ne_zero hi

Premises used: AddCircle.injective_toCircle, one_ne_zero
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₃ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₄ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₅ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
intro₆ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) x : ℂ)
      ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) y : ℂ)
intro₇ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i), ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
intro₈ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)), x i = y i
⊢ (mFourierSubalgebra d).SeparatesPoints

Tactic:
classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi

Premises used: fourier_one, funext_iff, Subtype.coe_inj, Ne, UnitAddTorus.mFourier_single, Classical.not_forall
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ (mFourierSubalgebra d).topologicalClosure = ⊤

Tactic:
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
    mFourierSubalgebra_separatesPoints

Premises used: UnitAddTorus.mFourierSubalgebra_separatesPoints, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
rw :
  Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
        (mFourierSubalgebra d).toSubalgebra))
    ⊤
⊢ Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ)) (topologicalClosure (span ℂ (range mFourier))) ⊤

Tactic:
rw [← mFourierSubalgebra_coe]

Premises used: UnitAddTorus.mFourierSubalgebra_coe
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
        (mFourierSubalgebra d).toSubalgebra))
    ⊤

Tactic:
congr_arg (Subalgebra.toSubmodule <| StarSubalgebra.toSubalgebra ·)
    mFourierSubalgebra_closure_eq_top

Premises used: iInf, StarSubalgebra.toSubalgebra, UnitAddTorus.mFourierSubalgebra_closure_eq_top, Set.Mem, Set.iInter, Set.univ, setOf, congr_arg, closure, Subalgebra.toSubmodule, Submodule.topologicalClosure, AddSubmonoid.topologicalClosure, Set.sInter, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
        (mFourierSubalgebra d).toSubalgebra))
    ⊤

Tactic:
exact congr_arg (Subalgebra.toSubmodule <| StarSubalgebra.toSubalgebra ·)
    mFourierSubalgebra_closure_eq_top

Premises used: StarSubalgebra.toSubalgebra, UnitAddTorus.mFourierSubalgebra_closure_eq_top, congr_arg, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
ι : Type u_2
b : ι → ℝ
⊢ Eq (α := (a : UnitAddTorus ι) → { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) })
    (⇑(measurableEquivPiIoc b) : (a : UnitAddTorus ι) → { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) })
    fun (x : UnitAddTorus ι) ↦
    Subtype.mk (p := fun (x : ι → ℝ) ↦ ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1))
      (fun (i : ι) ↦ (↑((AddCircle.equivIoc 1 (b i) : (a : AddCircle 1) → (↑(Ioc (b i) (b i + 1)) : Type)) (x i)) : ℝ))
      ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
ι : Type u_2
b : ι → ℝ
x : UnitAddTorus ι
⊢ Eq (α := { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) })
    ((measurableEquivPiIoc b : (a : UnitAddTorus ι) → { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }) x :
      { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) })
    (Subtype.mk (p := fun (x : ι → ℝ) ↦ ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1))
        (fun (i : ι) ↦
          (↑((AddCircle.equivIoc 1 (b i) : (a : AddCircle 1) → (↑(Ioc (b i) (b i + 1)) : Type)) (x i)) : ℝ))
        ⋯ :
      { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) })

Tactic:
rfl

Premises used: rfl