awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 (F := F →L[𝕜] E) 1 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun (y : E) ↦ (↑(M y).symm : F →L[𝕜] E)) s x : (a : E) → F →L[𝕜] E) v =
      -(↑(M x).symm : F →L[𝕜] E) ∘SL
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v) (↑(M x).symm : F →L[𝕜] E)
hMx : (↑(M x) : E →L[𝕜] F) = fderivWithin 𝕜 f s x
AV :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x)
AW :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x)
    (fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x)
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ W (f y)) s x

Tactic:
exact hW.comp x Af hst

Premises used: DifferentiableWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
simp :
  Eq.{u_2 + 1} (α := E)
    ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (lieBracketWithin 𝕜 V W t (f x)) : E)
    ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f u x) : (a : F) → E) (lieBracketWithin 𝕜 V W t (f x)) : E)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) u x

Tactic:
simp only [pullbackWithin]

Premises used: VectorField.pullbackWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
e_a : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f u x)
⊢ Eq.{u_2 + 1} (α := E)
    ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f s x) : (a : F) → E) (lieBracketWithin 𝕜 V W t (f x)) : E)
    ((ContinuousLinearMap.inverse (fderivWithin 𝕜 f u x) : (a : F) → E) (lieBracketWithin 𝕜 V W t (f x)) : E)

Tactic:
congr 2
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f u x)

Tactic:
fderivWithin_congr_set hus.symm

Premises used: fderivWithin_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f u x)

Tactic:
exact fderivWithin_congr_set hus.symm

Premises used: fderivWithin_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
apply : pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s
apply₁ : pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s
⊢ lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V u) (pullbackWithin 𝕜 f W u) u x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) u x

Tactic:
apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem _ _ hx

Premises used: Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
a : {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f V u x = pullbackWithin 𝕜 f V s x) x} ∈ 𝓝 x
⊢ pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
h :
  ∀ (y : E) (hy : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f u y) (fderivWithin 𝕜 f s y)),
    pullbackWithin 𝕜 f V u y = pullbackWithin 𝕜 f V s y
⊢ {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f V u x = pullbackWithin 𝕜 f V s x) x} ∈ 𝓝 x

Tactic:
filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy

Premises used: fderivWithin_eventually_congr_set
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
y : E
hy : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f u y) (fderivWithin 𝕜 f s y)
⊢ pullbackWithin 𝕜 f V u y = pullbackWithin 𝕜 f V s y

Tactic:
simp [pullbackWithin, hy]

Premises used: VectorField.pullbackWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
a : {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f W u x = pullbackWithin 𝕜 f W s x) x} ∈ 𝓝 x
⊢ pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
h :
  ∀ (y : E) (hy : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f u y) (fderivWithin 𝕜 f s y)),
    pullbackWithin 𝕜 f W u y = pullbackWithin 𝕜 f W s y
⊢ {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f W u x = pullbackWithin 𝕜 f W s x) x} ∈ 𝓝 x

Tactic:
filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy

Premises used: fderivWithin_eventually_congr_set
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
u : Set E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 u
hx : x ∈ u
hst : MapsTo f u t
hus : u =ᶠ[𝓝 x] s
y : E
hy : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f u y) (fderivWithin 𝕜 f s y)
⊢ pullbackWithin 𝕜 f W u y = pullbackWithin 𝕜 f W s y

Tactic:
simp [pullbackWithin, hy]

Premises used: VectorField.pullbackWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
hf : IsSymmSndFDerivAt 𝕜 f x
h'f : ContDiffAt 𝕜 2 f x
hV : DifferentiableAt 𝕜 V (f x)
hW : DifferentiableAt 𝕜 W (f x)
simp :
  ∀ (hf : IsSymmSndFDerivWithinAt 𝕜 f univ x) (hV : DifferentiableWithinAt 𝕜 V univ (f x))
    (hW : DifferentiableWithinAt 𝕜 W univ (f x)),
    pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W univ) univ x =
      lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V univ) (pullbackWithin 𝕜 f W univ) univ x
⊢ pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x

Tactic:
simp only [← lieBracketWithin_univ, ← pullbackWithin_univ, ← isSymmSndFDerivWithinAt_univ,
    ← differentiableWithinAt_univ] at hf h'f hV hW ⊢

Premises used: isSymmSndFDerivWithinAt_univ, VectorField.lieBracketWithin_univ, VectorField.pullbackWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
hV : DifferentiableWithinAt 𝕜 V univ (f x)
hW : DifferentiableWithinAt 𝕜 W univ (f x)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V univ) (pullbackWithin 𝕜 f W univ) univ x

