awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : MeasurableSpace D
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
inst_8 : NormedField 𝕜
inst_9 : NormedSpace 𝕜 F
inst_10 : SMulCommClass ℝ 𝕜 F
inst_11 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_12 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
rcases :
  ∀ (k : ℕ) (C : ℝ) (hC_pos : 0 ≤ C)
    (hC :
      ∀ (f : 𝓢(E, F)),
        ‖f.toLp p μ‖ ≤
          HMul.hMul (β := ℝ) C
            ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)),
          norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
            HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rcases norm_toLp_le_seminorm 𝕜 F p μ with ⟨k, C, hC_pos, hC⟩

Premises used: SchwartzMap.norm_toLp_le_seminorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : MeasurableSpace D
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
inst_8 : NormedField 𝕜
inst_9 : NormedSpace 𝕜 F
inst_10 : SMulCommClass ℝ 𝕜 F
inst_11 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_12 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ
hC_pos : 0 ≤ C
hC :
  ∀ (f : 𝓢(E, F)),
    ‖f.toLp p μ‖ ≤
      HMul.hMul (β := ℝ) C ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
⟨Finset.Iic (k, 0), C, hC_pos, hC⟩

Premises used: Prod.mk, And.intro, Exists.intro, Finset.Iic, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : MeasurableSpace D
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
inst_8 : NormedField 𝕜
inst_9 : NormedSpace 𝕜 F
inst_10 : SMulCommClass ℝ 𝕜 F
inst_11 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_12 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ
hC_pos : 0 ≤ C
hC :
  ∀ (f : 𝓢(E, F)),
    ‖f.toLp p μ‖ ≤
      HMul.hMul (β := ℝ) C ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
exact ⟨Finset.Iic (k, 0), C, hC_pos, hC⟩
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_10 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
f : 𝓢(E, F)
⊢ (toLpCLM 𝕜 F p μ : (a : 𝓢(E, F)) → ↥(Lp F p μ)) f = f.toLp p μ

Tactic:
rfl

Premises used: SchwartzMap.toLp, MeasureTheory.MemLp.toLp, rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_7 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ Continuous (Y := ↥(Lp F p μ)) fun (f : 𝓢(E, F)) ↦ f.toLp p μ

Tactic:
(toLpCLM ℝ F p μ).continuous

Premises used: Real, SchwartzMap.toLpCLM, ContinuousLinearMap.continuous, SchwartzMap.toLp, MeasureTheory.MemLp.toLp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))) f

Tactic:
(mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (y : ↥(Lp F p μ)),
      Membership.mem (γ := Set ↥(Lp F p μ))
          (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ))) y ∧
        y ∈ Metric.closedBall f ε
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))) f

Tactic:
refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (g : E → F) (hg₁ : HasCompactSupport g) (hg₂ : ContDiff ℝ ∞ g)
    (hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε),
    ∃ (y : ↥(Lp F p μ)),
      Membership.mem (γ := Set ↥(Lp F p μ))
          (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ))) y ∧
        y ∈ Metric.closedBall f ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ)) (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))
        y ∧
      y ∈ Metric.closedBall f ε

Tactic:
obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.exist_eLpNorm_sub_le, Fact.out
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
h :
  Membership.mem (γ := Set ↥(Lp F p μ)) (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))
      ((hg₁.toSchwartzMap hg₂).toLp p μ) ∧
    (hg₁.toSchwartzMap hg₂).toLp p μ ∈ Metric.closedBall f ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ)) (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))
        y ∧
      y ∈ Metric.closedBall f ε

Tactic:
use (hg₁.toSchwartzMap hg₂).toLp p μ

Premises used: SchwartzMap.toLp, HasCompactSupport.toSchwartzMap
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
h :
  ∀ (a : E),
    (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) a = (hg₁.toSchwartzMap hg₂ : (a : E) → F) a →
      ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F)) a =
        ((↑(↑f : E →ₘ[μ] F) : E → F) - g) a
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ]
    (↑(↑f : E →ₘ[μ] F) : E → F) - g

Tactic:
filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]

