awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
H : LocallyIntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F)
⊢ Integrable (⇑f : (a : E) → F) μ
have rw : IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
Tactic: rw [← integrableOn_iff_integrable_of_support_subset (subset_tsupport f)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
H : LocallyIntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F)
⊢ IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
have H₁ : IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (tsupport (⇑f : (a : E) → F)) μ
Tactic: replace H := H.integrableOn_compact_subset f.tsupport_subset f.hasCompactSupport
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
H : IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (tsupport (⇑f : (a : E) → F)) μ
⊢ IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
have suffices : IntegrableOn (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
Tactic: suffices IntegrableOn ((1 : ℝ) • f) (tsupport f) μ by simpa
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
H : IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (tsupport (⇑f : (a : E) → F)) μ
⊢ IntegrableOn (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
have rw : ∀ (H : MemLp (ε := ℝ) (fun (x : E) ↦ 1) 1 (μ.restrict (tsupport (⇑f : (a : E) → F)))),
  MemLp (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) 1 (μ.restrict (tsupport (⇑f : (a : E) → F)))
Tactic: rw [IntegrableOn, ← memLp_one_iff_integrable] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
m : MeasurableSpace E
inst_9 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_10 : NormedAddCommGroup F₁
inst_11 : NormedSpace 𝕜 F₁
inst_12 : NormedSpace ℝ F₁
inst_13 : NormedAddCommGroup F₂
inst_14 : NormedSpace 𝕜 F₂
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : Algebra ℝ 𝕜
inst_18 : IsScalarTower ℝ 𝕜 F₁
inst_19 : NormedSpace ℝ F₃
inst_20 : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_8 + 1} (α := F₃)
    ((fun (f : 𝓓^{n}(Ω, F₁)) ↦
          (if LocallyIntegrableOn φ (↑Ω : Set E) μ then
              ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
            else 0 :
            F₃))
        (ofSupportedIn K_sub_Ω f) :
      F₃)
    (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
              (if LocallyIntegrableOn φ (↑Ω : Set E) μ then ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ
                else 0 :
                𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃))
            K K_sub_Ω :
          (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
        f :
      F₃)
have pos : ∀ (h : LocallyIntegrableOn φ (↑Ω : Set E) μ),
  Eq.{u_8 + 1} (α := F₃)
    ((fun (f : 𝓓^{n}(Ω, F₁)) ↦
          (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ :
            F₃))
        (ofSupportedIn K_sub_Ω f) :
      F₃)
    (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
              (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ : 𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃))
            K K_sub_Ω :
          (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
        f :
      F₃)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
m : MeasurableSpace E
inst_9 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_10 : NormedAddCommGroup F₁
inst_11 : NormedSpace 𝕜 F₁
inst_12 : NormedSpace ℝ F₁
inst_13 : NormedAddCommGroup F₂
inst_14 : NormedSpace 𝕜 F₂
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : Algebra ℝ 𝕜
inst_18 : IsScalarTower ℝ 𝕜 F₁
inst_19 : NormedSpace ℝ F₃
inst_20 : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F₁)
pos :
  ∀ (h : LocallyIntegrableOn φ (↑Ω : Set E) μ),
    Eq.{u_8 + 1} (α := F₃)
      ((fun (f : 𝓓^{n}(Ω, F₁)) ↦
            (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ :
              F₃))
          (ofSupportedIn K_sub_Ω f) :
        F₃)
      (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
                (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ : 𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃))
              K K_sub_Ω :
            (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
          f :
        F₃)
⊢ Eq.{u_8 + 1} (α := F₃)
    ((fun (f : 𝓓^{n}(Ω, F₁)) ↦
          (if LocallyIntegrableOn φ (↑Ω : Set E) μ then
              ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
            else 0 :
            F₃))
        (ofSupportedIn K_sub_Ω f) :
      F₃)
    (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
              (if LocallyIntegrableOn φ (↑Ω : Set E) μ then ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ
                else 0 :
                𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃))
            K K_sub_Ω :
          (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
        f :
      F₃)
have neg : ∀ (h : ¬LocallyIntegrableOn φ (↑Ω : Set E) μ),
  Eq.{u_8 + 1} (α := F₃) ((fun (f : 𝓓^{n}(Ω, F₁)) ↦ (0 : F₃)) (ofSupportedIn K_sub_Ω f) : F₃)
    (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦ (0 : 𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃)) K K_sub_Ω :
          (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
        f :
      F₃)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F₁
