awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
⊢ 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)
have apply : pullbackWithin 𝕜 f W s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))
Tactic: apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
⊢ pullbackWithin 𝕜 f W s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))
have h₁ : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E |
      Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) x} x →
        Membership.mem (γ := Set E)
          {x : E |
            (fun (x : E) ↦
                pullbackWithin 𝕜 f W s x = (fun (y : E) ↦ (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y)) : E)) x)
              x}
          x}
    a
Tactic: filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ (↑(M y) : E →L[𝕜] F) = fderivWithin 𝕜 f s y) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              (fun (x : E) ↦
                  pullbackWithin 𝕜 f W s x =
                    (fun (y : E) ↦ (((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y)) : E)) x)
                x}
            x}
      a
⊢ pullbackWithin 𝕜 f W s =ᶠ[𝓝[s] x] fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))
have h₂ : ∀ (a : E),
  (↑(M a) : E →L[𝕜] F) = fderivWithin 𝕜 f s a →
    pullbackWithin 𝕜 f W s a = ((↑(M a).symm : F →L[𝕜] E) : (a : F) → E) (W (f a))
Tactic: filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have Af : DifferentiableWithinAt 𝕜 f s x
Tactic: have Af : DifferentiableWithinAt 𝕜 f s x := h'f.differentiableWithinAt two_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
have pos : HSub.hSub (α := E) (β := E) (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 W t (f x) : (a : F) → F) (V (f x)) : F) : E)
    (((M x).symm : (a : F) → E) ((fderivWithin 𝕜 V t (f x) : (a : F) → F) (W (f x)) : F) : E) =
  HSub.hSub (α := E) (β := E)
    ((fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (W (f y))) s x : (a : E) → E)
        (((M x).symm : (a : F) → E) (V (f x)) : E) :
      E)
    ((fderivWithin 𝕜 (fun (y : E) ↦ ((↑(M y).symm : F →L[𝕜] E) : (a : F) → E) (V (f y))) s x : (a : E) → E)
        (((M x).symm : (a : F) → E) (W (f x)) : E) :
      E)
Tactic: simp only [lieBracketWithin_eq, pullbackWithin_eq_of_fderivWithin_eq hMx, map_sub, AV, AW]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) u x
have 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)
Tactic: simp only [pullbackWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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.{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)
have e_a : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f u x)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V u) (pullbackWithin 𝕜 f W u) u x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) u x
have apply : pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem _ _ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V u) (pullbackWithin 𝕜 f W u) u x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) u x
have apply₁ : pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem _ _ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f V u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f V s
have a : {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f V u x = pullbackWithin 𝕜 f V s x) x} ∈ 𝓝 x
Tactic: apply nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f V u x = pullbackWithin 𝕜 f V s x) x} ∈ 𝓝 x
have 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
Tactic: filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ pullbackWithin 𝕜 f W u =ᶠ[𝓝[u] x] pullbackWithin 𝕜 f W s
have a : {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f W u x = pullbackWithin 𝕜 f W s x) x} ∈ 𝓝 x
Tactic: apply nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ {x : E | (fun (x : E) ↦ pullbackWithin 𝕜 f W u x = pullbackWithin 𝕜 f W s x) x} ∈ 𝓝 x
have 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
Tactic: filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
⊢ pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x
have 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
Tactic: simp only [← lieBracketWithin_univ, ← pullbackWithin_univ, ← isSymmSndFDerivWithinAt_univ,
    ← differentiableWithinAt_univ] at hf h'f hV hW ⊢
Cleared hypotheses: hf, hV, hW
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
have 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
Tactic: refine le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
⊢ 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
have 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
Tactic: refine le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
have refine : ∀ (hxt : x - t ∈ support g), t ∈ -tsupport g + s
Tactic: refine mt (fun hxt => hu ?_) ht
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
have refine : (fun (x1 x2 : G) ↦ x1 + x2) (-(x - t)) x = t
Tactic: refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
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
⊢ 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
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
have refine : ∀ (i : G), ‖g i‖ ≤ ⨆ (i : G), ‖g i‖
Tactic: refine convolution_integrand_bound_right_of_le_of_subset _ (fun i => ?_) hx hu
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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
hcf : HasCompactSupport f
hf : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) : F) ≤
    (-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t
have h : Eq (α := ℝ) ((-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t)
  ((-tsupport f + s).indicator (fun (t : G) ↦ ‖L.flip‖ * ‖g t‖ * ⨆ (i : G), ‖f i‖) t)
Tactic: convert! hcf.convolution_integrand_bound_right L.flip hf hx using 1