mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u + mulInvariantVectorField v) (mulInvariantVectorField w) 1 =
    mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1 +
      mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1

Tactic:
mlieBracket_add_left

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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1 +
      mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1 =
    mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1 +
      mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1

case hV
𝕜 : 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
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField u x⟩) 1

case hV₁
𝕜 : 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
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1
Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
by
  obtain ⟨s', hxs', hfg⟩ := h'.exists_mem
  obtain ⟨s, hss', hs, hxs⟩ := mem_nhds_iff.mp hxs'
  refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
  · simpa using ⟨mem_domChart_source hf, by rwa [interior_eq_iff_isOpen.mpr hs]⟩
  · exact hfg (mem_of_mem_nhds hxs') ▸ mem_codChart_source hf
  · exact restr_mem_maximalAtlas _ hf.domChart_mem_maximalAtlas hs
  · trans s' ∩ f ⁻¹' hf.codChart.source
    · apply subset_inter
      · exact Subset.trans (by simp [interior_eq_iff_isOpen.mpr hs]) hss'
      · exact Subset.trans (by simp) hf.source_subset_preimage_source
    · rw [hfg.inter_preimage_eq]; exact inter_subset_right
  · exact hP.congr (hfg.mono hss' |>.mono (by grind)) <| hP.mono_source hs hf.property

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

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
y : PiLp p fun x ↦ ℝ
⊢ y ∈ {y | a ≤ y.ofLp i} \ {y | a < y.ofLp i} ↔ y ∈ {y | a = y.ofLp i}

Tactic:
simpa only [mem_sdiff, mem_ofPred_eq, not_lt] using antisymm_iff

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

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
⊢ interior (⋂ i, f i ⁻¹' Ici a) = ⋂ i, f i ⁻¹' Ioi a

Tactic:
interior_iInter_of_finite

Goal state after:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
⊢ ⋂ i, interior (f i ⁻¹' Ici a) = ⋂ i, f i ⁻¹' Ioi a
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ ⟨toLp 2 (update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0)), ⋯⟩ = ⟨xval, xprop⟩

Tactic:
by
    rw [Subtype.mk_eq_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]
    exact ⟨max_eq_left xprop, fun i _ => rfl⟩

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_ofPred, PiLp.zero_apply]

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

Goal state before:
pp: case pos
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
u : EuclideanHalfSpace 1
hz' : ↑(𝓡∂ 1) u ∈ ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target
hu : (↑u).ofLp 0 ≤ y - x
⊢ (↑((Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
        (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
      (↑(𝓡∂ 1) u) =
    (⇑φ ∘ fun x ↦ (x, 0)) (↑(𝓡∂ 1) u)

Tactic:
simp [hz, φ, φ₀, modelWithCornersEuclideanHalfSpace_symm_apply, u.property,
      IccLeftChart_symm_apply_of_le hu]

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
x : M
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
⊢ IsImmersionAtOfComplement PUnit.{u_2 + 1} I I n Subtype.val ⟨x, hx⟩

Tactic:
apply Manifold.IsImmersionAtOfComplement.of_opens

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

Goal state before:
pp: case mp
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
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

pp: case mpr
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
t₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀

Tactic:
· intro h
    rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem] at h
    obtain ⟨s, hs, h⟩ := h
    exact ⟨s, hs, fun t ht ↦ (h t ht).hasMFDerivWithinAt⟩

Goal state after:
case mpr
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
t₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀
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 ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ HasMFDerivAt[s] (↑(extChartAt I (γ t₀)) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))))

Tactic:
apply (HasMFDerivWithinAt.comp t (hasMFDerivWithinAt_extChartAt (I := I) hsrc) (hγ _ ht)
    (Set.subset_preimage_image _ _)).congr_mfderiv

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t)) =
    ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
t₀ : ℝ
hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
dt : ℝ
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
obtain ⟨ε, hε, h⟩ := hγ

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)

Tactic:
convert! (H₁.of_le le_top).comp' H₂ using 1

Goal state after:
case e'_23
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
⊢ Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source =
    Set.univ ∩ f ⁻¹' ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
t₀ : ℝ
hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
a : ℝ
ha : a ≠ 0
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)

Tactic:
obtain ⟨ε, hε, h⟩ := hγ

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)

Tactic:
have := congr_arg DFunLike.coe <| (this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)
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 ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ IsOpen s

Tactic:
isOpen_iff_mem_nhds

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
⊢ ∀ x ∈ s, s ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: x y : ↑I
⊢ volume (Ioc x y) = ENNReal.ofReal (↑y - ↑x)

Tactic:
simp only [volume_apply, image_subtype_val_Ioc, Real.volume_Ioc]

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)
x y : M
r : ℝ≥0∞
γ : Path x y
γ_smooth : ContMDiff (𝓡∂ 1) I 1 ⇑γ
hγ : ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑γ x_1) 1‖ₑ < r
⊢ ∃ γ, γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r

Tactic:
refine ⟨γ ∘ (projIcc 0 1 zero_le_one), by simp, by simp,
    contMDiffOn_comp_projIcc_iff.2 γ_smooth, ?_⟩

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)
x y : M
r : ℝ≥0∞
γ : Path x y
γ_smooth : ContMDiff (𝓡∂ 1) I 1 ⇑γ
hγ : ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑γ x_1) 1‖ₑ < r
⊢ pathELength I (⇑γ ∘ projIcc 0 1 ⋯) 0 1 < r
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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
s'_eq : s' =ᶠ[𝓝 x₀] s
t' : Set M' := t ∩ (extChartAt I' (f x₀)).source
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
⊢ mlieBracketWithin I (mpullbackWithin I I' f V s') (mpullbackWithin I I' f W s') s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

Tactic:
by
    apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem _ _ hx₀
    · apply nhdsWithin_le_nhds
      filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, hy]
    · apply nhdsWithin_le_nhds
      filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, hy]

Goal state after:
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:
funext 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✝² : ∀ (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
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:
calc cov σ x
    _ = cov ((ψ : M → 𝕜) • σ) x := by
      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
    _ = cov ((ψ : M → 𝕜) • σ') x := by rw [funext H]
    _ = cov σ' x := by
      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

Goal state after:
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 cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
inst✝³ : CompleteSpace 𝕜
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ s
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ (hcov.difference hcov' x) (σ x) = cov σ x - cov' σ x

Tactic:
simp only [difference, hx, reduceDIte]
  rw [TensorialAt.mkHom_apply _ hσ]
  rfl

Goal state after: