-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierSubalgebra_coe :
    Subalgebra.toSubmodule (@fourierSubalgebra T).toSubalgebra = span ℂ (range (@fourier T))

Proof state:
case hs.refine_1.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
z : AddCircle T
⊢ (fourier 0) z = 1 z

Tactic:
exact fourier_zero

Result:
no goals

Proof state:
case hs.refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)),
    x ∈ Submonoid.closure (range fourier) →
      y ∈ Submonoid.closure (range fourier) → x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier

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

Result:
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier m * fourier n ∈ range fourier

Proof state:
case hs.refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1

Tactic:
ext1 z

Result:
case hs.refine_1.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
z : AddCircle T
⊢ (fourier 0) z = 1 z

Proof state:
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier m * fourier n ∈ range fourier

Tactic:
refine ⟨m + n, ?_⟩

Result:
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier (m + n) = fourier m * fourier n

Proof state:
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ ↑(span ℂ (range fourier))

Tactic:
refine Subset.trans ?_ Submodule.subset_span

Result:
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ range fourier

Proof state:
case hs
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ x ∈ range fourier

Tactic:
refine Submonoid.closure_induction (fun _ => id) ⟨0, ?_⟩ ?_ hx

Result:
case hs.refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1

case hs.refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)),
    x ∈ Submonoid.closure (range fourier) →
      y ∈ Submonoid.closure (range fourier) → x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier

Proof state:
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ range fourier

Tactic:
intro x hx

Result:
case hs
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ x ∈ range fourier

Proof state:
case hs.refine_2.intro.intro.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
z : AddCircle T
⊢ (fourier (m + n)) z = (fourier m * fourier n) z

Tactic:
exact fourier_add

Result:
no goals

Proof state:
T : ℝ
⊢ Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = span ℂ (range fourier)

Tactic:
apply adjoin_eq_span_of_subset

Result:
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ ↑(span ℂ (range fourier))

Proof state:
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier (m + n) = fourier m * fourier n

Tactic:
ext1 z

Result:
case hs.refine_2.intro.intro.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
z : AddCircle T
⊢ (fourier (m + n)) z = (fourier m * fourier n) z