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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := ⋯
v : (x : M) → TangentSpace I' (f x) := ⋯
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := ⋯
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
⊢ MDiffAt inverse (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderiv[s] f x₀))

Tactic:
apply ContMDiffAt.mdifferentiableAt _ one_ne_zero

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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := ⋯
v : (x : M) → TangentSpace I' (f x) := ⋯
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := ⋯
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
⊢ ContMDiffAt 𝓘(𝕜, E →L[𝕜] E') 𝓘(𝕜, E' →L[𝕜] E) 1 inverse
    (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderiv[s] f x₀))
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s = lieBracketWithin 𝕜 V W s

Tactic:
ext x
  simp [mlieBracketWithin_apply]

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

Goal state before:
pp: case hg
𝕜 : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun b ↦ g⁻¹ * b) (g * h * 1)

pp: case hf
𝕜 : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun x ↦ g * h * x) 1

Tactic:
· exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

Goal state after:
case hf
𝕜 : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun x ↦ g * h * x) 1
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: case hf
𝕜 : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun x ↦ g * h * x) 1

Tactic:
· exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this

Tactic:
dsimp

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦ toLp 2 fun x_1 ↦ w - x
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this

Tactic:
dsimp

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦ toLp 2 fun x ↦ y - w
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : ℕ∞ω
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
by
  have h₀ : ContDiff ℝ ω fun w : E => ‖w‖ ^ 2 := contDiff_norm_sq ℝ
  have h₁ : ContDiff ℝ ω fun w : E => (‖w‖ ^ 2 + 4)⁻¹ := by
    refine (h₀.add contDiff_const).inv ?_
    intro x
    nlinarith
  have h₂ : ContDiff ℝ ω fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v := by
    refine (contDiff_const.smul contDiff_id).add ?_
    exact (h₀.sub contDiff_const).smul contDiff_const
  exact (h₁.smul h₂).of_le le_top

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    w

Tactic:
have h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0 :=
    Submodule.orthogonalProjectionOnto_orthogonalComplement_singleton_eq_zero v

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    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
⊢ IsMIntegralCurveOn γ v s

Tactic:
by
  intro t ht
  apply HasMFDerivAt.hasMFDerivWithinAt
  obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
  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
v : E
hv✝ : ‖v‖ = 1
x : ↑(sphere 0 1)
hv : ‖↑x‖ = 1
hx : x ∈ {⟨v, ⋯⟩}ᶜ
h : ↑x = v
⊢ ↑x = ↑⟨v, ⋯⟩

Tactic:
dsimp

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv✝ : ‖v‖ = 1
x : ↑(sphere 0 1)
hv : ‖↑x‖ = 1
hx : x ∈ {⟨v, ⋯⟩}ᶜ
h : ↑x = v
⊢ ↑x = v
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↑(sphere 0 1)
h : w ∈ {⟨v, ?m.125⟩}ᶜ
⊢ ↑w ∈ {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
dsimp

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↑(sphere 0 1)
h : w ∈ {⟨v, ?m.125⟩}ᶜ
⊢ ¬⟪v, ↑w⟫ = 1
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₀
t : ℝ
ht1 : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
ht2 : HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((tangentCoordChange I (g t) (g t₀) (g t)) (v (g t))) t
⊢ (tangentCoordChange I (g t) (g t₀) (g t)) (v (g t)) =
    (fun x x_1 ↦
        (tangentCoordChange I (↑(extChartAt I (g t₀)).symm x_1) (g t₀) (↑(extChartAt I (g t₀)).symm x_1))
          (v (↑(extChartAt I (g t₀)).symm x_1)))
      t ((↑(extChartAt I (g t₀)) ∘ g) t)

Tactic:
congr <;>
      rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]

Goal state after:
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
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t : { x // x ∈ Ioo a b }
ht : ↑t ∈ closure (Subtype.val '' {a_1 | γ ↑a_1 = γ' ↑a_1})
⊢ t ∈ {a_1 | γ ↑a_1 = γ' ↑a_1}

Tactic:
← closure_subtype

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
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t : { x // x ∈ Ioo a b }
ht : t ∈ closure {a_1 | γ ↑a_1 = γ' ↑a_1}
⊢ t ∈ {a_1 | γ ↑a_1 = γ' ↑a_1}
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

Tactic:
by
  rcases h.eq_or_lt with rfl | h
  · simp
  have f_im : f '' (Icc a b) = Icc (f a) (f b) := h'f.continuousOn.image_Icc_of_monotoneOn h.le hf
  simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
  have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
  rw [lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc B hf]
  apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
  have : (mfderiv[Icc a b] (γ ∘ f) t) =
      (mfderiv[Icc (f a) (f b)] γ (f t)) ∘L mfderiv[Icc a b] f t := by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht
  rw [this]
  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
  have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace% (f t)) := by
    simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
    rfl
  rw [this]
  have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg
  simp only [map_smul, enorm_smul, ← Real.enorm_of_nonneg this, f_im]

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

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✝¹ : (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
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ riemannianEDist I x y ≤ pathELength I γ a b

Tactic:
have hη : CMDiff[Icc 0 1] 1 (γ ∘ η) := by
    apply hγ.comp
    · rw [contMDiffOn_iff_contDiffOn]
      exact η.contDiff.contDiffOn
    · rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
      simp [hab]

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✝¹ : (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
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
⊢ riemannianEDist I x y ≤ pathELength I γ a b
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv =
    ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))

Tactic:
dsimp

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv =
    ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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
inst✝² : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∉ e.baseSet
i : ι
⊢ localFrameCoeff I e b i x = 0

Tactic:
by
  simpa [localFrameCoeff] using
    (e.isLocalFrameOn_localFrame_baseSet I 1 b).coeff_apply_of_notMem hx i

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

Goal state before:
pp: case insert
𝕜 : 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
hΦ : TensorialAt I F Φ x
ι : Type u_10
σ : ι → (x : M) → V x
a : ι
s : Finset ι
ha : a ∉ s
h : (∀ i ∈ s, MDiffAt (T% σ) x) → (Φ fun x' ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
hσ : ∀ i ∈ insert a s, MDiffAt (T% σ) x
⊢ (Φ fun x' ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a s, Φ (σ i)

Tactic:
| insert a s ha h =>

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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
c : 𝕜
v : V x
⊢ Φ (extend F (c • v)) = (RingHom.id 𝕜) c • Φ (extend F v)

Tactic:
dsimp

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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
c : 𝕜
v : V x
⊢ Φ (extend F (c • v)) = c • Φ (extend F v)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - (-VectorField.mlieBracket I (extend E Y₀) (extend E X₀)) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)

Tactic:
dsimp

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
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - -VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)