awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle))
    (topologicalClosure
      (Submodule.map (↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle))
        (span ℂ (range fourier))))
    ⊤

Tactic:
(ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
      span_fourier_closure_eq_top

Premises used: span_fourier_closure_eq_top, ContinuousMap.toLp_denseRange, DenseRange.topologicalClosure_map_submodule, AddCircle.haarAddCircle, Complex
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst : Fact (1 ≤ p)
hp : p ≠ ∞
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)))
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (topologicalClosure (span ℂ (range (fourierLp p)))) ⊤

Tactic:
convert!
    (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
      span_fourier_closure_eq_top

Premises used: span_fourier_closure_eq_top, ContinuousMap.toLp_denseRange, DenseRange.topologicalClosure_map_submodule, AddCircle.haarAddCircle, Complex
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
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)))
⊢ Eq (α := Submodule ℂ ↥(Lp ℂ p haarAddCircle)) (span ℂ (range (fourierLp p)))
    (Submodule.map (↑(toLp p haarAddCircle ℂ) : C(AddCircle T, ℂ) →ₗ[ℂ] ↥(Lp ℂ p haarAddCircle))
      (span ℂ (range fourier)))

Tactic:
rw [map_span]

Premises used: Submodule.map_span
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
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)))
⊢ 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)))

Tactic:
rw [range_comp']

Premises used: Set.range_comp'
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 ℂ
      (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:
simp only [ContinuousLinearMap.coe_coe]

Premises used: ContinuousLinearMap.coe_coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
rw : ∀ (i j : ℤ), inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
⊢ Orthonormal ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2)

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
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)
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0

Tactic:
rw [ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)]

Premises used: fourier, AddCircle.haarAddCircle, MeasureTheory.ContinuousMap.inner_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
simp_rw :
  Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle)
    (if i = j then 1 else 0)
⊢ 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:
simp_rw [← fourier_neg, ← fourier_add]

Premises used: fourier_neg, fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
neg : ∀ (h : ¬i = j), Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 0
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle)
    (if i = j then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Tactic:
sub_ne_zero.mpr (Ne.symm h)

Premises used: Iff.mpr, sub_ne_zero, Ne.symm, Int.sub
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Tactic:
exact sub_ne_zero.mpr (Ne.symm h)

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Tactic:
have hij : j + -i ≠ 0 := by
    exact sub_ne_zero.mpr (Ne.symm h)
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : j + -i ≠ 0
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 0

Tactic:
integral_eq_zero_of_add_right_eq_neg (μ := haarAddCircle)
      (fourier_add_half_inv_index hij hT.elim)

Premises used: MeasureTheory.integral_eq_zero_of_add_right_eq_neg, Fact.elim, fourier_add_half_inv_index
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : j + -i ≠ 0
⊢ Eq (α := ℂ) (∫ (x : AddCircle T), (fourier (j + -i) : (a : AddCircle T) → ℂ) x ∂haarAddCircle) 0

Tactic:
convert!
    integral_eq_zero_of_add_right_eq_neg (μ := haarAddCircle)
      (fourier_add_half_inv_index hij hT.elim)

Premises used: MeasureTheory.integral_eq_zero_of_add_right_eq_neg, Fact.elim, fourier_add_half_inv_index
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a 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:
rfl
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ ∀ (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
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
simp_rw :
  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))
⊢ 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)))

Tactic:
simp_rw +singlePass [this]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
hφ1 : AEStronglyMeasurable (α := AddCircle T) (β := ℂ) (⇑(fourier n) : (a : AddCircle T) → ℂ) haarAddCircle
hφ2 : ∀ᵐ (a : AddCircle T) ∂haarAddCircle, Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1
⊢ Integrable.{u_1, 0} (ε := E)
    (fun (t : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) (f t)) haarAddCircle

Tactic:
apply hf.bdd_smul 1

Premises used: MeasureTheory.Integrable.bdd_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ AEStronglyMeasurable (α := AddCircle T) (β := ℂ) (⇑(fourier n) : (a : AddCircle T) → ℂ) haarAddCircle

Tactic:
(map_continuous (fourier n)).aestronglyMeasurable

Premises used: fourier, ContinuousMapClass.map_continuous, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ AEStronglyMeasurable (α := AddCircle T) (β := ℂ) (⇑(fourier n) : (a : AddCircle T) → ℂ) haarAddCircle

Tactic:
exact (map_continuous (fourier n)).aestronglyMeasurable

Premises used: fourier, ContinuousMapClass.map_continuous, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
hφ2 : ∀ (a : AddCircle T), Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1
⊢ ∀ᵐ (a : AddCircle T) ∂haarAddCircle, Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1

Tactic:
apply ae_of_all

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
hφ2 : ‖(↑(n • t).toCircle : ℂ)‖ ≤ 1
hφ2₁ hφ2₂ : LE.le (α := ℝ) 1 1
⊢ Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) ≤ 1

Tactic:
rw [fourier_apply, Circle.norm_coe]

Premises used: Circle.norm_coe, fourier_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
h : ∀ (x : ℤ), fourierCoeff (f + g) x = (fourierCoeff f + fourierCoeff g) x
⊢ fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g

Tactic:
ext x
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
x : ℤ
⊢ fourierCoeff (f + g) x = (fourierCoeff f + fourierCoeff g) x

