mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffAt[s] x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hf : MDiffAt[s] f x₀
⊢ (mfderiv[t] g (f x₀) ∘SL mfderiv[s] f x₀).inverse (V ((g ∘ f) x₀)) =
    (mfderiv[s] f x₀).inverse ((mfderiv[t] g (f x₀)).inverse (V (g (f x₀))))

Tactic:
IsInvertible.inverse_comp_apply_of_right hf',

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffAt[s] x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hf : MDiffAt[s] f x₀
⊢ (mfderiv[s] f x₀).inverse ((mfderiv[t] g (f x₀)).inverse (V ((g ∘ f) x₀))) =
    (mfderiv[s] f x₀).inverse ((mfderiv[t] g (f x₀)).inverse (V (g (f x₀))))
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : M → F
X : M
x✝ : TangentSpace I X
⊢ (d[univ] f X) x✝ = (d% f X) x✝

Tactic:
simp [mvfderiv, mvfderivWithin]

Goal state after:
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
have M : minSmoothness 𝕜 3 ≠ 0 := lt_of_lt_of_le (by simp) le_minSmoothness |>.ne'
  have A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3 := by
    rw [← minSmoothness_add]
    norm_num
  let fg : G → TangentBundle I G := fun g ↦ TotalSpace.mk' E g 0
  have sfg : CMDiff (minSmoothness 𝕜 2) fg := contMDiff_zeroSection _ _
  let fv : G → TangentBundle I G := fun _ ↦ TotalSpace.mk' E 1 v
  have sfv : CMDiff (minSmoothness 𝕜 2) fv := contMDiff_const
  let F₁ : G → (TangentBundle I G × TangentBundle I G) := fun g ↦ (fg g, fv g)
  have S₁ : CMDiff (minSmoothness 𝕜 2) F₁ := sfg.prodMk sfv
  let F₂ : (TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G) :=
    (equivTangentBundleProd I G I G).symm
  have S₂ : CMDiff (minSmoothness 𝕜 2) F₂ := contMDiff_equivTangentBundleProd_symm
  let F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G :=
    tangentMap% (fun (p : G × G) ↦ p.1 * p.2)
  have S₃ : CMDiff (minSmoothness 𝕜 2) F₃ := by
    apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl
    rw [A]
    exact contMDiff_mul I (minSmoothness 𝕜 3)
  let S := (S₃.comp S₂).comp S₁
  convert! S with g
  · simp [F₁, F₂, F₃, fg, fv]
  · simp only [comp_apply, tangentMap, F₃, F₂, F₁, fg, fv]
    rw [mfderiv_prod_eq_add_apply ((contMDiff_mul I (minSmoothness 𝕜 3)).mdifferentiableAt M)]
    simp +instances [mulInvariantVectorField]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ (fderivWithin 𝕜 f' s' x₀) (V' x₀) • W' x₀
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' (f' • W') s') x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x

Tactic:
trans mpullback I 𝓘(𝕜, E) ((extChartAt I x)) (fun y ↦ A y + B y) x

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
f' : E → 𝕜 := ⋯
s' : Set E := ⋯
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' (f' • W') s') x =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (fun y ↦ A y + B y) x

𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
f' : E → 𝕜 := ⋯
s' : Set E := ⋯
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (fun y ↦ A y + B y) x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hW : (MDiffAt fun x ↦ ⟨x, W x⟩) x
⊢ mlieBracket I V (f • W) x = (d% f x) (V x) • W x + f x • mlieBracket I V W x

Tactic:
← mdifferentiableWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hW : (MDiffAt[univ] fun x ↦ ⟨x, W x⟩) x
⊢ mlieBracket I V (f • W) x = (d% f x) (V x) • W x + f x • mlieBracket I V W x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hV : (MDiffAt fun x ↦ ⟨x, V x⟩) x
⊢ mlieBracket I (f • V) W x = -(d% f x) (W x) • V x + f x • mlieBracket I V W x

Tactic:
← mdifferentiableWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun x ↦ ⟨x, V x⟩) x
⊢ mlieBracket I (f • V) W x = -(d% f x) (W x) • V x + f x • mlieBracket I V W x
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ↑z < y
⊢ ↑z ∈ (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.source

Tactic:
simp [Homeomorph.addLeft]

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) ↑w
A : (MDiffAt fun z ↦ ↑z) w
⊢ MDiffAt f w

Tactic:
← mdifferentiableWithinAt_univ

