awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier n : (a : AddCircle T) → ℂ) x = (↑(n • x).toCircle : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
rw :
  Complex.exp ((↑2 : ℂ) * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))
⊢ (fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))

Tactic:
rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe,
    Circle.coe_exp, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
    Complex.ofReal_mul, Complex.ofReal_intCast]

Premises used: zsmul_eq_mul, Complex.ofReal_intCast, fourier_apply, QuotientAddGroup.mk_zsmul, Function.Periodic.lift_coe, Complex.ofReal_div, AddCircle.toCircle, Circle.coe_exp, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
e_z :
  2 * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)
⊢ Complex.exp (2 * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ 2 * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))

Tactic:
fourier_coe_apply

Premises used: fourier_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))

Tactic:
exact fourier_coe_apply

Premises used: fourier_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : AddCircle T
⊢ Eq (α := ℂ) ((fourier 0 : (a : AddCircle T) → ℂ) x : ℂ) (1 : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
⊢ (↑(toCircle (T := T) 0) : ℂ) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
rw₂ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * 0 / (↑T : ℂ)) = 1
rw₃ : Complex.exp (0 / (↑T : ℂ)) = 1
rw₄ : Complex.exp 0 = 1
rw₅ rw₆ : Eq (α := ℂ) 1 1
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)

Tactic:
rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]

Premises used: Complex.exp_zero, zero_div, fourier_coe_apply, MulZeroClass.mul_zero, Complex.ofReal_zero, QuotientAddGroup.mk_zero
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : AddCircle T
rw : (↑(HSMul.hSMul (α := ℤ) 1 x).toCircle : ℂ) = (↑x.toCircle : ℂ)
rw₁ rw₂ : (↑x.toCircle : ℂ) = (↑x.toCircle : ℂ)
⊢ (fourier 1 : (a : AddCircle T) → ℂ) x = (↑x.toCircle : ℂ)

Tactic:
rw [fourier_apply, one_zsmul]

Premises used: fourier_apply, one_zsmul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : AddCircle T
H :
  ∀ (z : ℝ),
    Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)

Tactic:
induction x using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
z : ℝ
H :
  Eq (α := ℂ) ((↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -n • z)) : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * n • z)) : ℂ) : ℂ)
H₁ :
  Eq (α := ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -n • z)) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * n • z))⁻¹ : ℂ)
H₂ :
  Eq (α := ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -n • z)) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (-(2 * π / T * n • z))) : ℂ)
H₃ :
  Eq (α := ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -(n • z))) : ℂ)
    (↑((Circle.exp : (a : ℝ) → Circle) (-(2 * π / T * n • z))) : ℂ)
⊢ (↑(Function.Periodic.lift (f := fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) ⋯
          (↑(-n • z) : ℝ ⧸ AddSubgroup.zmultiples T)) :
      ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      (↑(Function.Periodic.lift (f := fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) ⋯
            (↑(n • z) : ℝ ⧸ AddSubgroup.zmultiples T)) :
        ℂ)

Tactic:
simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
    neg_smul, mul_neg]

Premises used: neg_smul, Circle.exp_neg, Circle.coe_inv_eq_conj, Function.Periodic.lift_coe, mul_neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : AddCircle T
rw :
  Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)
⊢ (↑(-(n • x)).toCircle : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
rw [← neg_smul, ← fourier_apply]

Premises used: neg_smul, fourier_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : AddCircle T
⊢ Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)

Tactic:
fourier_neg

Premises used: fourier_neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : AddCircle T
⊢ Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)

Tactic:
exact fourier_neg

Premises used: fourier_neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
simp_rw : (↑((m + n) • x).toCircle : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
simp_rw₁ : (↑(m • x + n • x).toCircle : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
simp_rw₂ : (↑((m • x).toCircle * (n • x).toCircle) : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
⊢ (fourier (m + n) : (a : AddCircle T) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]

Premises used: AddCircle.toCircle_add, add_zsmul, Circle.coe_mul, fourier_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
rw :
  (fourier (m + n) : (a : AddCircle T) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)
⊢ (↑((m + n) • x).toCircle : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
rw [← fourier_apply]

Premises used: fourier_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n) : (a : AddCircle T) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
fourier_add

Premises used: fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n) : (a : AddCircle T) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
exact fourier_add

Premises used: fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
rw : Eq (α := ℝ) (⨆ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)) 1
⊢ norm (E := C(AddCircle T, ℂ)) (fourier n) = 1

Tactic:
rw [ContinuousMap.norm_eq_iSup_norm]

Premises used: ContinuousMap.norm_eq_iSup_norm
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
⊢ ∀ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) = 1

