awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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))⁻¹ : ℂ)
⊢ (↑(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)) :
        ℂ)
have H₂ : Eq (α := ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -n • z)) : ℂ)
  (↑((Circle.exp : (a : ℝ) → Circle) (-(2 * π / T * n • z))) : ℂ)
Tactic: simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
    neg_smul, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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))) : ℂ)
⊢ (↑(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)) :
        ℂ)
have H₃ : Eq (α := ℂ) (↑((Circle.exp : (a : ℝ) → Circle) (2 * π / T * -(n • z))) : ℂ)
  (↑((Circle.exp : (a : ℝ) → Circle) (-(2 * π / T * n • z))) : ℂ)
Tactic: simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
    neg_smul, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (↑(-(n • x)).toCircle : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)
have rw : Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)
Tactic: rw [← neg_smul, ← fourier_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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 : ℂ)
have simp_rw : (↑((m + n) • x).toCircle : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
Tactic: simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
simp_rw : (↑((m + 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 : ℂ)
have simp_rw₁ : (↑(m • x + n • x).toCircle : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
Tactic: simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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 : ℂ)
⊢ (fourier (m + n) : (a : AddCircle T) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)
have simp_rw₂ : (↑((m • x).toCircle * (n • x).toCircle) : ℂ) = (↑(m • x).toCircle : ℂ) * (↑(n • x).toCircle : ℂ)
Tactic: simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (↑((m + n) • x).toCircle : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)
have rw : (fourier (m + n) : (a : AddCircle T) → ℂ) x =
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier m : (a : AddCircle T) → ℂ) x : ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)
Tactic: rw [← fourier_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
⊢ norm (E := C(AddCircle T, ℂ)) (fourier n) = 1
have rw : Eq (α := ℝ) (⨆ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)) 1
Tactic: rw [ContinuousMap.norm_eq_iSup_norm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
⊢ Eq (α := ℝ) (⨆ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)) 1
have this : ∀ (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 _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
inst : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) = 1
⊢ Eq (α := ℝ) (⨆ (x : AddCircle T), norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ)) 1
have simp_rw : Eq (α := ℝ) (⨆ (x : AddCircle T), 1) 1
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (x + (↑(T / 2 / (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ)
    (-(fourier n : (a : AddCircle T) → ℂ) x : ℂ)
have rw : (↑(n • x).toCircle : ℂ) * (↑(toCircle (T := T) (↑(n • (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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) = -1
have rw : Complex.exp ((↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) * Complex.I) = -1
Tactic: rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ Complex.exp ((↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) * Complex.I) = -1
have h : (↑(2 * π / T * ((↑n : ℝ) * (T / 2 / (↑n : ℝ)))) : ℂ) = (↑π : ℂ)
Tactic: convert! Complex.exp_pi_mul_I using 3
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (↑(n • x).toCircle : ℂ) * (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) =
    -(fourier n : (a : AddCircle T) → ℂ) x
have this : (↑(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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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 : ℂ) * (↑(toCircle (T := T) (↑(n • (T / 2 / (↑n : ℝ))) : ℝ ⧸ AddSubgroup.zmultiples T)) : ℂ) =
    -(fourier n : (a : AddCircle T) → ℂ) x
have rw : (↑(n • x).toCircle : ℂ) * -1 = -(fourier n : (a : AddCircle T) → ℂ) x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
⊢ LE.le (α := Subalgebra ℂ C(AddCircle T, ℂ)) (adjoin ℂ (range fourier)) (star (adjoin ℂ (range fourier)))
have refine : range fourier ⊆ (↑(star (adjoin ℂ (range fourier))) : Set C(AddCircle T, ℂ))
Tactic: refine adjoin_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
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, ℂ))
have hs : (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ (↑(span ℂ (range fourier)) : Set C(AddCircle T, ℂ))
Tactic: apply adjoin_eq_span_of_subset
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
⊢ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ (↑(span ℂ (range fourier)) : Set C(AddCircle T, ℂ))
have hs : (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ)) ⊆ range fourier
Tactic: refine Subset.trans ?_ Submodule.subset_span
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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
have hs : Eq (α := C(AddCircle T, ℂ)) (fourier 0) 1
Tactic: refine Submonoid.closure_induction (fun _ => id) ⟨0, ?_⟩ ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
hs : Eq (α := C(AddCircle T, ℂ)) (fourier 0) 1
⊢ Membership.mem (γ := Set C(AddCircle T, ℂ)) (range fourier) x
have 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)
Tactic: refine Submonoid.closure_induction (fun _ => id) ⟨0, ?_⟩ ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
⊢ Eq (α := C(AddCircle T, ℂ)) (fourier 0) 1
have hs : ∀ (z : AddCircle T), Eq (α := ℂ) ((fourier 0 : (a : AddCircle T) → ℂ) z : ℂ) ((1 : (a : AddCircle T) → ℂ) z : ℂ)
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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))
have hs : fourier (m + n) = HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n)
Tactic: refine ⟨m + n, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ (↑(Submonoid.closure (range fourier)) : Set C(AddCircle T, ℂ))
m n : ℤ
⊢ fourier (m + n) = HMul.hMul (α := C(AddCircle T, ℂ)) (fourier m) (fourier n)
have 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 : ℂ)
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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
have 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)
Tactic: refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ Ne (α := ℂ) ((fourier 1 : (a : AddCircle T) → ℂ) x : ℂ) ((fourier 1 : (a : AddCircle T) → ℂ) y : ℂ)
have rw : (↑x.toCircle : ℂ) ≠ (↑y.toCircle : ℂ)
Tactic: rw [fourier_one, fourier_one]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (↑x.toCircle : ℂ) ≠ (↑y.toCircle : ℂ)
have contrapose : ∀ (hxy : (↑x.toCircle : ℂ) = (↑y.toCircle : ℂ)), x = y
Tactic: contrapose hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : (↑x.toCircle : ℂ) = (↑y.toCircle : ℂ)
⊢ x = y
have hxy₁ : x.toCircle = y.toCircle
Tactic: rw [Subtype.coe_inj] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Eq (α := Submodule ℂ C(AddCircle T, ℂ)) (topologicalClosure (span ℂ (range fourier))) ⊤
have rw : Eq (α := Submodule ℂ C(AddCircle T, ℂ))
  (topologicalClosure
    ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(AddCircle T, ℂ)) → Submodule ℂ C(AddCircle T, ℂ))
      (StarSubalgebra.toSubalgebra fourierSubalgebra)))
  ⊤
