awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) ∂μ)
have h : Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
  (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) a))
  fun (a : E) ↦ HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) a : ℂ) ((f : (a : E) → F) a : F)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦ HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) a : ℂ) ((f : (a : E) → F) a : F)
have h : ∀ (x : E) (hf : (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x = (f : (a : E) → F) x),
  HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)
Tactic: filter_upwards [f.coeFn_toLp p μ] with x hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x = (f : (a : E) → F) x
⊢ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)
have h : HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) =
  HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ Continuous (X := ↥(Lp F p μ)) (Y := 𝓢'(E, F)) toTemperedDistribution
have h : ∀ (x : 𝓢(E, ℂ)), Continuous (Y := F) fun (x_1 : ↥(Lp F p μ)) ↦ (toTemperedDistribution x_1 : (a : 𝓢(E, ℂ)) → F) x
Tactic: apply PointwiseConvergenceCLM.continuous_of_continuous_eval
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
⊢ Continuous (Y := F) fun (x : ↥(Lp F p μ)) ↦ (toTemperedDistribution x : (a : 𝓢(E, ℂ)) → F) g
have this : Fact (1 ≤ (1 - p⁻¹)⁻¹)
Tactic: haveI : Fact (1 ≤ (1 - p⁻¹)⁻¹) := by simp [fact_iff]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
this : Fact (1 ≤ (1 - p⁻¹)⁻¹)
⊢ Continuous (Y := F) fun (x : ↥(Lp F p μ)) ↦ (toTemperedDistribution x : (a : 𝓢(E, ℂ)) → F) g
have hpq : p.HolderConjugate (1 - p⁻¹)⁻¹
Tactic: have hpq : ENNReal.HolderConjugate p (1 - p⁻¹)⁻¹ :=
      ENNReal.HolderConjugate.inv_one_sub_inv' hp.out
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ Eq (α := Submodule ℂ ↥(Lp F p μ))
    (LinearMap.ker (M₂ := 𝓢'(E, F)) (↑(toTemperedDistributionCLM F μ p) : ↥(Lp F p μ) →ₗ[ℂ] 𝓢'(E, F))) ⊥
have rw : ∀ (m : ↥(Lp F p μ)),
  Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) m : 𝓢'(E, F)) (0 : 𝓢'(E, F)) →
    m = 0
Tactic: rw [LinearMap.ker_eq_bot', ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
⊢ f = 0
have rw : (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] 0
Tactic: rw [eq_zero_iff_ae_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] 0
have hf₁ : LocallyIntegrable (↑(↑f : E →ₘ[μ] F) : E → F) μ
Tactic: apply ae_eq_zero_of_integral_contDiff_smul_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
hf₁ : LocallyIntegrable (↑(↑f : E →ₘ[μ] F) : E → F) μ
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] 0
have h : ∀ (g : E → ℝ),
  ContDiff ℝ ∞ g → HasCompactSupport g → Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
Tactic: apply ae_eq_zero_of_integral_contDiff_smul_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
have hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
Tactic: have hg₁ : HasCompactSupport (Complex.ofRealCLM ∘ g) := g_cpt.comp_left rfl
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
have hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
Tactic: have hg₂ : ContDiff ℝ ∞ (Complex.ofRealCLM ∘ g) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
have _ : Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ : F)
  ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
      (hg₁.toSchwartzMap hg₂) :
    F)
Tactic: calc
      _ = toTemperedDistributionCLM F μ p f (hg₁.toSchwartzMap hg₂) := by simp
      _ = _ := by simp [hf]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : FiniteDimensional ℝ E
inst_8 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : Eq (α := 𝓢'(E, F)) ((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) (0 : 𝓢'(E, F))
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
hg₂ : ContDiff ℝ (F := ℂ) ∞ ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ g)
_ :
  Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ : F)
    ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
        (hg₁.toSchwartzMap hg₂) :
      F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : E), g x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ) 0