Premises used: SchwartzMap.coeFn_toLp, HasCompactSupport.toSchwartzMap
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (a : E),
    (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) a = (hg₁.toSchwartzMap hg₂ : (a : E) → F) a →
      ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F)) a =
        ((↑(↑f : E →ₘ[μ] F) : E → F) - g) a

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ]
    (↑(↑f : E →ₘ[μ] F) : E → F) - g

Tactic:
have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᶠ[ae μ] (f : E → F) - g := by
    filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]
    simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
this :
  (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ]
    (↑(↑f : E →ₘ[μ] F) : E → F) - g
h : (eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ).toReal ≤ ε
⊢ Membership.mem (γ := Set ↥(Lp F p μ)) (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))
      ((hg₁.toSchwartzMap hg₂).toLp p μ) ∧
    (hg₁.toSchwartzMap hg₂).toLp p μ ∈ Metric.closedBall f ε

Tactic:
simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and,
    Lp.dist_def, eLpNorm_congr_ae this]

Premises used: Set.mem_range, MeasureTheory.Lp.dist_def, SchwartzMap.toLpCLM_apply, Metric.mem_closedBall', MeasureTheory.eLpNorm_congr_ae, true_and, exists_apply_eq_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
this :
  (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ]
    (↑(↑f : E →ₘ[μ] F) : E → F) - g
h₁ : ENNReal.ofReal ε ≠ ∞
⊢ (eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ).toReal ≤ ε

Tactic:
grw [hg₃, ENNReal.toReal_ofReal hε.le]

Premises used: LT.lt.le, ENNReal.toReal_ofReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
this :
  (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑((hg₁.toSchwartzMap hg₂).toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ]
    (↑(↑f : E →ₘ[μ] F) : E → F) - g
⊢ ENNReal.ofReal ε ≠ ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup H
inst_1 : NormedSpace ℝ H
inst_2 : FiniteDimensional ℝ H
inst_3 : MeasurableSpace H
inst_4 : BorelSpace H
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst_7 : μ.HasTemperateGrowth
h :
  (ae μ).EventuallyEq (β := ℂ)
    (fun (a : H) ↦ inner ℂ ((↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) ((↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a))
    fun (a : H) ↦ inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)
⊢ inner ℂ (E := ↥(Lp V 2 μ)) (f.toLp 2 μ) (g.toLp 2 μ) =
    ∫ (x : H), inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) x : V) ((g : (a : H) → V) x : V) ∂μ

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup H
inst_1 : NormedSpace ℝ H
inst_2 : FiniteDimensional ℝ H
inst_3 : MeasurableSpace H
inst_4 : BorelSpace H
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst_7 : μ.HasTemperateGrowth
⊢ (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑f : (a : H) → V)

Tactic:
have hf_ae := f.coeFn_toLp 2 μ
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup H
inst_1 : NormedSpace ℝ H
inst_2 : FiniteDimensional ℝ H
inst_3 : MeasurableSpace H
inst_4 : BorelSpace H
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst_7 : μ.HasTemperateGrowth
hf_ae : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑f : (a : H) → V)
⊢ (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑g : (a : H) → V)

Tactic:
have hg_ae := g.coeFn_toLp 2 μ
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup H
inst_1 : NormedSpace ℝ H
inst_2 : FiniteDimensional ℝ H
inst_3 : MeasurableSpace H
inst_4 : BorelSpace H
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst_7 : μ.HasTemperateGrowth
hf_ae : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑f : (a : H) → V)
hg_ae : (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑g : (a : H) → V)
h :
  ∀ (a : H) (hf : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a = (f : (a : H) → V) a)
    (hg : (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a = (g : (a : H) → V) a),
    inner ℂ ((↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) ((↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) =
      inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)
⊢ (ae μ).EventuallyEq (β := ℂ)
    (fun (a : H) ↦ inner ℂ ((↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) ((↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a))
    fun (a : H) ↦ inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)

Tactic:
filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup H
inst_1 : NormedSpace ℝ H
inst_2 : FiniteDimensional ℝ H
inst_3 : MeasurableSpace H
inst_4 : BorelSpace H
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst_7 : μ.HasTemperateGrowth
hf_ae : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑f : (a : H) → V)
hg_ae : (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑g : (a : H) → V)
a : H
hf : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a = (f : (a : H) → V) a
hg : (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a = (g : (a : H) → V) a
h :
  inner ℂ ((f : (a : H) → V) a) ((↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) =
    inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)
h₁ h₂ :
  inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V) =
    inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)
⊢ inner ℂ ((↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) ((↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) a) =
    inner.{0, u_9} ℂ (E := V) ((f : (a : H) → V) a : V) ((g : (a : H) → V) a : V)

Tactic:
rw [hf, hg]
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
x_1 : ℕ × ℕ
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ ‖x‖ ^ (k, n).1 *
      norm.{u_8} (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ ℝ) F)
        (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(ℝ, F)) ↦ (deriv (⇑x : (a : ℝ) → F) : (x : ℝ) → F)) f) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ)
      ((Finset.sup {(k, n + 1)} (schwartzSeminormFamily 𝕜 ℝ F) : (a : 𝓢(ℝ, F)) → ℝ) f : ℝ)