Tactic:
have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.norm_coe _
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) = 1
simp_rw : Eq (α := ℝ) (⨆ (x : AddCircle T), 1) 1
⊢ Eq (α := ℝ) (⨆ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)) 1

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) = 1
⊢ Eq (α := ℝ) (⨆ (x : AddCircle T), 1) 1

Tactic:
ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) = 1
⊢ Eq (α := ℝ) (⨆ (x : AddCircle T), 1) 1

Tactic:
exact ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
rw :
  (↑(n • x).toCircle : ℂ) * (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) =
    -(fourier n : (a : AddCircle T) → ℂ) x
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (x + (↑(T / 2 / (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ)
    (-(fourier n : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add,
    Metric.unitSphere.coe_mul]

Premises used: AddCircle.toCircle_add, Metric.unitSphere.coe_mul, zsmul_add, fourier_apply, QuotientAddGroup.mk_zsmul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
rw : Complex.exp ((↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) * Complex.I) = -1
⊢ (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) = -1

Tactic:
rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]

Premises used: zsmul_eq_mul, Function.Periodic.lift_coe, AddCircle.toCircle, Circle.coe_exp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ Complex.exp ((↑π : ℂ) * Complex.I) = -1

Tactic:
Complex.exp_pi_mul_I

Premises used: Complex.exp_pi_mul_I
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
h : (↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) = (↑π : ℂ)
⊢ Complex.exp ((↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) * Complex.I) = -1

Tactic:
convert! Complex.exp_pi_mul_I using 3

Premises used: Complex.exp_pi_mul_I
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) = (↑π : ℂ)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) = -1

Tactic:
have : (@toCircle T (n • (T / 2 / n) : ℝ) : ℂ) = -1 := by
    rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]
    convert! Complex.exp_pi_mul_I using 3
    field_simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) = -1
rw : (↑(n • x).toCircle : ℂ) * -1 = -(fourier n : (a : AddCircle T) → ℂ) x
⊢ (↑(n • x).toCircle : ℂ) * (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) =
    -(fourier n : (a : AddCircle T) → ℂ) x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) = -1
⊢ (↑(n • x).toCircle : ℂ) * -1 = -(fourier n : (a : AddCircle T) → ℂ) x

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
⊢ LE.le (α := Subalgebra ℂ C(AddCircle T, ℂ)) (adjoin ℂ (range fourier)) (star (adjoin ℂ (range fourier)))

Tactic:
adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
refine : range fourier ⊆ (↑(star (adjoin ℂ (range fourier))) : Set C(AddCircle T, ℂ))
⊢ LE.le (α := Subalgebra ℂ C(AddCircle T, ℂ)) (adjoin ℂ (range fourier)) (star (adjoin ℂ (range fourier)))

Tactic:
refine adjoin_le ?_

Premises used: Algebra.adjoin_le
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
⊢ fourier n ∈ (↑(star (adjoin ℂ (range fourier))) : Set C(AddCircle T, ℂ))

Tactic:
subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩

Premises used: iInf, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf, ContinuousMap.ext, Set.preimage, fourier_neg, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
⊢ fourier n ∈ (↑(star (adjoin ℂ (range fourier))) : Set C(AddCircle T, ℂ))

Tactic:
exact subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hs :
  (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ (↑(span ℂ (range fourier)) : Set C(AddCircle T, ℂ))
⊢ Eq (α := Submodule ℂ C(AddCircle T, ℂ))
    ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(AddCircle T, ℂ)) → Submodule ℂ C(AddCircle T, ℂ))
        (StarSubalgebra.toSubalgebra fourierSubalgebra) :
      Submodule ℂ C(AddCircle T, ℂ))
    (span ℂ (range fourier) : Submodule ℂ C(AddCircle T, ℂ))

