mathlib-initiative/mathlib-tactics huggingface dataset:
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.ι
        (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
          (smoothSheaf IM I M R).presheaf)
        U ≫
      (forgetStalk IM I M R x).inv ≫ ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    colimit.ι
        (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
          (smoothSheaf IM I M R).presheaf)
        U ≫
      smoothSheaf.evalHom IM I R x

Tactic:
change (colimit.ι _ U) ≫ _ = colimit.ι ((OpenNhds.inclusion x).op ⋙ _) U ≫ _

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 (evalHom IM I M R x)) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x
Module: Mathlib.Geometry.Manifold.Riemannian.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
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y)
γ : ℝ → M := ↑(extChartAt I x).symm ∘ ⇑η
⊢ segment ℝ (↑(extChartAt I x) x) (↑(extChartAt I x) y) ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}

Tactic:
apply Subset.trans _ hr

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ⋯
γ : ℝ → M := ⋯
⊢ segment ℝ (↑(extChartAt I x) x) (↑(extChartAt I x) y) ⊆ ball (↑(extChartAt I x) x) r ∩ range ↑I
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
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'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
⊢ mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀

Tactic:
rw [this, mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt
    hx₀ hn hst (by simp) (subset_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
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'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
⊢ mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ =
    mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
x : M
⊢ IsLocalRing ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)

Tactic:
apply IsLocalRing.of_nonunits_add

Goal state after:
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
x : M
⊢ ∀ (a b : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)),
    a ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) →
      b ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) →
        a + b ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk 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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
y : M
hy : ∀ᶠ (x_1 : M) in 𝓝[s] y, ↑(extChartAt I x) x_1 ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
hyU :
  ∀ᶠ (x_1 : M) in 𝓝[s] y,
    U x_1 =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)) x_1
hyV :
  ∀ᶠ (x_1 : M) in 𝓝[s] y,
    V x_1 =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)) x_1
h'yU :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (m' + 1)
    (fun x_1 ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I) x_1⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
h'yV :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (m' + 1)
    (fun x_1 ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
hy_chart : y ∈ (chartAt H x).source
hys : y ∈ s
⊢ m' + 1 ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.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
inst✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
⊢ r / C > 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝¹ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this✝ : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
this : ‖(Trivialization.symmL ℝ (trivializationAt F E x) x) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2
⊢ 0 ≤ r' * ‖v‖

Tactic:
by positivity

Goal state after:
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
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F 1 (e.localFrame b) e.baseSet
j : ι
⊢ (e.basisAt b hx) j = (he.toBasisAt hx) j

Tactic:
simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx]

Goal state after:
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
inst✝⁴ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
k : ℕ∞ω
x : M
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
⊢ e.baseSet ∈ 𝓝 x

Tactic:
by simp [e.open_baseSet.mem_nhds hxe]

Goal state after:
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
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : MDiffAt aux x
⊢ e.baseSet ∈ 𝓝 x

Tactic:
by simp [e.open_baseSet.mem_nhds hxe]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

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
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
V : M → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F V)
inst✝² : (x : M) → NormedAddCommGroup (V x)
inst✝¹ : (x : M) → InnerProductSpace ℝ (V x)
inst✝ : FiberBundle F V
cov : CovariantDerivative I F V
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ ((↑cov σ x) X₀) (τ x) - inner ℝ (σ x) ((↑cov τ x) X₀)

Tactic:
real_inner_comm

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
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
V : M → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F V)
inst✝² : (x : M) → NormedAddCommGroup (V x)
inst✝¹ : (x : M) → InnerProductSpace ℝ (V x)
inst✝ : FiberBundle F V
cov : CovariantDerivative I F V
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ (τ x) ((↑cov σ x) X₀) - inner ℝ (σ x) ((↑cov τ x) X₀)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
⊢ cov.derivMetricTensor x = 0 x

Tactic:
apply VectorBundle.injective_eval_mdifferentiableAt_sec I F

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
⊢ (fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) = (fun A Z x_1 ↦ A (Z x)) (0 x)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
⊢ (fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) = (fun A Z x_1 ↦ A (Z x)) (0 x)

Tactic:
ext1 σ

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
σ : (x : M) → V x
⊢ (fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) σ = (fun A Z x_1 ↦ A (Z x)) (0 x) σ