inst_13 : NormedSpace ℝ F₃
inst_14 : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : ¬LocallyIntegrableOn φ (↑Ω : Set E) μ
⊢ Eq (α := 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) (integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) (0 : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃)
have h : ∀ (x : 𝓓^{n}(Ω, F₁)),
  Eq.{u_8 + 1} (α := F₃) (((integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) : (a : 𝓓^{n}(Ω, F₁)) → F₃) x : F₃)
    ((0 : (a : 𝓓^{n}(Ω, F₁)) → F₃) x : F₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F₁
inst_13 : NormedSpace ℝ F₃
inst_14 : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_8 + 1} (α := F₃)
    (((integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) : (a : 𝓓^{n}(Ω, F₁)) → F₃) (ofSupportedIn K_sub_Ω f) : F₃)
    ((ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
have hφ' : IntegrableOn φ (↑K : Set E) μ
Tactic: have hφ' := hφ.integrableOn_compact_subset K_sub_Ω K.isCompact
-- 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
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : AddCircle T) ↦ f t)
have rw : ∫ (t : AddCircle T), f t ∂haarAddCircle =
  HSMul.hSMul (β := E) T⁻¹
    (∫ (t : AddCircle T), f t ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
Tactic: rw [volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    inv_smul_smul₀ hT.out.ne']
-- 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
rw :
  ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹
      (∫ (t : AddCircle T), f t ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : AddCircle T) ↦ f t)
have rw₁ : ∫ (t : AddCircle T), f t ∂haarAddCircle =
  T⁻¹ • HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal (∫ (x : AddCircle T), f x ∂haarAddCircle)
Tactic: rw [volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    inv_smul_smul₀ hT.out.ne']
-- 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
rw :
  ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹
      (∫ (t : AddCircle T), f t ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₁ :
  ∫ (t : AddCircle T), f t ∂haarAddCircle =
    T⁻¹ • HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal (∫ (x : AddCircle T), f x ∂haarAddCircle)
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : AddCircle T) ↦ f t)
have rw₂ : ∫ (t : AddCircle T), f t ∂haarAddCircle = T⁻¹ • HSMul.hSMul (β := E) T (∫ (x : AddCircle T), f x ∂haarAddCircle)
Tactic: rw [volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    inv_smul_smul₀ hT.out.ne']
-- 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
rw :
  ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹
      (∫ (t : AddCircle T), f t ∂HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle)
rw₁ :
  ∫ (t : AddCircle T), f t ∂haarAddCircle =
    T⁻¹ • HSMul.hSMul (β := E) (ENNReal.ofReal T).toReal (∫ (x : AddCircle T), f x ∂haarAddCircle)
rw₂ : ∫ (t : AddCircle T), f t ∂haarAddCircle = T⁻¹ • HSMul.hSMul (β := E) T (∫ (x : AddCircle T), f x ∂haarAddCircle)
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle =
    HSMul.hSMul (β := E) T⁻¹ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : AddCircle T) ↦ f t)
have rw₃ : Eq.{u_1 + 1} (α := E) (∫ (t : AddCircle T), f t ∂haarAddCircle) (∫ (x : AddCircle T), f x ∂haarAddCircle)
Tactic: rw [volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    inv_smul_smul₀ hT.out.ne']
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
⊢ MemLp f p AddCircle.haarAddCircle ↔
    MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
have hT' : 0 < T
Tactic: have hT' := hT.out
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
⊢ MemLp f p AddCircle.haarAddCircle ↔
    MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
have refine : ∀ (h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)),
  MemLp f p AddCircle.haarAddCircle