Tactic:
apply adjoin_eq_span_of_subset

Premises used: Algebra.adjoin_eq_span_of_subset
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
⊢ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ (↑(span ℂ (range fourier)) : Set C(AddCircle T, ℂ))

Tactic:
Subset.trans ?_ Submodule.subset_span

Premises used: Set.Subset.trans, Submodule.subset_span
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hs : (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ range fourier
⊢ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ (↑(span ℂ (range fourier)) : Set C(AddCircle T, ℂ))

Tactic:
refine Subset.trans ?_ Submodule.subset_span

Premises used: Set.Subset.trans, Submodule.subset_span
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
⊢ Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) x

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

Premises used: Submonoid.closure_induction
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
hs : Eq (α := C(AddCircle T, ℂ)) (fourier 0) 1
hs₁ :
  ∀ (x y : C(AddCircle T, ℂ))
    (hx : Membership.mem (γ := Submonoid C(AddCircle T, ℂ)) (Submonoid.closure (range fourier)) x)
    (hy : Membership.mem (γ := Submonoid C(AddCircle T, ℂ)) (Submonoid.closure (range fourier)) y),
    Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) x →
      Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) y →
        Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) (x * y)
⊢ Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) x

Tactic:
refine Submonoid.closure_induction (fun _ => id) ⟨0, ?_⟩ ?_ hx
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
hs : ∀ (z : AddCircle T), Eq (α := ℂ) ((fourier 0 : (a : AddCircle T) → ℂ) z : ℂ) ((1 : (a : AddCircle T) → ℂ) z : ℂ)
⊢ Eq (α := C(AddCircle T, ℂ)) (fourier 0) 1

Tactic:
ext1 z
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
z : AddCircle T
⊢ Eq (α := ℂ) ((fourier 0 : (a : AddCircle T) → ℂ) z : ℂ) ((1 : (a : AddCircle T) → ℂ) z : ℂ)

Tactic:
fourier_zero

Premises used: fourier_zero
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
z : AddCircle T
⊢ Eq (α := ℂ) ((fourier 0 : (a : AddCircle T) → ℂ) z : ℂ) ((1 : (a : AddCircle T) → ℂ) z : ℂ)

Tactic:
exact fourier_zero

Premises used: fourier_zero
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
⊢ Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier)
    (HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n))

Tactic:
⟨m + n, ?_⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Exists.intro, Set.range
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
hs : fourier (m + n) = HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n)
⊢ Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier)
    (HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n))

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
hs :
  ∀ (z : AddCircle T),
    Eq (α := ℂ) ((fourier (m + n) : (a : AddCircle T) → ℂ) z : ℂ)
      ((HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n) : (a : AddCircle T) → ℂ) z : ℂ)
⊢ fourier (m + n) = HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n)

Tactic:
ext1 z
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
z : AddCircle T
⊢ Eq (α := ℂ) ((fourier (m + n) : (a : AddCircle T) → ℂ) z : ℂ)
    ((HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n) : (a : AddCircle T) → ℂ) z : ℂ)

Tactic:
fourier_add

Premises used: fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
z : AddCircle T
⊢ Eq (α := ℂ) ((fourier (m + n) : (a : AddCircle T) → ℂ) z : ℂ)
    ((HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n) : (a : AddCircle T) → ℂ) z : ℂ)

Tactic:
exact fourier_add

Premises used: fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ (f : AddCircle T → ℂ),
    Membership.mem (γ := Set (AddCircle T → ℂ))
        ((fun (f : C(AddCircle T, ℂ)) ↦ (⇑f : (a : AddCircle T) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra fourierSubalgebra) : Set C(AddCircle T, ℂ)))
        f ∧
      f x ≠ f y

Tactic:
⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩

Premises used: Algebra.subset_adjoin, fourier, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
refine :
  Ne (α := ℂ) ((fun (f : C(AddCircle T, ℂ)) ↦ ((⇑f : (a : AddCircle T) → ℂ) : (a : AddCircle T) → ℂ)) (fourier 1) x)
    ((fun (f : C(AddCircle T, ℂ)) ↦ ((⇑f : (a : AddCircle T) → ℂ) : (a : AddCircle T) → ℂ)) (fourier 1) y)