Tactic:
simpa only [Real.norm_eq_abs, Finset.sup_singleton, schwartzSeminormFamily_apply, one_mul,
        norm_iteratedFDeriv_eq_norm_iteratedDeriv, ← iteratedDeriv_succ'] using
        f.le_seminorm' 𝕜 k (n + 1) x

Premises used: Finset.sup_singleton, iteratedDeriv_succ', HAdd.hAdd, SchwartzMap.le_seminorm', SchwartzMap.schwartzSeminormFamily_apply, OfNat.ofNat, norm_iteratedFDeriv_eq_norm_iteratedDeriv, one_mul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
x : ℝ
⊢ Eq (α := F) ((((derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f : 𝓢(ℝ, F)) : (a : ℝ) → F) x : F)
    (deriv (⇑f : (a : ℝ) → F) x : F)

Tactic:
rfl

Premises used: deriv, rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : 𝓢(ℝ, F)
x : ℝ
⊢ HasDerivAt (F := F) (⇑f : (a : ℝ) → F) (deriv (⇑f : (a : ℝ) → F) x) x

Tactic:
f.differentiableAt.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, SchwartzMap.differentiableAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
x_1 : ℕ × ℕ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (E →L[ℝ] F))
        (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(E, F)) ↦ (fderiv ℝ (⇑x : (a : E) → F) : (x : E) → E →L[ℝ] F)) f) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ)
      ((Finset.sup {(k, n + 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simpa only [schwartzSeminormFamily_apply, Seminorm.comp_apply, Finset.sup_singleton,
        one_smul, norm_iteratedFDeriv_fderiv, one_mul] using f.le_seminorm 𝕜 k (n + 1) x

Premises used: Finset.sup_singleton, one_smul, Seminorm.comp_apply, SchwartzMap.le_seminorm, HAdd.hAdd, SchwartzMap.schwartzSeminormFamily_apply, OfNat.ofNat, one_mul, norm_iteratedFDeriv_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x : E
⊢ Eq (α := E →L[ℝ] F)
    ((((fderivCLM 𝕜 E F : (a : 𝓢(E, F)) → 𝓢(E, E →L[ℝ] F)) f : 𝓢(E, E →L[ℝ] F)) : (a : E) → E →L[ℝ] F) x : E →L[ℝ] F)
    (fderiv ℝ (⇑f : (a : E) → F) x : E →L[ℝ] F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
x : E
⊢ HasFDerivAt.{0, u_5, u_8} (F := F) (⇑f : (a : E) → F) (fderiv ℝ (⇑f : (a : E) → F) x) x

Tactic:
f.differentiableAt.hasFDerivAt

Premises used: DifferentiableAt.hasFDerivAt, SchwartzMap.differentiableAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
m : E
f : 𝓢(E, F)
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂_{m} f : (a : E) → F) x : F) ((fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) m : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
h : ∀ (x : E), Eq.{u_8 + 1} (α := F) ((∂_{v + w} f : (a : E) → F) x : F) ((∂_{v} f + ∂_{w} f : (a : E) → F) x : F)
⊢ ∂_{v + w} f = ∂_{v} f + ∂_{w} f

Tactic:
ext x