awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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)
    (∫ (b : AddCircle T),
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
        (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
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))
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))
rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (b : AddCircle T),
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
          (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
⊢ 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 =
  (1 / T) •
    HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
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))
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))
rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (b : AddCircle T),
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
          (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₃ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
⊢ 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 =
  (1 / T) •
    HSMul.hSMul (β := E) T
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
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))
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))
rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (b : AddCircle T),
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
          (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₃ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₄ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) T
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
⊢ 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) • T)
    (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
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))
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))
rw₂ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) (1 / T)
      (∫ (b : AddCircle T),
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) b : ℂ)
          (f b) ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₃ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₄ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    (1 / T) •
      HSMul.hSMul (β := E) T
        (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
rw₅ :
  ∫ (t : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) t : ℂ) (f t) ∂haarAddCircle =
    HSMul.hSMul (β := E) ((1 / T) • T)
      (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
⊢ 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 * T)
    (∫ (x : AddCircle T), HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) (f x) ∂haarAddCircle)
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
hf : Integrable f haarAddCircle
n : ℤ
⊢ Integrable.{u_1, 0} (ε := E)
    (fun (t : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) (f t)) haarAddCircle
have hφ1 : AEStronglyMeasurable (α := AddCircle T) (β := ℂ) (⇑(fourier n) : (a : AddCircle T) → ℂ) haarAddCircle
Tactic: apply hf.bdd_smul 1
-- 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
hf : Integrable f haarAddCircle
n : ℤ
hφ1 : AEStronglyMeasurable (α := AddCircle T) (β := ℂ) (⇑(fourier n) : (a : AddCircle T) → ℂ) haarAddCircle
⊢ Integrable.{u_1, 0} (ε := E)
    (fun (t : AddCircle T) ↦ HSMul.hSMul (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) (f t)) haarAddCircle
have hφ2 : ∀ᵐ (a : AddCircle T) ∂haarAddCircle, Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1
Tactic: apply hf.bdd_smul 1
-- 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
hf : Integrable f haarAddCircle
n : ℤ
⊢ ∀ᵐ (a : AddCircle T) ∂haarAddCircle, Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1
have hφ2 : ∀ (a : AddCircle T), Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) a : ℂ) ≤ 1
Tactic: apply ae_of_all
-- 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
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
⊢ Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) ≤ 1
have hφ2 : ‖(↑(n • t).toCircle : ℂ)‖ ≤ 1
Tactic: rw [fourier_apply, Circle.norm_coe]
-- 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
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
hφ2 : ‖(↑(n • t).toCircle : ℂ)‖ ≤ 1
⊢ Norm.norm (E := ℂ) ((fourier n : (a : AddCircle T) → ℂ) t : ℂ) ≤ 1
have hφ2₁ : LE.le (α := ℝ) 1 1
Tactic: rw [fourier_apply, Circle.norm_coe]
-- 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 g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
⊢ fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g
have h : ∀ (x : ℤ), fourierCoeff (f + g) x = (fourierCoeff f + fourierCoeff g) x
Tactic: ext x
-- 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
ι : Type u_2
f : ι → AddCircle T → E
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))
have empty : ∀ (x : ℤ), Eq.{u_1 + 1} (α := E) (fourierCoeff (T := T) (∑ i ∈ ∅, f i) x) ((∑ i ∈ ∅, fourierCoeff (f i)) x)
Tactic: ext
-- 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
ι : 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
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, fourierCoeff (f i))
have hf₁ : Integrable (f a) haarAddCircle
Tactic: obtain ⟨hf₁, hf₂⟩ := by simpa using hf
-- 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
ι : 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
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, fourierCoeff (f i))
have hf₂ : ∀ a ∈ s, Integrable (f a) haarAddCircle
Tactic: obtain ⟨hf₁, hf₂⟩ := by simpa using hf
-- 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
ι : 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
hf₂ : ∀ a ∈ s, Integrable (f a) haarAddCircle
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, fourierCoeff (f i))
have insert : fourierCoeff (f a + ∑ x ∈ s, f x) = ∑ i ∈ 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₂]
-- 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
ι : 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)
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
    (∑ i ∈ Insert.insert a s, fourierCoeff (f i))
have insert₁ : fourierCoeff (f a + ∑ x ∈ s, f x) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
Tactic: rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]
-- 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
ι : 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)
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
    (∑ i ∈ Insert.insert a s, fourierCoeff (f i))
have insert₂ : fourierCoeff (f a) + fourierCoeff (T := T) (∑ i ∈ s, f i) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
Tactic: rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]
-- 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
ι : 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)
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ Insert.insert a s, f i))
    (∑ i ∈ Insert.insert a s, fourierCoeff (f i))
have insert₃ : fourierCoeff (f a) + ∑ i ∈ s, fourierCoeff (f i) = fourierCoeff (f a) + ∑ x ∈ s, fourierCoeff (f x)
Tactic: rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]
-- 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
ι : Type u_2
s : Finset ι
f : ι → AddCircle T → E
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))
have 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))
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₂]
Cleared hypotheses: s, hf
-- 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
ι : 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))
⊢ Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ s, f i)) (∑ i ∈ s, fourierCoeff (f i))
have 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 a s, Integrable (f i) haarAddCircle),
  Eq.{u_1 + 1} (α := (n : ℤ) → E) (fourierCoeff (T := T) (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a 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₂]
Cleared hypotheses: s, hf