Tactic: refine ⟨fun h ↦ h.smul_measure (by finiteness), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
⊢ MemLp f p AddCircle.haarAddCircle
have this : MemLp f p ((ENNReal.ofReal T)⁻¹ • HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
Tactic: have := h.smul_measure (c := (ENNReal.ofReal T)⁻¹) (by finiteness)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
this :
  MemLp f p ((ENNReal.ofReal T)⁻¹ • HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
⊢ MemLp f p AddCircle.haarAddCircle
have rwa : ∀
  (this :
    MemLp f p
      (HSMul.hSMul (β := Measure (AddCircle T)) ((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) AddCircle.haarAddCircle)),
  MemLp f p AddCircle.haarAddCircle
Tactic: rwa [smul_smul, ENNReal.inv_mul_cancel (by positivity) (by finiteness), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
this :
  MemLp f p ((ENNReal.ofReal T)⁻¹ • HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
rwa :
  ∀
    (this :
      MemLp f p
        (HSMul.hSMul (β := Measure (AddCircle T)) ((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) AddCircle.haarAddCircle)),
    MemLp f p AddCircle.haarAddCircle
⊢ MemLp f p AddCircle.haarAddCircle
have rwa₁ : ∀ (this : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (AddCircle T)) 1 AddCircle.haarAddCircle)),
  MemLp f p AddCircle.haarAddCircle
Tactic: rwa [smul_smul, ENNReal.inv_mul_cancel (by positivity) (by finiteness), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
this :
  MemLp f p ((ENNReal.ofReal T)⁻¹ • HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)
rwa :
  ∀
    (this :
      MemLp f p
        (HSMul.hSMul (β := Measure (AddCircle T)) ((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) AddCircle.haarAddCircle)),
    MemLp f p AddCircle.haarAddCircle
rwa₁ :
  ∀ (this : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (AddCircle T)) 1 AddCircle.haarAddCircle)),
    MemLp f p AddCircle.haarAddCircle
⊢ MemLp f p AddCircle.haarAddCircle
have rwa₂ : ∀ (this : MemLp f p AddCircle.haarAddCircle), MemLp f p AddCircle.haarAddCircle
Tactic: rwa [smul_smul, ENNReal.inv_mul_cancel (by positivity) (by finiteness), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))
have rw : Complex.exp ((↑2 : ℂ) * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I) =
  Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))
Tactic: rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe,
    Circle.coe_exp, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
    Complex.ofReal_mul, Complex.ofReal_intCast]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (2 * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I) =
    Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))
have e_z : 2 * (↑π : ℂ) / (↑T : ℂ) * ((↑n : ℂ) * (↑x : ℂ)) * Complex.I = 2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw₂ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * 0 / (↑T : ℂ)) = 1
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
rw₂ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * 0 / (↑T : ℂ)) = 1
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw₃ : Complex.exp (0 / (↑T : ℂ)) = 1
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
rw₂ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * 0 / (↑T : ℂ)) = 1
rw₃ : Complex.exp (0 / (↑T : ℂ)) = 1
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw₄ : Complex.exp 0 = 1
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
rw : Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (1 : ℂ)
rw₁ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * (↑0 : ℂ) / (↑T : ℂ)) = 1
rw₂ : Complex.exp (2 * (↑π : ℂ) * Complex.I * (↑n : ℂ) * 0 / (↑T : ℂ)) = 1
rw₃ : Complex.exp (0 / (↑T : ℂ)) = 1
rw₄ : Complex.exp 0 = 1
⊢ Eq (α := ℂ) ((fourier n : (a : AddCircle T) → ℂ) 0 : ℂ) (1 : ℂ)
have rw₅ : Eq (α := ℂ) 1 1
Tactic: rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
x : AddCircle T
⊢ (fourier 1 : (a : AddCircle T) → ℂ) x = (↑x.toCircle : ℂ)
have rw : (↑(HSMul.hSMul (α := ℤ) 1 x).toCircle : ℂ) = (↑x.toCircle : ℂ)
Tactic: rw [fourier_apply, one_zsmul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
x : AddCircle T
rw : (↑(HSMul.hSMul (α := ℤ) 1 x).toCircle : ℂ) = (↑x.toCircle : ℂ)
⊢ (fourier 1 : (a : AddCircle T) → ℂ) x = (↑x.toCircle : ℂ)
have rw₁ : (↑x.toCircle : ℂ) = (↑x.toCircle : ℂ)
Tactic: rw [fourier_apply, one_zsmul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : AddCircle T
⊢ Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) x : ℂ) : ℂ)
have H : ∀ (z : ℝ),
  Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier n : (a : AddCircle T) → ℂ) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) : ℂ)
Tactic: induction x using QuotientAddGroup.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
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)) : ℂ) : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑((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)) : ℂ) : ℂ)
⊢ (↑(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]