awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have _ : ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f) =
  ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
      (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f))
Tactic: calc
      _ = ∂_{m 0} (∂^{tail m} f) := iteratedLineDerivOp_succ_left _ _
      _ = ∂_{m 0} (∂^{init <| tail m} (∂_{tail m <| last n} f)) := by
        congr 1
        exact IH _
      _ = _ := by
        rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
_ :
  ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f) =
    ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f))
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have _₁ : ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
      (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)) =
  ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
Tactic: calc
      _ = ∂_{m 0} (∂^{tail m} f) := iteratedLineDerivOp_succ_left _ _
      _ = ∂_{m 0} (∂^{init <| tail m} (∂_{tail m <| last n} f)) := by
        congr 1
        exact IH _
      _ = _ := by
        rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
n : ℕ
m : Fin (n + 1) → V
f : E
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
have zero : ∀ (m : Fin (HAdd.hAdd (α := ℕ) 0 1) → V),
  ∂^{m} f = ∂^{init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V) m} (∂_{m (last 0)} f)
Tactic: induction n with
  | zero => rfl
  -- The proof is `∂^{n + 2} = ∂ ∂^{n + 1} = ∂ ∂^n ∂ = ∂^{n+1} ∂`
  | succ n IH =>
    have hmzero : init m 0 = m 0 := by simp only [init_def, castSucc_zero]
    have hmtail : tail m (last n) = m (last n.succ) := by
      simp only [tail_def, succ_last]
    calc
      _ = ∂_{m 0} (∂^{tail m} f) := iteratedLineDerivOp_succ_left _ _
      _ = ∂_{m 0} (∂^{init <| tail m} (∂_{tail m <| last n} f)) := by
        congr 1
        exact IH _
      _ = _ := by
        rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
n : ℕ
m : Fin (n + 1) → V
f : E
zero :
  ∀ (m : Fin (HAdd.hAdd (α := ℕ) 0 1) → V),
    ∂^{m} f = ∂^{init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V) m} (∂_{m (last 0)} f)
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
have succ : ∀ (n : ℕ) (IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f))
  (m : Fin (n + 1 + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
Tactic: induction n with
  | zero => rfl
  -- The proof is `∂^{n + 2} = ∂ ∂^{n + 1} = ∂ ∂^n ∂ = ∂^{n+1} ∂`
  | succ n IH =>
    have hmzero : init m 0 = m 0 := by simp only [init_def, castSucc_zero]
    have hmtail : tail m (last n) = m (last n.succ) := by
      simp only [tail_def, succ_last]
    calc
      _ = ∂_{m 0} (∂^{tail m} f) := iteratedLineDerivOp_succ_left _ _
      _ = ∂_{m 0} (∂^{init <| tail m} (∂_{tail m <| last n} f)) := by
        congr 1
        exact IH _
      _ = _ := by
        rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
y : V
f : E
n : ℕ
IH : iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n) (fun (x : Fin n) ↦ y) f = ∂_{y}^[n] f
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n + 1) (fun (x : Fin (n + 1)) ↦ y) f = ∂_{y}^[n + 1] f
have succ : ∂_{y}
    (iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n)
      (tail (α := fun (i : Fin (n + 1)) ↦ V) fun (x : Fin (n + 1)) ↦ y) f) =
  ∂_{y} (∂_{y}^[n] f)
Tactic: rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
n : ℕ
y : V
f : E
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n) (fun (x : Fin n) ↦ y) f = ∂_{y}^[n] f
have zero : iteratedLineDerivOp.{u_11, u_12} (V := V) (n := 0) (fun (x : Fin 0) ↦ y) f = ∂_{y}^[0] f
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']
    congr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
n : ℕ
y : V
f : E
zero : iteratedLineDerivOp.{u_11, u_12} (V := V) (n := 0) (fun (x : Fin 0) ↦ y) f = ∂_{y}^[0] f
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n) (fun (x : Fin n) ↦ y) f = ∂_{y}^[n] f
have succ : ∀ (n : ℕ) (IH : iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n) (fun (x : Fin n) ↦ y) f = ∂_{y}^[n] f),
  iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n + 1) (fun (x : Fin (n + 1)) ↦ y) f = ∂_{y}^[n + 1] f
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']
    congr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : AddCommGroup V
inst_2 : AddCommGroup E
inst_3 : LineDerivAdd V E E
x y : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
m : Fin (n + 1) → V
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
have succ : ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} (x + y)) =
  ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x) + ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} y)