have _₁ : Eq.{u_4 + 1} (α := F)
  ((((toTemperedDistributionCLM F μ p : (a : ↥(Lp F p μ)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F)
      (hg₁.toSchwartzMap hg₂) :
    F)
  (0 : F)
Tactic: calc
      _ = toTemperedDistributionCLM F μ p f (hg₁.toSchwartzMap hg₂) := by simp
      _ = _ := by simp [hf]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
c : ℂ
f : 𝓢'(E, F)
⊢ (smulLeftCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = c • f
have h : ∀ (x : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
    ((c • f : (a : 𝓢(E, ℂ)) → F) x : F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) ((smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) : 𝓢'(E, F))
    ((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
have h : ∀ (x : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) ((smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)
    ((((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁) (smulLeftCLM F (g₁ * g₂))
have h : ∀ (f : 𝓢'(E, F)),
  Eq (α := 𝓢'(E, F)) ((smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((smulLeftCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ + g₂) = HAdd.hAdd (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂)
have h : ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F (g₁ + g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((HAdd.hAdd (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext f u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ - g₂) = HSub.hSub (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂)
have h : ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F (g₁ - g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((HSub.hSub (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F g₁) (smulLeftCLM F g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext f u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F (-g)) (-smulLeftCLM F g)
have h : ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((((smulLeftCLM F (-g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((-smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
Tactic: ext f u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
g : ι → E → ℂ
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x) (∑ i ∈ s, smulLeftCLM F (g i))
have h : ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
      F)
    ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
Tactic: ext f u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
⊢ Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f))
    ((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f))
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
      F)
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((Lp.toTemperedDistribution (MemLp.toLp g hg₂ • f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (Lp.toTemperedDistribution f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u :
      F)
have h : Eq.{u_4 + 1} (α := F)
  (∫ (x : E), HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) ∂μ)
  (∫ (x : E),
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          x :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
Tactic: simp only [Lp.toTemperedDistribution_apply, smulLeftCLM_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E),
      HSMul.hSMul (α := ℂ)
        (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
            x :
          ℂ)
        ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
have h : Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
  (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) a : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) a))
  fun (a : E) ↦
  HSMul.hSMul (α := ℂ)
    (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ) a :
      ℂ)
    ((↑(↑f : E →ₘ[μ] F) : E → F) a)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) a : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          a :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) a)
have h : ∀ (x : E)
  (hg :
    (↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x =
      ((↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) • (↑(↑f : E →ₘ[μ] F) : E → F)) x)
  (hg' : (↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) x = g x),
  HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          x :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) x)
Tactic: filter_upwards [Lp.coeFn_lpSMul (r := r) (hg₂.toLp _) f, hg₂.coeFn_toLp] with x hg hg'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
𝕜 : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ Eq (α := 𝓢'(ℝ, F))
    ((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F)) ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F)) f) :
      𝓢'(ℝ, F))
    ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F))
        ((SchwartzMap.derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f) :
      𝓢'(ℝ, F))
have h : ∀ (g : 𝓢(ℝ, ℂ)),
  Eq (α := F)
    ((((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F)) ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F)) f) :
            𝓢'(ℝ, F)) :
          (a : 𝓢(ℝ, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F))
              ((SchwartzMap.derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f) :
            𝓢'(ℝ, F)) :
          (a : 𝓢(ℝ, ℂ)) → F)
        g :
      F)
Tactic: ext1 g
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
x y : E
f : 𝓢'(E, F)
⊢ ∂_{x + y} f = ∂_{x} f + ∂_{y} f
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((∂_{x + y} f : (a : 𝓢(E, ℂ)) → F) u : F) ((∂_{x} f + ∂_{y} f : (a : 𝓢(E, ℂ)) → F) u : F)
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
r : ℝ
x : E
f : 𝓢'(E, F)
⊢ ∂_{r • x} f = r • ∂_{x} f
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((∂_{r • x} f : (a : 𝓢(E, ℂ)) → F) u : F) ((r • ∂_{x} f : (a : 𝓢(E, ℂ)) → F) u : F)
Tactic: ext u