⊢ ∃ (f : AddCircle T → ℂ),
    Membership.mem (γ := Set (AddCircle T → ℂ))
        ((fun (f : C(AddCircle T, ℂ)) ↦ (⇑f : (a : AddCircle T) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra fourierSubalgebra) : Set C(AddCircle T, ℂ)))
        f ∧
      f x ≠ f y

Tactic:
refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
rw : (↑x.toCircle : ℂ) ≠ (↑y.toCircle : ℂ)
⊢ Ne (α := ℂ) ((fourier 1 : (a : AddCircle T) → ℂ) x : ℂ) ((fourier 1 : (a : AddCircle T) → ℂ) y : ℂ)

Tactic:
rw [fourier_one, fourier_one]

Premises used: fourier_one
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
contrapose : ∀ (hxy : (↑x.toCircle : ℂ) = (↑y.toCircle : ℂ)), x = y
⊢ (↑x.toCircle : ℂ) ≠ (↑y.toCircle : ℂ)

Tactic:
contrapose hxy
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : (↑x.toCircle : ℂ) = (↑y.toCircle : ℂ)
⊢ x.toCircle = y.toCircle

Tactic:
rw [Subtype.coe_inj] at hxy

Premises used: Subtype.coe_inj
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y

Tactic:
injective_toCircle hT.elim.ne' hxy

Premises used: AddCircle.injective_toCircle, LT.lt.ne', Fact.elim
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y

Tactic:
exact injective_toCircle hT.elim.ne' hxy

Premises used: AddCircle.injective_toCircle, LT.lt.ne', Fact.elim
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Eq (α := StarSubalgebra ℂ C(AddCircle T, ℂ)) (StarSubalgebra.topologicalClosure fourierSubalgebra) ⊤

Tactic:
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints fourierSubalgebra
    fourierSubalgebra_separatesPoints

Premises used: fourierSubalgebra_separatesPoints, fourierSubalgebra, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
rw :
  Eq (α := Submodule ℂ C(AddCircle T, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(AddCircle T, ℂ)) → Submodule ℂ C(AddCircle T, ℂ))
        (StarSubalgebra.toSubalgebra fourierSubalgebra)))
    ⊤
⊢ Eq (α := Submodule ℂ C(AddCircle T, ℂ)) (topologicalClosure (span ℂ (range fourier))) ⊤

Tactic:
rw [← fourierSubalgebra_coe]

Premises used: fourierSubalgebra_coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Eq (α := Submodule ℂ C(AddCircle T, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(AddCircle T, ℂ)) → Submodule ℂ C(AddCircle T, ℂ))
        (StarSubalgebra.toSubalgebra fourierSubalgebra)))
    ⊤

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

Premises used: iInf, StarSubalgebra.toSubalgebra, Set.Mem, Set.iInter, Set.univ, setOf, congr_arg, closure, Subalgebra.toSubmodule, fourierSubalgebra_closure_eq_top, Submodule.topologicalClosure, AddSubmonoid.topologicalClosure, Set.sInter, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Eq (α := Submodule ℂ C(AddCircle T, ℂ))
    (topologicalClosure
      ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(AddCircle T, ℂ)) → Submodule ℂ C(AddCircle T, ℂ))
        (StarSubalgebra.toSubalgebra fourierSubalgebra)))
    ⊤

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

Premises used: StarSubalgebra.toSubalgebra, congr_arg, Subalgebra.toSubmodule, fourierSubalgebra_closure_eq_top, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
n : ℤ
⊢ (↑(↑(fourierLp p n) : AddCircle T →ₘ[haarAddCircle] ℂ) :
      AddCircle T → ℂ) =ᶠ[ae (F := Measure (AddCircle T)) haarAddCircle]
    (⇑(fourier n) : (a : AddCircle T) → ℂ)

Tactic:
coeFn_toLp haarAddCircle (fourier n)

Premises used: fourier, AddCircle.haarAddCircle, ContinuousMap.coeFn_toLp