Tactic: simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : AddCommGroup V
inst_2 : AddCommGroup E
inst_3 : LineDerivAdd V E E
x y : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
m : Fin (n + 1) → V
succ :
  ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} (x + y)) =
    ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x) + ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} y)
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
have succ₁ : ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x + ∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} y) =
  ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x) + ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} y)
Tactic: simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
n : ℕ
m : Fin n → V
inst_1 : AddCommGroup V
inst_2 : AddCommGroup E
inst_3 : LineDerivAdd V E E
x y : E
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
have zero : ∀ (m : Fin 0 → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
n : ℕ
m : Fin n → V
inst_1 : AddCommGroup V
inst_2 : AddCommGroup E
inst_3 : LineDerivAdd V E E
x y : E
zero : ∀ (m : Fin 0 → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
have succ : ∀ (n : ℕ) (IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y) (m : Fin (n + 1) → V),
  ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : SMul R E
inst_2 : LineDerivSMul R V E E
r : R
x : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x
m : Fin (n + 1) → V
⊢ ∂^{m} (r • x) = r • ∂^{m} x
have succ : ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} (r • x)) =
  r • ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x)
Tactic: simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : SMul R E
inst_2 : LineDerivSMul R V E E
r : R
x : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x
m : Fin (n + 1) → V
succ :
  ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} (r • x)) =
    r • ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x)
⊢ ∂^{m} (r • x) = r • ∂^{m} x
have succ₁ : ∂_{m 0} (r • ∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x) =
  r • ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} x)
Tactic: simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
n : ℕ
m : Fin n → V
inst_1 : SMul R E
inst_2 : LineDerivSMul R V E E
r : R
x : E
⊢ ∂^{m} (r • x) = r • ∂^{m} x
have zero : ∀ (m : Fin 0 → V), ∂^{m} (r • x) = r • ∂^{m} x
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
n : ℕ
m : Fin n → V
inst_1 : SMul R E
inst_2 : LineDerivSMul R V E E
r : R
x : E
zero : ∀ (m : Fin 0 → V), ∂^{m} (r • x) = r • ∂^{m} x
⊢ ∂^{m} (r • x) = r • ∂^{m} x
have succ : ∀ (n : ℕ) (IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x) (m : Fin (n + 1) → V), ∂^{m} (r • x) = r • ∂^{m} x
Tactic: induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : TopologicalSpace E
inst_2 : ContinuousLineDeriv V E E
n : ℕ
m : Fin n → V
⊢ Continuous ∂^{m}
have zero : ∀ (m : Fin 0 → V), Continuous ∂^{m}
Tactic: induction n with
  | zero =>
    exact continuous_id
  | succ n IH =>
    exact (continuous_lineDerivOp _).comp (IH _)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : TopologicalSpace E