Goal state after:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) ↑w
A : (MDiffAt[univ] fun z ↦ ↑z) w
⊢ MDiffAt[univ] f w
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h✝ : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
s' : Set ℝ
hs' : s' ∈ 𝓝 t
h : ∀ y ∈ s', HasMFDerivAt% γ y (ContinuousLinearMap.smulRight 1 (v (γ y)))
⊢ HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
exact h _ (mem_of_mem_nhds hs')

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
u v : ↑(sphere 0 1)
⊢ u = v ↔ ⟪↑u, ↑v⟫_ℝ = 1

Tactic:
simp [Subtype.ext_iff, inner_eq_one_iff_of_norm_eq_one]

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ 0 ∈ Ioo (-a') a'

Tactic:
mem_Ioo

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ -a' < 0 ∧ 0 < a'
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E := ⋯
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip✝ : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x ↦ v') t) ((fun x ↦ s) t)
hsrc : ∀ {g : ℝ → M}, IsMIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
⊢ ∀ᶠ (x : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x ↦ v') x ((↑(extChartAt I (g t₀)) ∘ g) x)) x

Tactic:
apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
      rintro t ⟨ht1, ht2⟩
      rw [hv', h']
      apply ht2.congr_deriv
      congr <;>
      rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
⊢ -(ε / 2) < 0

Tactic:
rw [neg_lt, neg_zero]; exact half_pos hε

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
ha : ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
hlt : asup - ε / 2 < a
⊢ False

Tactic:
obtain ⟨γ, h0, hγ⟩ := ha

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
⊢ False
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
⊢ (∃ T > 0, Periodic γ T) ↔ ¬Injective γ

Tactic:
refine ⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
⊢ ¬Injective γ → ∃ T > 0, Periodic γ T
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: s : Set ↑I
hs : MeasurableSet s
| volume (Subtype.val '' σ ⁻¹' s)

Tactic:
image_coe_preimage_symm,

Goal state after:
s : Set ↑I
hs : MeasurableSet s
| volume ((fun x ↦ 1 - x) ⁻¹' Subtype.val '' s)
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case st
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ⋯
⊢ Icc 0 1 ⊆ ⇑η ⁻¹' Icc a b

Tactic:
rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
      simp [hab]

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case h'f
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ DifferentiableOn ℝ η (Icc a b)

Tactic:
simp only [η]
      apply (ContDiff.contDiffOn _).differentiableOn one_ne_zero
      fun_prop

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
F : Type u_5
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F V)
inst✝⁹ : (x : M) → AddCommGroup (V x)
inst✝⁸ : (x : M) → Module 𝕜 (V x)
inst✝⁷ : (x : M) → TopologicalSpace (V x)
inst✝⁶ : FiberBundle F V
A : Type u_9
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
c : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x →ₗ[𝕜] 𝕜 := Trivialization.localFrameCoeff I t b
hs : ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x},
    MDiffAt (T% σ) x → ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt ((LinearMap.piApply (c i)) σ) x
hΦ_eq : ∀ {σ : (x : M) → V x}, MDiffAt (T% σ) x → Φ σ = Φ fun x' ↦ ∑ i, (c i x') (σ x') • s i x'
⊢ Φ σ = Φ σ'

Tactic:
hΦ_eq hσ,

Goal state after:
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
F : Type u_5
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F V)
inst✝⁹ : (x : M) → AddCommGroup (V x)
inst✝⁸ : (x : M) → Module 𝕜 (V x)
inst✝⁷ : (x : M) → TopologicalSpace (V x)
inst✝⁶ : FiberBundle F V
A : Type u_9
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
c : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x →ₗ[𝕜] 𝕜 := Trivialization.localFrameCoeff I t b
hs : ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x},
    MDiffAt (T% σ) x → ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt ((LinearMap.piApply (c i)) σ) x
hΦ_eq : ∀ {σ : (x : M) → V x}, MDiffAt (T% σ) x → Φ σ = Φ fun x' ↦ ∑ i, (c i x') (σ x') • s i x'
⊢ (Φ fun x' ↦ ∑ i, (c i x') (σ x') • s i x') = Φ σ'
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H✝ : Type u_3
inst✝¹¹ : TopologicalSpace H✝
I : ModelWithCorners 𝕜 E H✝
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H✝ M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt% ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + (d% ψ x).smulRight (σ x)
⊢ cov (ψ • σ') x = cov σ' x

Tactic:
simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

Goal state after: