-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem mFourierSubalgebra_coe :
    (mFourierSubalgebra d).toSubalgebra.toSubmodule = span ℂ (range mFourier)

Proof state:
case hs.refine_2.intro.intro
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
⊢ mFourier m * mFourier n ∈ range mFourier

Tactic:
refine ⟨m + n, ?_⟩

Result:
case hs.refine_2.intro.intro
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
⊢ mFourier (m + n) = mFourier m * mFourier n

Proof state:
case hs.refine_1
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ mFourier 0 = 1

Tactic:
ext z

Result:
case hs.refine_1.h
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
z : UnitAddTorus d
⊢ (mFourier 0) z = 1 z

Proof state:
case hs
d : Type u_1
inst✝ : Fintype d
⊢ ↑(Submonoid.closure (range mFourier)) ⊆ ↑(span ℂ (range mFourier))

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

Result:
case hs.refine_1
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ mFourier 0 = 1

case hs.refine_2
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ ∀ (x y : C(UnitAddTorus d, ℂ)),
    x ∈ Submonoid.closure (range mFourier) →
      y ∈ Submonoid.closure (range mFourier) → x ∈ range mFourier → y ∈ range mFourier → x * y ∈ range mFourier

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ Subalgebra.toSubmodule (mFourierSubalgebra d).toSubalgebra = span ℂ (range mFourier)

Tactic:
apply adjoin_eq_span_of_subset

Result:
case hs
d : Type u_1
inst✝ : Fintype d
⊢ ↑(Submonoid.closure (range mFourier)) ⊆ ↑(span ℂ (range mFourier))

Proof state:
case hs.refine_2.intro.intro.h
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
z : UnitAddTorus d
⊢ (mFourier (m + n)) z = (mFourier m * mFourier n) z

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

Result:
no goals

Proof state:
case hs.refine_1.h
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
z : UnitAddTorus d
⊢ (mFourier 0) z = 1 z

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

Result:
no goals

Proof state:
case hs.refine_2.intro.intro
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
⊢ mFourier (m + n) = mFourier m * mFourier n

Tactic:
ext z

Result:
case hs.refine_2.intro.intro.h
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
z : UnitAddTorus d
⊢ (mFourier (m + n)) z = (mFourier m * mFourier n) z

Proof state:
case hs.refine_2
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ ∀ (x y : C(UnitAddTorus d, ℂ)),
    x ∈ Submonoid.closure (range mFourier) →
      y ∈ Submonoid.closure (range mFourier) → x ∈ range mFourier → y ∈ range mFourier → x * y ∈ range mFourier

Tactic:
rintro _ _ _ _ ⟨m, rfl⟩ ⟨n, rfl⟩

Result:
case hs.refine_2.intro.intro
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
⊢ mFourier m * mFourier n ∈ range mFourier