awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(integralAgainstBilinLM B μ φ) : (a : 𝓓^{n}_{K}(E, F₁)) → F₃)

Tactic:
continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _
      (.of_real fun _ ↦ ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, fun f ↦ ?_⟩)

Premises used: Norm.norm, HMul.hMul, Seminorm.IsBounded.of_real, MeasureTheory.Measure.restrict, SetLike.coe, MeasureTheory.integral, Exists.intro, norm_withSeminorms, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
refine :
  ∀ (x : Fin 1) (f : 𝓓^{n}_{K}(E, F₁)),
    (normSeminorm 𝕜 F₃ : (a : F₃) → ℝ) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
      HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
        ((Finset.sup {0} (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K) : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(integralAgainstBilinLM B μ φ) : (a : 𝓓^{n}_{K}(E, F₁)) → F₃)

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _
      (.of_real fun _ ↦ ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, fun f ↦ ?_⟩)

Premises used: Norm.norm, HMul.hMul, Seminorm.IsBounded.of_real, MeasureTheory.Measure.restrict, SetLike.coe, MeasureTheory.integral, Exists.intro, norm_withSeminorms, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
x : Fin 1
f : 𝓓^{n}_{K}(E, F₁)
⊢ (normSeminorm 𝕜 F₃ : (a : F₃) → ℝ) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((Finset.sup {0} (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K) : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
simpa using norm_integralAgainstBilinLM_le

Premises used: ContDiffMapSupportedIn.norm_integralAgainstBilinLM_le
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinCLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (if IntegrableOn φ (↑K : Set E) μ then
        ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
      else 0 :
      F₃)

Tactic:
integralAgainstBilinLM_apply

Premises used: ContDiffMapSupportedIn.integralAgainstBilinLM_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinCLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ : F₃)

Tactic:
integralAgainstBilinLM_eq_integral hφ

Premises used: ContDiffMapSupportedIn.integralAgainstBilinLM_eq_integral
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinCLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (∫ (x : E) in (↑K : Set E),
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ :
      F₃)

Tactic:
integralAgainstBilinLM_eq_setIntegral hφ

Premises used: ContDiffMapSupportedIn.integralAgainstBilinLM_eq_setIntegral
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
m : Fin 0 → V
f : E
⊢ ∂^{m} f = f

Tactic:
rfl

Premises used: LineDeriv.iteratedLineDerivOp, rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
m : Fin 1 → V
f : E
⊢ ∂^{m} f = ∂_{m 0} f

Tactic:
rfl

Premises used: LineDeriv.iteratedLineDerivOp, rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
n : ℕ
m : Fin (n + 1) → V
f : E
⊢ ∂^{m} f = ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) m} f)

Tactic:
rfl

Premises used: LineDeriv.iteratedLineDerivOp, rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
m : Fin (HAdd.hAdd (α := ℕ) 0 1) → V
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V) m} (∂_{m (last 0)} f)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0

Tactic:
simp only [init_def, castSucc_zero]

Premises used: Fin.init_def, Fin.castSucc_zero
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0

Tactic:
have hmzero : init m 0 = m 0 := by simp only [init_def, castSucc_zero]
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)

Tactic:
simp only [tail_def, succ_last]

Premises used: Fin.tail_def, Fin.succ_last
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)

Tactic:
have hmtail : tail m (last n) = m (last n.succ) := by
      simp only [tail_def, succ_last]
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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 = ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f)

Tactic:
iteratedLineDerivOp_succ_left _ _

Premises used: LineDeriv.iteratedLineDerivOp_succ_left
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
e_a :
  ∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f =
    ∂^{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 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:
congr 1
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
⊢ ∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f =
    ∂^{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:
IH _
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
⊢ ∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f =
    ∂^{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:
exact IH _
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
rw :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
rw₁ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0}
      (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
rw₂ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{m 0}
      (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
rw₃ rw₄ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} 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)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)

Tactic:
rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left, Fin.tail_init_eq_init_tail
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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 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)
⊢ ∂^{m} 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]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left, Fin.init, LineDeriv.iteratedLineDerivOp, Fin.last, LineDeriv.lineDerivOp, OfNat.ofNat, Fin.tail
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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)
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)
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} 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]

Premises used: Fin.succ, LineDeriv.iteratedLineDerivOp_succ_left, LineDeriv.iteratedLineDerivOp, LineDeriv.lineDerivOp, OfNat.ofNat, Fin.tail
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
y : V
f : E
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := 0) (fun (x : Fin 0) ↦ y) f = ∂_{y}^[0] f

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
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)
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n + 1) (fun (x : Fin (n + 1)) ↦ y) f = ∂_{y}^[n + 1] f

Tactic:
rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply', LineDeriv.iteratedLineDerivOp_succ_left
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
⊢ ∂_{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:
congr
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
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
⊢ iteratedLineDerivOp.{u_11, u_12} (V := V) (n := n) (fun (x : Fin n) ↦ y) f = ∂_{y}^[n] f

Tactic:
induction n with
  | zero => rfl
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left, Function.iterate_succ_apply']
    congr

Premises used: Function.iterate_succ_apply', Fin.succ, LineDeriv.iteratedLineDerivOp_succ_left
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
v : V
⊢ lineDerivOp.{u_5, u_6, u_7} (E := E) v 0 = 0

Tactic:
map_zero (AddMonoidHom.mk' ∂_{v} (lineDerivOp_add v))

Premises used: map_zero, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
v : V
x : E
⊢ ∂_{v} (-x) = -∂_{v} x

Tactic:
map_neg (AddMonoidHom.mk' ∂_{v} (lineDerivOp_add v)) x

Premises used: map_neg, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
v : V
f : ι → E
s : Finset ι
⊢ lineDerivOp.{u_5, u_6, u_7} (E := E) v (∑ i ∈ s, f i) = ∑ i ∈ s, ∂_{v} (f i)

Tactic:
map_sum (AddMonoidHom.mk' ∂_{v} (lineDerivOp_add v)) f s

Premises used: map_sum, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
x : E
⊢ lineDerivOp.{u_5, u_6, u_7} (V := V) 0 x = 0

Tactic:
map_zero (AddMonoidHom.mk' (∂_{·} x) (lineDerivOp_left_add · · x))

Premises used: map_zero, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
v : V
x : E
⊢ ∂_{-v} x = -∂_{v} x

Tactic:
map_neg (AddMonoidHom.mk' (∂_{·} x) (lineDerivOp_left_add · · x)) v

Premises used: map_neg, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
ι : Type u_1
V : Type u_5
E : Type u_6
F : Type u_7
inst : AddCommGroup V
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : LineDeriv V E F
inst_4 : LineDerivAdd V E F
f : ι → V
x : E
s : Finset ι
⊢ lineDerivOp.{u_5, u_6, u_7} (V := V) (∑ i ∈ s, f i) x = ∑ i ∈ s, ∂_{f i} x

Tactic:
map_sum (AddMonoidHom.mk' (∂_{·} x) (lineDerivOp_left_add · · x)) f s

Premises used: map_sum, AddMonoidHom.mk', LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.DerivNotation
Goal:
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : AddCommGroup F
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup V
inst_8 : LineDeriv V E F
inst_9 : LineDerivAdd V E F
inst_10 : LineDerivSMul R V E F
inst_11 : ContinuousLineDeriv V E F
m : V
x : E
⊢ (lineDerivOpCLM R E m : (a : E) → F) x = ∂_{m} x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.DerivNotation
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
m : Fin 0 → V
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

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

Tactic:
simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left, LineDerivAdd.lineDerivOp_add