Tactic:
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW uniqueDiffOn_univ
    (mem_univ _) (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
hV : DifferentiableWithinAt 𝕜 V univ (f x)
hW : DifferentiableWithinAt 𝕜 W univ (f x)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V univ) (pullbackWithin 𝕜 f W univ) univ x

Tactic:
exact pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW uniqueDiffOn_univ
    (mem_univ _) (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
inst_5 : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hn : minSmoothness 𝕜 2 ≤ n
h'f : ContDiffWithinAt 𝕜 n f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hst : MapsTo f s t
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt
  (h'f.isSymmSndFDerivWithinAt hn hu h'x hx) (h'f.of_le (le_minSmoothness.trans hn)) hV hW hu hx hst

Premises used: ContDiffWithinAt.of_le, VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, le_minSmoothness, ContDiffWithinAt.isSymmSndFDerivWithinAt, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
hn : minSmoothness 𝕜 2 ≤ n
f : E → F
V W : F → F
x : E
h'f : ContDiffAt 𝕜 n f x
hV : DifferentiableAt 𝕜 V (f x)
hW : DifferentiableAt 𝕜 W (f x)
⊢ pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x

Tactic:
pullback_lieBracket_of_isSymmSndFDerivAt (h'f.isSymmSndFDerivAt hn)
    (h'f.of_le (le_minSmoothness.trans hn)) hV hW

Premises used: ContDiffAt.isSymmSndFDerivAt, le_minSmoothness, VectorField.pullback_lieBracket_of_isSymmSndFDerivAt, ContDiffAt.of_le, LE.le.trans
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    u.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * C) t

Tactic:
le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t

Premises used: Set.le_indicator
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
refine_1 :
  ∀ t ∈ u,
    (fun (t : G) ↦
          norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F))
        t ≤
      ‖L‖ * ‖f t‖ * C
refine_2 :
  ∀ (t : G) (ht : t ∉ u),
    LE.le (α := ℝ)
      ((fun (t : G) ↦
          norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F))
        t)
      0
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    u.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * C) t

Tactic:
refine le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t

Premises used: Set.le_indicator
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
h : t ∈ u
⊢ (fun (t : G) ↦ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F))
      t ≤
    ‖L‖ * ‖f t‖ * C

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]

Premises used: le_rfl, ContinuousLinearMap.le_of_opNorm₂_le_of_le
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ x - t ∉ support g

Tactic:
mt (fun hxt => hu ?_) ht

Premises used: mt
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
refine : ∀ (hxt : x - t ∈ support g), t ∈ -tsupport g + s
⊢ x - t ∉ support g

Tactic:
refine mt (fun hxt => hu ?_) ht

Premises used: mt
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
hxt : x - t ∈ support g
⊢ t ∈ -tsupport g + s

Tactic:
⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩

Premises used: Iff.mpr, Set.Mem, subset_closure, setOf, Set.image2, And.intro, Exists.intro, Set.neg_mem_neg
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
hxt : x - t ∈ support g
refine : (fun (x1 x2 : G) ↦ x1 + x2) (-(x - t)) x = t
⊢ t ∈ -tsupport g + s

Tactic:
refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
hxt : x - t ∈ support g
⊢ (fun (x1 x2 : G) ↦ x1 + x2) (-(x - t)) x = t

Tactic:
simp only [neg_sub, sub_add_cancel]

Premises used: neg_sub, sub_add_cancel
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ x - t ∉ support g

Tactic:
have : x - t ∉ support g := by
      refine mt (fun hxt => hu ?_) ht
      refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
      simp only [neg_sub, sub_add_cancel]
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t_1 : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
this : x - t ∉ support g
⊢ LE.le (α := ℝ)
    ((fun (t : G) ↦
        norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F))
      t)
    0

Tactic:
simp only [notMem_support.mp this, (L _).map_zero, norm_zero, le_rfl]

Premises used: ContinuousLinearMap.map_zero, le_rfl, norm_zero, Function.notMem_support, Iff.mp, DFunLike.coe
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : AddGroup G
inst_8 : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    u.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖) t

Tactic:
convolution_integrand_bound_right_of_le_of_subset _ (fun i => ?_) hx hu

Premises used: MeasureTheory.convolution_integrand_bound_right_of_le_of_subset