awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
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
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

Tactic:
induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]

Premises used: Fin.succ, LineDeriv.iteratedLineDerivOp_succ_left, LineDerivAdd.lineDerivOp_add
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ ∂^{m} 0 = 0

Tactic:
map_zero (AddMonoidHom.mk' ∂^{m} (iteratedLineDerivOp_add m))

Premises used: map_zero, LineDeriv.iteratedLineDerivOp, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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 : E
⊢ ∂^{m} (-x) = -∂^{m} x

Tactic:
map_neg (AddMonoidHom.mk' ∂^{m} (iteratedLineDerivOp_add m)) x

Premises used: map_neg, LineDeriv.iteratedLineDerivOp, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
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
f : ι → E
s : Finset ι
⊢ ∂^{m} (∑ i ∈ s, f i) = ∑ i ∈ s, ∂^{m} (f i)

Tactic:
map_sum (AddMonoidHom.mk' ∂^{m} (iteratedLineDerivOp_add m)) f s

Premises used: map_sum, LineDeriv.iteratedLineDerivOp, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
m : Fin 0 → V
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
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)
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left, LineDerivSMul.lineDerivOp_smul
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
succ :
  ∀ (n : ℕ) (IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x) (m : Fin (n + 1) → V), ∂^{m} (r • x) = r • ∂^{m} x
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]

Premises used: Fin.succ, LineDeriv.iteratedLineDerivOp_succ_left, LineDerivSMul.lineDerivOp_smul
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : TopologicalSpace E
inst_2 : ContinuousLineDeriv V E E
m : Fin 0 → V
⊢ Continuous ∂^{m}

Tactic:
continuous_id

Premises used: LineDeriv.iteratedLineDerivOp, continuous_id
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : TopologicalSpace E
inst_2 : ContinuousLineDeriv V E E
m : Fin 0 → V
⊢ Continuous ∂^{m}

Tactic:
exact continuous_id

Premises used: continuous_id
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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 : ℕ
IH : ∀ (m : Fin n → V), Continuous ∂^{m}
m : Fin (n + 1) → V
⊢ Continuous ∂^{m}

Tactic:
(continuous_lineDerivOp _).comp (IH _)

Premises used: ContinuousLineDeriv.continuous_lineDerivOp, Continuous.comp, LineDeriv.iteratedLineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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 : ℕ
IH : ∀ (m : Fin n → V), Continuous ∂^{m}
m : Fin (n + 1) → V
⊢ Continuous ∂^{m}

Tactic:
exact (continuous_lineDerivOp _).comp (IH _)

Premises used: ContinuousLineDeriv.continuous_lineDerivOp, Continuous.comp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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}
succ : ∀ (n : ℕ) (IH : ∀ (m : Fin n → V), Continuous ∂^{m}) (m : Fin (n + 1) → V), Continuous ∂^{m}
⊢ Continuous ∂^{m}

Tactic:
induction n with
  | zero =>
    exact continuous_id
  | succ n IH =>
    exact (continuous_lineDerivOp _).comp (IH _)

Premises used: Fin.succ, continuous_id
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
inst : LineDeriv V E E
inst_1 : TopologicalSpace E
inst_2 : Ring R
inst_3 : AddCommGroup V
inst_4 : AddCommGroup E
inst_5 : Module R E
inst_6 : LineDerivAdd V E E
inst_7 : LineDerivSMul R V E E
inst_8 : ContinuousLineDeriv V E E
n : ℕ
m : Fin n → V
x : E
⊢ (iteratedLineDerivOpCLM R E m : (a : E) → E) x = ∂^{m} x

Tactic:
rfl

Premises used: LineDeriv.iteratedLineDerivOp, rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : CommRing R
inst_6 : AddCommGroup E
inst_7 : Module R E
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : LineDerivAdd E V₂ V₃
inst_11 : LineDerivAdd E V₁ V₂
inst_12 : LineDerivSMul R E V₂ V₃
inst_13 : LineDerivLeftSMul R E V₁ V₂
inst_14 : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (m₁ m₂ n : E),
    (fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) (m₁ + m₂) n =
      HAdd.hAdd (α := V₃) ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m₁ n) ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m₂ n)

