awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 < ε
⊢ ∃ (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 ε
have 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 ε
Tactic: obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 ε
⊢ ∃ (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 ε
have 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 ε
Tactic: use (hg₁.toSchwartzMap hg₂).toLp p μ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
have 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
Tactic: filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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 ε
⊢ 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 ε
have this : (↑(↑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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ 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 ε
have h : (eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ).toReal ≤ ε
Tactic: simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and,
    Lp.dist_def, eLpNorm_congr_ae this]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ (eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ).toReal ≤ ε
have h₁ : ENNReal.ofReal ε ≠ ∞
Tactic: grw [hg₃, ENNReal.toReal_ofReal hε.le]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ 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) ∂μ
have 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)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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
⊢ (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)
have hf_ae : (↑(↑(f.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑f : (a : H) → V)
Tactic: have hf_ae := f.coeFn_toLp 2 μ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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)
⊢ (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)
have hg_ae : (↑(↑(g.toLp 2 μ) : H →ₘ[μ] V) : H → V) =ᶠ[ae μ] (⇑g : (a : H) → V)
Tactic: have hg_ae := g.coeFn_toLp 2 μ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
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)
⊢ ∂_{v + w} f = ∂_{v} f + ∂_{w} f
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
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
r : ℝ
y : E
f : 𝓢(E, F)
⊢ ∂_{r • y} f = r • ∂_{y} f
have h : ∀ (x : E), Eq.{u_8 + 1} (α := F) ((∂_{r • y} f : (a : E) → F) x : F) ((r • ∂_{y} f : (a : E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
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)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x : (a : (i : Fin (n + 1)) → E) → F) m : F)
have succ : Eq.{u_8 + 1} (α := F) ((∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f) : (a : E) → F) x : F)
  ((fderiv ℝ
          (fun (y : E) ↦
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) y : (a : (i : Fin n) → E) → F)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m))
          x :
        (a : E) → F)
      (m 0) :
    F)
Tactic: rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
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)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
succ :
  Eq.{u_8 + 1} (α := F) ((∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f) : (a : E) → F) x : F)
    ((fderiv ℝ
            (fun (y : E) ↦
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) y : (a : (i : Fin n) → E) → F)
                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m))
            x :
          (a : E) → F)
        (m 0) :
      F)
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x : (a : (i : Fin (n + 1)) → E) → F) m : F)
have succ₁ : DifferentiableAt ℝ (F := ContinuousMultilinearMap.{0, 0, u_5, u_8} ℝ (fun (i : Fin n) ↦ E) F)
  (iteratedFDeriv ℝ n (⇑f : (a : E) → F)) x
Tactic: rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
have zero : ∀ {m : Fin 0 → E} {x : E},
  Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x : (a : (i : Fin 0) → E) → F) m : F)
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ih =>
    rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
    · simp only [lineDerivOp_apply_eq_fderiv, ← ih]
    · exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x
Cleared hypotheses: n, m, x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
x : E
zero :
  ∀ {m : Fin 0 → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x : (a : (i : Fin 0) → E) → F) m : F)
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {m : Fin n → E} {x : E},
      Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
        ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F))
  {m : Fin (n + 1) → E} {x : E},
  Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x : (a : (i : Fin (n + 1)) → E) → F) m : F)
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ih =>
    rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
    · simp only [lineDerivOp_apply_eq_fderiv, ← ih]
    · exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x
Cleared hypotheses: n, m, x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
𝕜 : Type u_2
D : Type u_4
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 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
m : D
g : D ≃L[ℝ] E
f : 𝓢(E, F)
⊢ lineDerivOp (E := 𝓢(D, F)) m ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) =
    (compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) (lineDerivOp (V := E) ((g : (a : D) → E) m : E) f)
have h : ∀ (x : D),
  Eq.{u_8 + 1} (α := F)
    ((lineDerivOp (E := 𝓢(D, F)) m ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
    ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
              (lineDerivOp (V := E) ((g : (a : D) → E) m : E) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ Subset (α := Set ℝ) (tsupport (α := F) (⇑((derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f : 𝓢(ℝ, F)) : (a : ℝ) → F))
    (tsupport (α := F) (⇑f : (a : ℝ) → F))
have change : Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ deriv (⇑f : (a : ℝ) → F) x)
  (tsupport (α := F) (⇑f : (a : ℝ) → F))
Tactic: change tsupport (deriv f ·) ⊆ _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ deriv (⇑f : (a : ℝ) → F) x)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))
have simp_rw : Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ (fderiv ℝ (⇑f : (a : ℝ) → F) x : (a : ℝ) → F) 1)
  (tsupport (α := F) (⇑f : (a : ℝ) → F))
Tactic: simp_rw [← fderiv_apply_one_eq_deriv]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
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)
n : ℕ
IH :
  ∀ (m : Fin n → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
m : Fin (n + 1) → E
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
have succ : Subset.{u_5} (α := Set E)
  (tsupport.{u_5, u_8} (α := F) (⇑(∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f)) : (a : E) → F))
  (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
Tactic: rw [iteratedLineDerivOp_succ_left]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
have zero : ∀ (m : Fin 0 → E),
  Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left]
    exact (tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
zero :
  ∀ (m : Fin 0 → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (m : Fin n → E),
      Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
        (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F)))
  (m : Fin (n + 1) → E),
  Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left]
    exact (tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
⊢ (Δ f : (a : E) → F) x = Δ (E := (a : E) → F) (⇑f : (a : E) → F) x
have rw : (∑ i : Fin (Module.finrank ℝ E),
        lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
          (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
      (a : E) → F)
    x =
  Δ (E := (a : E) → F) (⇑f : (a : E) → F) x
Tactic: rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E)]