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
ι : 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: 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₂]
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: 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₂]
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
f : AddCircle T → E
c : ℂ
n : ℤ
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
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)
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
have 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)
Tactic: simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
    smul_assoc, integral_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
a b : ℝ
hab : a < b
f : ℝ → E
n : ℤ
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab f n =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))
have this : Fact (0 < b - a)
Tactic: haveI := Fact.mk (by linarith : 0 < b - a)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))
have rw : HSMul.hSMul (β := E) (1 / (b - a))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)))) =
  HSMul.hSMul (β := E) (1 / (b - a))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
Tactic: rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)))) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))
have e_a : Eq.{u_1 + 1} (α := E)
  (∫ (x : ℝ) in a..b,
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
  (∫ (x : ℝ) in a..b,
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
have e_a : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x))
Tactic: simp_rw [intervalIntegral.integral_of_le hab.le]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
have e_a : ∀ (x : ℝ) (hx : x ∈ Ioc a b),
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x)
Tactic: refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x)
have e_a : x ∈ Ioc a (a + (b - a))
Tactic: rw [liftIoc_coe_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))
have e_a : x ∈ Ioc a (a + b - a)
Tactic: rwa [add_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
have this : Fact (0 < b - a)
Tactic: haveI := Fact.mk (by linarith : 0 < b - a)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
⊢ fourierCoeffOn hab f = fourierCoeffOn hab g
have h₁ : ∀ (n : ℤ), fourierCoeffOn hab f n = fourierCoeffOn hab g n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
⊢ fourierCoeffOn hab f n = fourierCoeffOn hab g n
have h₁ : HSMul.hSMul (β := E) (1 / (b - a))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x)) =
  HSMul.hSMul (β := E) (1 / (b - a))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (g x))
Tactic: rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
⊢ HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (g x))
have h₁ : Eq.{u_1 + 1} (α := E)
  (∫ (x : ℝ) in a..b,
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x))
  (∫ (x : ℝ) in a..b,
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x))
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (g x))
have h₁ : Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b)))
  (fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x))
  fun (x : ℝ) ↦
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (g x)
Tactic: apply intervalIntegral.integral_congr_ae_restrict
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b)))
    (fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)
have h₁ : Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b)))
  (fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x))
  fun (x : ℝ) ↦
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (g x)
Tactic: simp only [uIoc_of_le hab.le]