Tactic:
simp [lineDerivOp_left_add]

Premises used: LineDerivAdd.lineDerivOp_left_add
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : CommRing R
inst_6 : AddCommGroup E
inst_7 : Module R E
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : LineDerivAdd E V₂ V₃
inst_11 : LineDerivAdd E V₁ V₂
inst_12 : LineDerivSMul R E V₂ V₃
inst_13 : LineDerivLeftSMul R E V₁ V₂
inst_14 : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E),
    (fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) (c • m) n =
      HSMul.hSMul (β := V₃) c ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m n)

Tactic:
simp [lineDerivOp_left_smul]

Premises used: LineDerivLeftSMul.lineDerivOp_left_smul
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : CommRing R
inst_6 : AddCommGroup E
inst_7 : Module R E
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : LineDerivAdd E V₂ V₃
inst_11 : LineDerivAdd E V₁ V₂
inst_12 : LineDerivSMul R E V₂ V₃
inst_13 : LineDerivLeftSMul R E V₁ V₂
inst_14 : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (m n₁ n₂ : E),
    (fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m (n₁ + n₂) =
      HAdd.hAdd (α := V₃) ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m n₁) ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m n₂)

Tactic:
simp [lineDerivOp_left_add, lineDerivOp_add]

Premises used: LineDerivAdd.lineDerivOp_add, LineDerivAdd.lineDerivOp_left_add
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : CommRing R
inst_6 : AddCommGroup E
inst_7 : Module R E
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : LineDerivAdd E V₂ V₃
inst_11 : LineDerivAdd E V₁ V₂
inst_12 : LineDerivSMul R E V₂ V₃
inst_13 : LineDerivLeftSMul R E V₁ V₂
inst_14 : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E),
    (fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m (c • n) =
      HSMul.hSMul (β := V₃) c ((fun (x1 x2 : E) ↦ ∂_{x1} (∂_{x2} f)) m n)

Tactic:
simp [lineDerivOp_left_smul, lineDerivOp_smul]

Premises used: LineDerivLeftSMul.lineDerivOp_left_smul, LineDerivSMul.lineDerivOp_smul
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
R : Type u_4
E : Type u_6
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : CommRing R
inst_6 : AddCommGroup E
inst_7 : Module R E
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : LineDerivAdd E V₂ V₃
inst_11 : LineDerivAdd E V₁ V₂
inst_12 : LineDerivSMul R E V₂ V₃
inst_13 : LineDerivLeftSMul R E V₁ V₂
inst_14 : LineDerivLeftSMul R E V₂ V₃
f : V₁
v w : E
⊢ (tensorLineDerivTwo R f : (a : E ⊗[R] E) → V₃) (v ⊗ₜ[R] w) = ∂_{v} (∂_{w} f)

Tactic:
lift.tmul _ _

Premises used: TensorProduct.lift.tmul
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
E : Type u_6
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : NormedAddCommGroup E
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
inst_8 : Module ℝ V₂
inst_9 : Module ℝ V₃
inst_10 : LineDerivAdd E V₁ V₂
inst_11 : LineDerivAdd E V₂ V₃
inst_12 : LineDerivSMul ℝ E V₂ V₃
inst_13 : LineDerivLeftSMul ℝ E V₁ V₂
inst_14 : LineDerivLeftSMul ℝ E V₂ V₃
inst_15 : Fintype ι
v : OrthonormalBasis ι ℝ E
f : V₁
⊢ Eq.{u_10 + 1} (α := V₃) ((tensorLineDerivTwo ℝ f : (a : E ⊗[ℝ] E) → V₃) (canonicalCovariantTensor E) : V₃)
    (∑ i : ι,
        lineDerivOp.{u_6, u_9, u_10} (V := E) ((v : (a : ι) → E) i : E)
          (lineDerivOp.{u_6, u_8, u_9} (V := E) ((v : (a : ι) → E) i : E) f) :
      V₃)

Tactic:
simp [InnerProductSpace.canonicalCovariantTensor_eq_sum E v,
    tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp]

Premises used: InnerProductSpace.canonicalCovariantTensor_eq_sum, LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
E : Type u_6
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst : LineDeriv E V₁ V₂
inst_1 : LineDeriv E V₂ V₃
inst_2 : AddCommGroup V₁
inst_3 : AddCommGroup V₂
inst_4 : AddCommGroup V₃
inst_5 : NormedAddCommGroup E
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
inst_8 : Module ℝ V₁
inst_9 : Module ℝ V₂
inst_10 : Module ℝ V₃
inst_11 : TopologicalSpace V₁
inst_12 : TopologicalSpace V₂
inst_13 : TopologicalSpace V₃
inst_14 : IsTopologicalAddGroup V₃
inst_15 : LineDerivAdd E V₁ V₂
inst_16 : LineDerivSMul ℝ E V₁ V₂
inst_17 : ContinuousLineDeriv E V₁ V₂
inst_18 : LineDerivAdd E V₂ V₃
inst_19 : LineDerivSMul ℝ E V₂ V₃
inst_20 : ContinuousLineDeriv E V₂ V₃
inst_21 : LineDerivLeftSMul ℝ E V₁ V₂
inst_22 : LineDerivLeftSMul ℝ E V₂ V₃
inst_23 : Fintype ι
v : OrthonormalBasis ι ℝ E
f : V₁
⊢ Eq.{u_10 + 1} (α := V₃) ((laplacianCLM ℝ E V₁ : (a : V₁) → V₃) f : V₃)
    (∑ i : ι,
        lineDerivOp.{u_6, u_9, u_10} (V := E) ((v : (a : ι) → E) i : E)
          (lineDerivOp.{u_6, u_8, u_9} (V := E) ((v : (a : ι) → E) i : E) f) :
      V₃)

Tactic:
simp [laplacianCLM, ← tensorLineDerivTwo_canonicalCovariantTensor_eq_sum]

Premises used: LineDeriv.laplacianCLM, LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum
-- Module: Mathlib.Analysis.Distribution.Distribution
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
F' : Type u_3
inst_5 : AddCommGroup F'
inst_6 : Module ℝ F'
inst_7 : TopologicalSpace F'
n : ℕ∞
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousSMul ℝ F
inst_10 : IsTopologicalAddGroup F'
inst_11 : ContinuousSMul ℝ F'
A : F →L[ℝ] F'
T : 𝓓'^{n}(Ω, F)
f : 𝓓^{n}(Ω, ℝ)
⊢ Eq.{u_3 + 1} (α := F')
    (((((mapCLM A : 𝓓'^{n}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F')) : (a : 𝓓'^{n}(Ω, F)) → 𝓓'^{n}(Ω, F')) T : 𝓓'^{n}(Ω, F')) :
          (a : 𝓓^{n}(Ω, ℝ)) → F')
        f :
      F')
    ((A : (a : F) → F') ((T : (a : 𝓓^{n}(Ω, ℝ)) → F) f : F) : F')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
f : 𝓓^{n}(Ω, ℝ)
⊢ (delta x : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f = (f : (a : E) → ℝ) x

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
h : ∀ (f : 𝓓^{n}(Ω, ℝ)), Eq (α := ℝ) ((delta x : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ) ((0 : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ)
⊢ Eq (α := 𝓓'^{n}(Ω, ℝ)) (delta x) 0

Tactic:
ext f
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
h : (f : (a : E) → ℝ) x = 0
⊢ Eq (α := ℝ) ((delta x : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ) ((0 : (a : 𝓓^{n}(Ω, ℝ)) → ℝ) f : ℝ)

Tactic:
change f x = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_mem : x ∈ tsupport (⇑f : (a : E) → ℝ)
⊢ False

Tactic:
hx (f.tsupport_subset hx_mem)

Premises used: TestFunction.tsupport_subset
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_mem : x ∈ tsupport (⇑f : (a : E) → ℝ)
⊢ False

Tactic:
exact hx (f.tsupport_subset hx_mem)

Premises used: TestFunction.tsupport_subset
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
⊢ x ∉ tsupport (⇑f : (a : E) → ℝ)

Tactic:
have hx_support : x ∉ tsupport f := by
    intro hx_mem
    exact hx (f.tsupport_subset hx_mem)
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_support : x ∉ tsupport (⇑f : (a : E) → ℝ)
⊢ (f : (a : E) → ℝ) x = 0

Tactic:
image_eq_zero_of_notMem_tsupport hx_support

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.Analysis.Distribution.Distribution
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_support : x ∉ tsupport (⇑f : (a : E) → ℝ)
⊢ (f : (a : E) → ℝ) x = 0

Tactic:
exact image_eq_zero_of_notMem_tsupport hx_support

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.Analysis.Distribution.Distribution
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 : E
T : 𝓓'^{k}(Ω, F)
f : 𝓓^{n}(Ω, ℝ)
⊢ Eq.{u_2 + 1} (α := F)
    (((((lineDerivCLM v : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) : (a : 𝓓'^{k}(Ω, F)) → 𝓓'^{n}(Ω, F)) T : 𝓓'^{n}(Ω, F)) :
          (a : 𝓓^{n}(Ω, ℝ)) → F)
        f :
      F)
    (-(T : (a : 𝓓^{k}(Ω, ℝ)) → F)
          (((TestFunction.lineDerivCLM ℝ v : 𝓓^{n}(Ω, ℝ) →L[ℝ] 𝓓^{k}(Ω, ℝ)) : (a : 𝓓^{n}(Ω, ℝ)) → 𝓓^{k}(Ω, ℝ)) f :
            𝓓^{k}(Ω, ℝ)) :
      F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.Distribution
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
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)
⊢ 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))

Tactic:
ext T f
-- Module: Mathlib.Analysis.Distribution.Distribution
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
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:
simp [lineDerivCLM_apply, TestFunction.lineDerivCLM_add, neg_add, -neg_add_rev]

Premises used: neg_add_rev, neg_add, TestFunction.lineDerivCLM_add, Distribution.lineDerivCLM_apply
-- Module: Mathlib.Analysis.Distribution.Distribution
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
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)
⊢ lineDerivCLM (c • v) =
    HSMul.hSMul (β := 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F)) c (lineDerivCLM v : 𝓓'^{k}(Ω, F) →L[ℝ] 𝓓'^{n}(Ω, F))

Tactic:
ext T f
-- Module: Mathlib.Analysis.Distribution.Distribution
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
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:
simp [lineDerivCLM_apply, TestFunction.lineDerivCLM_smul]

Premises used: Distribution.lineDerivCLM_apply, TestFunction.lineDerivCLM_smul
-- Module: Mathlib.Analysis.Distribution.Distribution
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
inst_5 : IsTopologicalAddGroup F
inst_6 : ContinuousSMul ℝ F
v : E
T : 𝓓'(Ω, F)
⊢ ∂_{v} T = ((lineDerivCLM v : 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, F)) : (a : 𝓓'(Ω, F)) → 𝓓'(Ω, F)) T

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.Distribution
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
inst_5 : IsTopologicalAddGroup F
inst_6 : ContinuousSMul ℝ F
v : E
⊢ Eq (α := 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, F)) (lineDerivOpCLM ℝ 𝓓'(Ω, F) v : 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, F))
    (lineDerivCLM v : 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, F))

Tactic:
rfl

Premises used: LineDeriv.lineDerivOpCLM, rfl, Distribution.lineDerivCLM
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
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 → 𝕜
f : 𝓢(E, F)
⊢ ((fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f =
    𝓕⁻ (E := 𝓢(E, F)) (((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
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)
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))
⊢ 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))

Tactic:
simp_rw [fourierMultiplierCLM_apply]

Premises used: SchwartzMap.fourierMultiplierCLM_apply