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 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
f : 𝓢(E, F)
m : E
⊢ lineDerivOp (E := 𝓢'(E, F)) m ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) (∂_{m} f)
have h : ∀ (g : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((lineDerivOp (E := 𝓢'(E, F)) m ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) (∂_{m} f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
Tactic: ext1 g
-- 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 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢(E, F)
⊢ Δ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (Δ f)
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((Δ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
    ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (Δ f) : 𝓢'(E, 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
⊢ 𝓕⁻ (𝓕 f) = f
have h : ∀ (x : 𝓢(E, ℂ)), Eq.{u_4 + 1} (α := F) ((𝓕⁻ (𝓕 f) : (a : 𝓢(E, ℂ)) → F) x : F) ((f : (a : 𝓢(E, ℂ)) → F) x : F)
Tactic: ext
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
⊢ 𝓕 (𝓕⁻ f) = f
have h : ∀ (x : 𝓢(E, ℂ)), Eq.{u_4 + 1} (α := F) ((𝓕 (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) x : F) ((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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
⊢ 𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 f)
have h : ∀ (g : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F)
    ((𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
Tactic: ext g
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F))
have e_a : f = 𝓕 (𝓕⁻ f)
Tactic: congr
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F)) =
    𝓕⁻ (𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)))
have rw : 𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F)) =
  𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F))
Tactic: rw [fourier_toTemperedDistributionCLM_eq]
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
⊢ ∂_{m} (𝓕 f) =
    𝓕
      (HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
        ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)))
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕 f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕
            (HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext u
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕 f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕
            (HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
⊢ 𝓕 (∂_{m} f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F))
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((𝓕 (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext u
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕 (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
⊢ ∂_{m} (𝓕⁻ f) =
    𝓕⁻
      (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
        ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)))
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕⁻
            (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext u
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕⁻
            (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
⊢ 𝓕⁻ (∂_{m} f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
      ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F))
have h : ∀ (u : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((𝓕⁻ (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
Tactic: ext u
-- 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 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕⁻ (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ 𝓕 (E := 𝓢'(E, ℂ)) (delta 0) = toTemperedDistribution volume
have h : ∀ (f : 𝓢(E, ℂ)),
  Eq (α := ℂ) ((𝓕 (E := 𝓢'(E, ℂ)) (delta 0) : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)
    ((toTemperedDistribution volume : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E_1 : Type u_3
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
Ω_1 Ω₁ Ω₂ : Opens E_1
F_1 : Type u_4
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
B : Type u_6
E : Type u_7
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℝ E
Ω : Opens E
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace ℝ F
n : ℕ∞
inst_13 : TestFunctionClass B Ω F n
f : B
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
have obtain : ∀ (C : ℝ) (hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C),
  ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
Tactic: obtain ⟨C, hC⟩ := (map_continuous f).bounded_above_of_compact_support (map_hasCompactSupport f)
-- 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 : ℕ∞
f g : 𝓓^{n}(Ω, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) f) ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toFun : E → F) (contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun) (hasCompactSupport' : HasCompactSupport toFun)
  (tsupport_subset' : tsupport toFun ⊆ (↑Ω : Set E))
  (h :
    Eq (α := (a : E) → F)
      ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
        { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
          tsupport_subset' := tsupport_subset' })
      ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)),
  { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
    g
Tactic: cases f
Cleared hypotheses: f, 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 : ℕ∞
g : 𝓓^{n}(Ω, F)
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
hasCompactSupport' : HasCompactSupport toFun
tsupport_subset' : tsupport toFun ⊆ (↑Ω : Set E)
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
      { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' })
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)
⊢ { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
    g
have mk : ∀ (toFun_1 : E → F) (contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1) (hasCompactSupport'_1 : HasCompactSupport toFun_1)
  (tsupport_subset'_1 : tsupport toFun_1 ⊆ (↑Ω : Set E))
  (h :
    Eq (α := (a : E) → F)
      ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
        { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
          tsupport_subset' := tsupport_subset' })
      ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
        { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
          tsupport_subset' := tsupport_subset'_1 })),
  { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
    { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
      tsupport_subset' := tsupport_subset'_1 }
Tactic: cases g
Cleared hypotheses: g, 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 : ℕ∞
R : Type u_6
S : Type u_7
inst_9 : Semiring R
inst_10 : Semiring S
inst_11 : Module R F
inst_12 : Module S F
inst_13 : SMulCommClass ℝ R F
inst_14 : SMulCommClass ℝ S F
inst_15 : ContinuousConstSMul R F
inst_16 : ContinuousConstSMul S F
inst_17 : SMul R S
inst_18 : IsScalarTower R S F
x : R
x_1 : S
x_2 : 𝓓^{n}(Ω, F)
⊢ (x • x_1) • x_2 = x • x_1 • x_2
have h : ∀ (a : E), ((x • x_1) • x_2 : (a : E) → F) a = (x • x_1 • x_2 : (a : E) → F) a
Tactic: ext
-- 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 : ℕ∞
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (ofSupportedIn K_sub_Ω)
have rw : LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace)
  (topologicalSpace Ω F n)
Tactic: rw [continuous_iff_coinduced_le]
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
⊢ Continuous[_, t] (⇑f : (a : 𝓓^{n}(Ω, F)) → V) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t] ((⇑f : (a : 𝓓^{n}(Ω, F)) → V) ∘ ofSupportedIn K_sub_Ω)
have simp_rw : Continuous[_, t]
    (⇑((↑ℝ :
            {S : Type u_1} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type u_6} →
                  [inst : Semiring ℝ] →
                    [inst_15 : Semiring S] →
                      [inst_16 : AddCommMonoid M] →
                        [inst_17 : AddCommMonoid M₂] →
                          [inst_18 : Module ℝ M] →
                            [inst_19 : Module ℝ M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
          f) :
      (a : 𝓓^{n}(Ω, F)) → V) ↔
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
    Continuous[_, t]
      ((⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V) ∘
        ofSupportedIn K_sub_Ω)
Tactic: simp_rw [← f.coe_restrictScalars ℝ]
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (topologicalSpace Ω F n)
      (induced
        (⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V)
        t) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
have this : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
Tactic: have : @IsTopologicalAddGroup _ (induced (f.restrictScalars ℝ) t) _ :=
    topologicalAddGroup_induced _