inst_2 : ContinuousLineDeriv V E E
n : ℕ
m : Fin n → V
zero : ∀ (m : Fin 0 → V), Continuous ∂^{m}
⊢ Continuous ∂^{m}
have succ : ∀ (n : ℕ) (IH : ∀ (m : Fin n → V), Continuous ∂^{m}) (m : Fin (n + 1) → V), Continuous ∂^{m}
Tactic: induction n with
  | zero =>
    exact continuous_id
  | succ n IH =>
    exact (continuous_lineDerivOp _).comp (IH _)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Distribution (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
⊢ Eq (α := 𝓓'^{n}(Ω, ℝ)) (delta x) 0
have h : ∀ (f : 𝓓^{n}(Ω, ℝ)), Eq (α := ℝ) ((delta x : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ) ((0 : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Distribution (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
⊢ Eq (α := ℝ) ((delta x : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ) ((0 : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ)
have h : (f : (a : E) → ℝ) x = 0
Tactic: change f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Distribution (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
⊢ (f : (a : E) → ℝ) x = 0
have hx_support : x ∉ tsupport (⇑f : (a : E) → ℝ)
Tactic: have hx_support : x ∉ tsupport f := by
    intro hx_mem
    exact hx (f.tsupport_subset hx_mem)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Distribution (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_2
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
n k : ℕ∞
inst_5 : IsTopologicalAddGroup F
inst_6 : ContinuousSMul ℝ F
v₁ v₂ : E
⊢ lineDerivCLM (v₁ + v₂) =
    HAdd.hAdd (α := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) (β := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))
      (lineDerivCLM v₁ : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) (lineDerivCLM v₂ : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))
have h : ∀ (T : 𝓓'^{k}(Ω, F)) (f : 𝓓^{n}(Ω, ℝ)),
  Eq.{u_2 + 1} (α := F)
    (((((lineDerivCLM (v₁ + v₂) : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) : (a : 𝓓'^{k}(Ω, F)) → 𝓓'^{n}(Ω, F)) T :
            𝓓'^{n}(Ω, F)) :
          (a : 𝓓^{n}(Ω, ℝ)) → F)
        f :
      F)
    ((((HAdd.hAdd (α := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) (β := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))
                  (lineDerivCLM v₁ : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))
                  (lineDerivCLM v₂ : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) :
                (a : 𝓓'^{k}(Ω, F)) → 𝓓'^{n}(Ω, F))
              T :
            𝓓'^{n}(Ω, F)) :
          (a : 𝓓^{n}(Ω, ℝ)) → F)
        f :
      F)
Tactic: ext T f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Distribution (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_2
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
n k : ℕ∞
inst_5 : IsTopologicalAddGroup F
inst_6 : ContinuousSMul ℝ F
c : ℝ
v : E
⊢ lineDerivCLM (c • v) =
    HSMul.hSMul (β := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) c (lineDerivCLM v : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))
have h : ∀ (T : 𝓓'^{k}(Ω, F)) (f : 𝓓^{n}(Ω, ℝ)),
  Eq.{u_2 + 1} (α := F)
    (((((lineDerivCLM (c • v) : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) : (a : 𝓓'^{k}(Ω, F)) → 𝓓'^{n}(Ω, F)) T :
            𝓓'^{n}(Ω, F)) :
          (a : 𝓓^{n}(Ω, ℝ)) → F)
        f :
      F)
    ((((HSMul.hSMul (β := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) c (lineDerivCLM v : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) :
                (a : 𝓓'^{k}(Ω, F)) → 𝓓'^{n}(Ω, F))
              T :
            𝓓'^{n}(Ω, F)) :
          (a : 𝓓^{n}(Ω, ℝ)) → F)
        f :
      F)
Tactic: ext T f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((fourierMultiplierCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
      𝓢(E, F))
    (((fourierMultiplierCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
have simp_rw : 𝓕⁻ (E := 𝓢(E, F))
    (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)) =
  𝓕⁻ (E := 𝓢(E, F)) (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
Tactic: simp_rw [fourierMultiplierCLM_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ 𝓕⁻ (E := 𝓢(E, F))
      (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)) =
    𝓕⁻ (E := 𝓢(E, F)) (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
have e_a : Eq (α := 𝓢(E, F))
  (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
  (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ fourierMultiplierCLM F (c • g) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)),
  Eq (α := 𝓢(E, F)) (((fourierMultiplierCLM F (c • g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
    ((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (∑ i ∈ s, fourierMultiplierCLM F (g i) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)),
  Eq (α := 𝓢(E, F))
    (((fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
      𝓢(E, F))
    ((∑ i ∈ s, fourierMultiplierCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
c : 𝕜
⊢ (fourierMultiplierCLM F fun (x : E) ↦ c) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_4 + 1} (α := F)
    (((((fourierMultiplierCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    ((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
      𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)),
  Eq (α := 𝓢(E, F))
    ((((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (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
m : E
f : 𝓢(E, F)
⊢ ∂_{m} f =
    HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
      (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
        𝓢(E, F))
have rw : ∂_{m} f =
  (2 * (↑π : ℂ) * Complex.I) •
    𝓕⁻ (E := 𝓢(E, F))
      (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (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
m : E
f : 𝓢(E, F)
rw :
  ∂_{m} f =
    (2 * (↑π : ℂ) * Complex.I) •
      𝓕⁻ (E := 𝓢(E, F))
        (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
⊢ ∂_{m} f =
    HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
      (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
        𝓢(E, F))
have rw₁ : ∂_{m} f =
  𝓕⁻
    (HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
      (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (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
m : E
f : 𝓢(E, F)
rw :
  ∂_{m} f =
    (2 * (↑π : ℂ) * Complex.I) •
      𝓕⁻ (E := 𝓢(E, F))
        (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
rw₁ :
  ∂_{m} f =
    𝓕⁻
      (HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
        (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)))
⊢ ∂_{m} f =
    HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
      (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
        𝓢(E, F))
have rw₂ : ∂_{m} f = 𝓕⁻ (𝓕 (∂_{m} f))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]