Tactic: rw [← fourierSubalgebra_coe]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (topologicalClosure (span ℂ (range (fourierLp p)))) ⊤
have h : Complex.instSemiring = Ring.toSemiring →
  HEq (α := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule (β := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule →
    Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (span ℂ (range (fourierLp p)))
      (Submodule.map (↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle))
        (span ℂ (range fourier)))
Tactic: convert!
    (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
      span_fourier_closure_eq_top
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
hp : p ≠ ∞
e_3 : Complex.instSemiring = Ring.toSemiring
e_6 : HEq (α := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule (β := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (span ℂ (range (fourierLp p)))
    (Submodule.map (↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle))
      (span ℂ (range fourier)))
have h : Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (span ℂ (range (fourierLp p)))
  (span ℂ
    (image (α := C(AddCircle T, ℂ))
      (⇑(↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle)) :
        (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ p haarAddCircle))
      (range fourier)))
Tactic: rw [map_span]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
hp : p ≠ ∞
e_3 : Complex.instSemiring = Ring.toSemiring
e_6 : HEq (α := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule (β := Module ℂ ↥(Lp ℂ p haarAddCircle)) Lp.instModule
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle))
    (span ℂ
      (range fun (n : ℤ) ↦ (toLp p haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ p haarAddCircle)) (fourier n)))
    (span ℂ
      (image (α := C(AddCircle T, ℂ))
        (⇑(↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle)) :
          (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ p haarAddCircle))
        (range fourier)))
have h : Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle))
  (span ℂ
    (image (α := C(AddCircle T, ℂ)) (⇑(toLp p haarAddCircle ℂ) : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ p haarAddCircle))
      (range fourier)))
  (span ℂ
    (image (α := C(AddCircle T, ℂ))
      (⇑(↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle)) :
        (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ p haarAddCircle))
      (range fourier)))
Tactic: rw [range_comp']
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Orthonormal ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2)
have rw : ∀ (i j : ℤ), inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
have rw : Eq (α := ℂ)
  (∫ (x : AddCircle T),
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier j : (a : AddCircle T) → ℂ) x : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) x : ℂ) : ℂ) ∂haarAddCircle)
  (if i = j then 1 else 0)
Tactic: rw [ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ Eq (α := ℂ)
    (∫ (x : AddCircle T),
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier j : (a : AddCircle T) → ℂ) x : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) x : ℂ) : ℂ) ∂haarAddCircle)
    (if i = j then 1 else 0)
have simp_rw : Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) (if i = j then 1 else 0)
Tactic: simp_rw [← fourier_neg, ← fourier_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle)
    (if i = j then 1 else 0)
have pos : ∀ (h : i = j), Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
pos : ∀ (h : i = j), Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 1
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle)
    (if i = j then 1 else 0)
have neg : ∀ (h : ¬i = j), Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 0
have hij : j + -i ≠ 0
Tactic: have hij : j + -i ≠ 0 := by
    exact sub_ne_zero.mpr (Ne.symm h)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ fourierCoeff f n =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
          (f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
have this : ∀ (x : ℝ),
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
    (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
      (↑x : ℝ ⧸ AddSubgroup.zmultiples T)
Tactic: have : ∀ x : ℝ, @fourier T (-n) x • f x = (fun z : AddCircle T => @fourier T (-n) z • f z) x := by
    intro x; rfl
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this :
  ∀ (x : ℝ),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
      (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
        (↑x : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ fourierCoeff f n =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
          (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
have rw : ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
  HSMul.hSMul (β := E) (1 / T)
    (∫ (x : ℝ) in a..a + T,
      (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
        (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
Tactic: rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
    volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this :
  ∀ (x : ℝ),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
      (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
        (↑x : ℝ ⧸ AddSubgroup.zmultiples T)
rw :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
          (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
⊢ fourierCoeff f n =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        (fun (z : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) z : ℂ) (f z))
          (↑x : ℝ ⧸ AddSubgroup.zmultiples T))
have rw₁ : ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
  HSMul.hSMul (β := E) (1 / T)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : AddCircle T) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ) (f b))
Tactic: rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
    volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]