mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: case intro.mpr
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
val✝ : Fintype ι
h : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x

Tactic:
·

Goal state after:
case intro.mpr
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
val✝ : Fintype ι
h : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case h'U
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x

pp: case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

pp: case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
·

Goal state after:
case h'U
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

pp: case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
·

Goal state after:
case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
·

Goal state after:
case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case h
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
A : ∑' (x : ↑t0), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε / 2
i : Fin N
this : Encodable ↑(S i)
⊢ ∀ (i_1 : ↑(S i)), MeasurableSet (closedBall (↑↑i_1) (r1 ↑↑i_1))

Tactic:
·

Goal state after:
case h
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
A : ∑' (x : ↑t0), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε / 2
i : Fin N
this : Encodable ↑(S i)
⊢ ∀ (i_1 : ↑(S i)), MeasurableSet (closedBall (↑↑i_1) (r1 ↑↑i_1))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y ↦ ↑(N y).symm) s x) v =
              -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm

Tactic:
have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y := by
    filter_upwards [hU] with y hy
    simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y ↦ ↑(N y).symm) s x) v =
              -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case e'_4
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
⊢ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2

Tactic:
·

Goal state after:
case e'_4
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
⊢ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case hc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm) s x

pp: case hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ V (f y)) s x

Tactic:
·

Goal state after:
case hc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm) s x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ V (f y)) s x

Tactic:
·

Goal state after:
case hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ V (f y)) s x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case h₁
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fun x ↦ (fderivWithin 𝕜 f s x).inverse (V (f x))) =ᶠ[𝓝[s] x] fun y ↦ ↑(M y).symm (V (f y))

pp: case hx
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Tactic:
·

Goal state after:
case h₁
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fun x ↦ (fderivWithin 𝕜 f s x).inverse (V (f x))) =ᶠ[𝓝[s] x] fun y ↦ ↑(M y).symm (V (f y))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case hx
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Tactic:
·

Goal state after:
case hx
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case h₁
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ (fun t ↦ f₀ (x + t • v)) =ᶠ[𝓝[(fun t ↦ x + t • v) ⁻¹' s] 0] fun t ↦ f₁ (x + t • v)

pp: case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + 0 • v) = f₁ (x + 0 • v)

Tactic:
·

Goal state after:
case h₁
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ (fun t ↦ f₀ (x + t • v)) =ᶠ[𝓝[(fun t ↦ x + t • v) ⁻¹' s] 0] fun t ↦ f₁ (x + t • v)
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + 0 • v) = f₁ (x + 0 • v)

Tactic:
·

Goal state after:
case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + 0 • v) = f₁ (x + 0 • v)
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : 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 : ¬(fderivWithin 𝕜 f s x).IsInvertible
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

pp: case pos
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : 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 : (fderivWithin 𝕜 f s x).IsInvertible
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : 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 : ¬(fderivWithin 𝕜 f s x).IsInvertible
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x