awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
⊢ IntegrableOn φ (tsupport (⇑f : (a : E) → F₁)) μ

Tactic:
replace hφ := hφ.integrableOn_compact_subset f.tsupport_subset f.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}(Ω, F₁)
hφ : IntegrableOn φ (tsupport (⇑f : (a : E) → F₁)) μ
rw :
  ∀ (hφ : MemLp φ 1 (μ.restrict (tsupport (⇑f : (a : E) → F₁)))),
    MemLp.{u_3, u_8} (ε := F₃)
      (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
      (μ.restrict (tsupport (⇑f : (a : E) → F₁)))
⊢ IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable] at hφ ⊢

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}(Ω, F₁)
hφ : MemLp φ 1 (μ.restrict (tsupport (⇑f : (a : E) → F₁)))
⊢ MemLp.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
    (μ.restrict (tsupport (⇑f : (a : E) → F₁)))

Tactic:
B.memLp_of_bilin 1 f.memLp_top hφ

Premises used: TestFunction.memLp_top, ContinuousLinearMap.memLp_of_bilin, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}(Ω, F₁)
hφ : MemLp φ 1 (μ.restrict (tsupport (⇑f : (a : E) → F₁)))
⊢ MemLp.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
    (μ.restrict (tsupport (⇑f : (a : E) → F₁)))

Tactic:
exact B.memLp_of_bilin 1 f.memLp_top hφ

Premises used: TestFunction.memLp_top, ContinuousLinearMap.memLp_of_bilin, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
rw : IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
⊢ Integrable (⇑f : (a : E) → F) μ

Tactic:
rw [← integrableOn_iff_integrable_of_support_subset (subset_tsupport f)]

Premises used: subset_tsupport, MeasureTheory.integrableOn_iff_integrable_of_support_subset, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
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 (ε := ℝ) (fun (x : E) ↦ 1) (tsupport (⇑f : (a : E) → F)) μ

Tactic:
replace H := H.integrableOn_compact_subset f.tsupport_subset f.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) μ
this : IntegrableOn (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
⊢ IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ

Tactic:
simpa
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) μ
suffices : IntegrableOn (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ
⊢ IntegrableOn (⇑f : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ

Tactic:
suffices IntegrableOn ((1 : ℝ) • f) (tsupport f) μ by simpa
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) μ
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)))
⊢ IntegrableOn (⇑(HSMul.hSMul (α := ℝ) 1 f) : (a : E) → F) (tsupport (⇑f : (a : E) → F)) μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable] at H ⊢

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Analysis.Distribution.TestFunction
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 : 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:
f.memLp_top.smul H

Premises used: MeasureTheory.MemLp.smul, TestFunction.memLp_top
-- Module: Mathlib.Analysis.Distribution.TestFunction
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 : 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:
exact f.memLp_top.smul H

Premises used: MeasureTheory.MemLp.smul, TestFunction.memLp_top
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₃)
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₃)
⊢ 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₃)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁)
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:
simp [h.integrableOn_compact_subset K_sub_Ω K.2]

Premises used: TopologicalSpace.Compacts.isCompact', MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁)
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:
simp
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₂
f : 𝓓^{n}(Ω, F₁)
⊢ Eq.{u_8 + 1} (α := F₃) (((integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) : (a : 𝓓^{n}(Ω, F₁)) → F₃) f : 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₃)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Analysis.Distribution.TestFunction
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) μ
f : 𝓓^{n}(Ω, F₁)
⊢ Eq.{u_8 + 1} (α := F₃) (((integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) : (a : 𝓓^{n}(Ω, F₁)) → F₃) f : F₃)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ : F₃)

Tactic:
simp [hφ]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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) μ
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₃)
⊢ Eq (α := 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) (integralAgainstBilinCLM B μ φ : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃) (0 : 𝓓^{n}(Ω, F₁) →L[𝕜] F₃)

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
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) μ
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:
simp [hφ]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁)
⊢ IntegrableOn φ (↑K : Set E) μ

Tactic:
have hφ' := hφ.integrableOn_compact_subset K_sub_Ω K.isCompact
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁)
hφ' : IntegrableOn φ (↑K : Set E) μ
⊢ 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₃)

Tactic:
simp [hφ, hφ']
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ IsProbabilityMeasure (α := AddCircle T) haarAddCircle

Tactic:
IsProbabilityMeasure.mk addHaarMeasure_self

Premises used: MeasureTheory.Measure.addHaarMeasure_self, MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ volume = HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) haarAddCircle

Tactic:
rfl

Premises used: setOf, 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
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)
rw₃ rw₄ : Eq.{u_1 + 1} (α := E) (∫ (t : AddCircle T), f t ∂haarAddCircle) (∫ (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)

Tactic:
rw [volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    inv_smul_smul₀ hT.out.ne']

Premises used: AddCircle.volume_eq_smul_haarAddCircle, inv_smul_smul₀, LT.lt.le, LT.lt.ne', ENNReal.toReal_ofReal, MeasureTheory.integral_smul_measure, Fact.out
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
⊢ 0 < T

Tactic:
have hT' := hT.out
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p AddCircle.haarAddCircle
⊢ ENNReal.ofReal T ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
refine :
  ∀ (h : MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)),
    MemLp f p AddCircle.haarAddCircle
⊢ MemLp f p AddCircle.haarAddCircle ↔
    MemLp f p (HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)

Tactic:
refine ⟨fun h ↦ h.smul_measure (by finiteness), fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ (ENNReal.ofReal T)⁻¹ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 ((ENNReal.ofReal T)⁻¹ • HSMul.hSMul (β := Measure (AddCircle T)) (ENNReal.ofReal T) AddCircle.haarAddCircle)

Tactic:
have := h.smul_measure (c := (ENNReal.ofReal T)⁻¹) (by finiteness)
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (HSMul.hSMul (β := Measure (AddCircle T)) ((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) AddCircle.haarAddCircle)
⊢ ENNReal.ofReal T ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (HSMul.hSMul (β := Measure (AddCircle T)) ((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) AddCircle.haarAddCircle)
⊢ ENNReal.ofReal T ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : MemLp f p AddCircle.haarAddCircle), 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

Premises used: smul_smul, one_smul, ENNReal.inv_mul_cancel