Tactic:
simpa [fourierCoeff, -fourier_apply] using integral_add (hf.fourier_smul _) (hg.fourier_smul _)

Premises used: fourierCoeff, fourier_apply, MeasureTheory.Integrable.fourier_smul, MeasureTheory.integral_add
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) haarAddCircle
empty : ∀ (x : ℤ), Eq.{u_1 + 1} (α := E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i) x) ((∑ i ∈ ∅, fourierCoeff (f i)) x)
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, fourierCoeff (f i))

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) haarAddCircle
x : ℤ
⊢ Eq.{u_1 + 1} (α := E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i) x) ((∑ i ∈ ∅, fourierCoeff (f i)) x)

Tactic:
simp [fourierCoeff]

Premises used: fourierCoeff
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))
hf : ∀ i ∈ insert a s, Integrable (f i) haarAddCircle
⊢ Integrable (f a) haarAddCircle ∧ ∀ a ∈ s, Integrable (f a) haarAddCircle

Tactic:
simpa using hf
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))
hf : ∀ i ∈ insert a s, Integrable (f i) haarAddCircle
⊢ Integrable (f a) haarAddCircle

Tactic:
obtain ⟨hf₁, hf₂⟩ := by simpa using hf
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))
hf : ∀ i ∈ insert a s, Integrable (f i) haarAddCircle
hf₁ : Integrable (f a) haarAddCircle
⊢ ∀ a ∈ s, Integrable (f a) haarAddCircle

Tactic:
obtain ⟨hf₁, hf₂⟩ := by simpa using hf
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))
hf : ∀ i ∈ Insert.insert a s, Integrable (f i) haarAddCircle
hf₁ : Integrable (f a) haarAddCircle
hf₂ : ∀ a ∈ s, Integrable (f a) haarAddCircle
insert : fourierCoeff (f a + ∑ x ∈ s, f x) = ∑ i ∈ Insert.insert a s, fourierCoeff (f i)
insert₁ : fourierCoeff (f a + ∑ x ∈ s, f x) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
insert₂ : fourierCoeff (f a) + fourierCoeff (T := T) (∑ i ∈ s, f i) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
insert₃ insert₄ : fourierCoeff (f a) + ∑ i ∈ s, fourierCoeff (f i) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
    (∑ i ∈ Insert.insert a s, fourierCoeff (f i))

Tactic:
rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]

Premises used: MeasureTheory.integrable_finsetSum', fourierCoeff.add, Finset.sum_insert
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
s : Finset ι
f : ι → AddCircle T → E
hf : ∀ i ∈ s, Integrable (f i) haarAddCircle
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, fourierCoeff (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (iha :
      ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
        Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i)))
    (hf : ∀ i ∈ Insert.insert a s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
      (∑ i ∈ Insert.insert a s, fourierCoeff (f i))
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))

Tactic:
induction s using Finset.induction_on with
  | empty => ext; simp [fourierCoeff]
  | insert a s ha iha =>
      obtain ⟨hf₁, hf₂⟩ := by simpa using hf
      rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]

Premises used: fourierCoeff, Insert.insert
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
s : Finset ι
f : ι → AddCircle T → E
hf : ∀ i ∈ s, Integrable (f i) haarAddCircle
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, fourierCoeff (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (iha :
      ∀ (hf : ∀ i ∈ s, Integrable (f i) haarAddCircle),
        Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i)))
    (hf : ∀ i ∈ Insert.insert a s, Integrable (f i) haarAddCircle),
    Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
      (∑ i ∈ Insert.insert a s, fourierCoeff (f i))
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => ext; simp [fourierCoeff]
  | insert a s ha iha =>
      obtain ⟨hf₁, hf₂⟩ := by simpa using hf
      rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]

Premises used: fourierCoeff, Insert.insert
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : AddCircle T → E
c : ℂ
n : ℤ
simp_rw :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) ((c • f) t) ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₁ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (c • f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) c • f t ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₃ :
  ∫ (t : AddCircle T), HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) c • f t ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₄ :
  ∫ (t : AddCircle T), HMul.hMul (β := ℂ) c ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) • f t ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₅ :
  ∫ (t : AddCircle T), HSMul.hSMul (β := ℂ) c ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) • f t ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
simp_rw₆ :
  ∫ (t : AddCircle T), c • HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) c
      (∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n

Tactic:
simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_smul]

Premises used: fourierCoeff, smul_assoc, MeasureTheory.integral_smul, mul_comm, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
c : ℂ
n : ℤ
⊢ fourierCoeff (T := T) (fun (x : AddCircle T) ↦ c * f x) n = c * fourierCoeff f n

Tactic:
fourierCoeff.const_smul f c n

Premises used: fourierCoeff.const_smul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : AddCircle T → E
h : f =ᶠ[ae (F := Measure (AddCircle T)) haarAddCircle] g
⊢ fourierCoeff f = fourierCoeff g

Tactic:
funext fun _ ↦ integral_congr_ae <| .smul (.refl _ _) h

Premises used: MeasureTheory.ae, MeasureTheory.integral_congr_ae, Filter.EventuallyEq.smul, fourier, funext, Filter.EventuallyEq.refl, AddCircle.haarAddCircle, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f : ℝ → E
n : ℤ
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ Fact (0 < b - a)

Tactic:
haveI := Fact.mk (by linarith : 0 < b - a)