mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst✝²⁸ : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst✝²⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁵ : NormedAddCommGroup F₁
inst✝²⁴ : NormedSpace 𝕜 F₁
inst✝²³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²² : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst✝²¹ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁰ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁹ : NormedAddCommGroup F₂
inst✝¹⁸ : NormedSpace 𝕜 F₂
inst✝¹⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁶ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_10
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_11
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
EM : Type u_12
inst✝¹⁰ : NormedAddCommGroup EM
inst✝⁹ : NormedSpace 𝕜 EM
HM : Type u_13
inst✝⁸ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace HM M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hϕ : MDiffAt[s] (T% ϕ) x
hv : MDiffAt[s] (T% v) x
⊢ (MDiffAt[s] fun m ↦ ⟨b m, (ϕ m) (v m)⟩) x

Tactic:
simp only [mdifferentiableWithinAt_hom_bundle] at hϕ

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst✝²⁸ : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst✝²⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁵ : NormedAddCommGroup F₁
inst✝²⁴ : NormedSpace 𝕜 F₁
inst✝²³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²² : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst✝²¹ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁰ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁹ : NormedAddCommGroup F₂
inst✝¹⁸ : NormedSpace 𝕜 F₂
inst✝¹⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁶ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_10
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_11
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
EM : Type u_12
inst✝¹⁰ : NormedAddCommGroup EM
inst✝⁹ : NormedSpace 𝕜 EM
HM : Type u_13
inst✝⁸ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace HM M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hv : MDiffAt[s] (T% v) x
hϕ : (MDiffAt[s] fun x ↦ b x) x ∧ (MDiffAt[s] fun x_1 ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) x
⊢ (MDiffAt[s] fun m ↦ ⟨b m, (ϕ m) (v m)⟩) 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
s : Set M
x : M
F : Type u_18
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : M → F
inst✝ : IsManifold I 1 M
hf :
  DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ MDiffAt[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

Tactic:
simpa [extChartAt_self_eq] using hf.mdifferentiableWithinAt

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
hφ : IsImmersionAtOfComplement F J J' n φ (f x)
x✝ : ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x
hf : ContinuousAt f x
h' : ContMDiffAt I J' n (φ ∘ f) x
this : hφ.domChart.source ∈ 𝓝 (f x)
⊢ ContMDiffAt I J n f x

Tactic:
obtain ⟨t, ht, htopen, hxt⟩ := mem_nhds_iff.mp (hf this)

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
hφ : IsImmersionAtOfComplement F J J' n φ (f x)
x✝ : ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x
hf : ContinuousAt f x
h' : ContMDiffAt I J' n (φ ∘ f) x
this : hφ.domChart.source ∈ 𝓝 (f x)
t : Set M
ht : t ⊆ f ⁻¹' hφ.domChart.source
htopen : IsOpen[inst✝⁵] t
hxt : x ∈ t
⊢ ContMDiffAt I J n f x
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
⊢ IsImmersionAtOfComplement Unit I I n Sum.inl x

Tactic:
apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inl x))
    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inl x))

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
⊢ EqOn (↑((chartAt H (Sum.inl x)).extend I) ∘ Sum.inl ∘ ↑((chartAt H x).extend I).symm)
    (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E Unit) ∘ fun x ↦ (x, 0)) ((chartAt H x).extend I).target
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
⊢ ContMDiff I J n f ↔ Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)

Tactic:
refine ⟨fun h ↦ ⟨h.continuous, hφ.contMDiff.comp h⟩, fun ⟨h, h'⟩ x ↦ ?_⟩
  rw [ContMDiffAt.iff_comp_isImmersionAtOfComplement (hφ (f x))]
  exact ⟨h.continuousAt, h' x⟩

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
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : StrongDual ℝ E) 0 := by
    convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
    simp only [map_zero, smul_zero]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
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₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
intro ⟨s, hs, h⟩
    rw [Metric.mem_nhds_iff] at hs
    obtain ⟨ε, hε, hε'⟩ := hs
    refine ⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩

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

Goal state before:
pp: case e'_11
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v v' : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
U' : ↥(ℝ ∙ ↑v')ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
H₁ : ContDiffOn ℝ ω (⇑U' ∘ stereoToFun ↑v') {x | ((innerSL ℝ) ↑v') x ≠ 1}
H₂ : ContDiff ℝ ω ((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm)
⊢ {a | ↑(stereographic' n v).symm (id a) ≠ v'} =
    {a | ((innerSL ℝ) ↑v') (((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm) a) ≠ 1}

Tactic:
simp only [id, comp_apply, OpenPartialHomeomorph.coe_toPartialEquiv_symm,
        innerSL_apply_apply, Ne, sphere_ext_iff, real_inner_comm (v' : E)]

Goal state after:
case e'_11
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v v' : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
U' : ↥(ℝ ∙ ↑v')ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
H₁ : ContDiffOn ℝ ω (⇑U' ∘ stereoToFun ↑v') {x | ((innerSL ℝ) ↑v') x ≠ 1}
H₂ : ContDiff ℝ ω ((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm)
⊢ {a | ¬⟪↑v', ↑(↑(stereographic' n v).symm a)⟫_ℝ = 1} =
    {a | ¬⟪↑v', stereoInvFunAux (↑v) ((ℝ ∙ ↑v)ᗮ.subtypeL (U.symm a))⟫_ℝ = 1}
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₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v) (t₀ / a)
⊢ IsMIntegralCurveAt γ v t₀

Tactic:
convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)

Goal state after:
case e'_10
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γ : IsMIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v) (t₀ / a)
⊢ γ = (γ ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

case e'_11
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γ : IsMIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v) (t₀ / a)
⊢ v = a⁻¹ • a • v

case e'_12
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γ : IsMIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v) (t₀ / a)
⊢ t₀ = t₀ / a / 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)
⊢ ↑(stereographic' n (-v)) v = 0

Tactic:
dsimp [stereographic']
  simp only [EmbeddingLike.map_eq_zero_iff]
  apply stereographic_neg_apply

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
⊢ EqOn (γ a') (γ a) (Ioo (-a') a')

Tactic:
apply isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
    (hγ a' (by positivity)) ((hγ a (lt_of_lt_of_le hpos hle)).mono _)
    (by rw [hγx a, hγx a'])
  · rw [mem_Ioo]
    exact ⟨neg_lt_zero.mpr hpos, by positivity⟩
  · apply Ioo_subset_Ioo <;> linarith

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
⊢ False

Tactic:
set asup := sSup s with hasup

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
⊢ 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
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
⊢ Subtype.val ⁻¹' closure (Subtype.val '' Subtype.val ⁻¹' {t | γ t = γ' t}) ⊆ Subtype.val ⁻¹' {t | γ t = γ' t}

Tactic:
preimage_ofPred_eq

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
⊢ Subtype.val ⁻¹' closure (Subtype.val '' {a_1 | γ ↑a_1 = γ' ↑a_1}) ⊆ {a_1 | γ ↑a_1 = γ' ↑a_1}
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: ⊢ map σ volume = volume

Tactic:
by
    ext s hs
    apply symmMeasurableEquiv.map_apply _ |>.trans
    conv_lhs => rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]

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
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
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y

Tactic:
rcases exists_between ha'b with ⟨b', ha'b', hb'b⟩

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
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 = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y
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
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x v : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact real_inner_self_nonneg

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
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₀
⊢ 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:
by
  have : mpullback I I' f (mlieBracketWithin I' V W t) x₀ =
      mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ := by
    simp only [mpullback, mpullbackWithin]
    congr
    apply (mfderivWithin_eq_mfderiv (hu _ hx₀) _).symm
    exact hf.mdifferentiableAt (two_pos.trans_le (le_minSmoothness.trans hn)).ne'
  rw [this, mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt
    hx₀ hn hst (by simp) (subset_univ _)]
  apply Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
  · rw [insert_eq_of_mem hx₀]
    filter_upwards [nhdsWithin_le_nhds ((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1
      (hf.of_le (le_minSmoothness.trans hn))), self_mem_nhdsWithin] with y hy h'y
    simp only [mpullback, mpullbackWithin]
    congr
    apply mfderivWithin_eq_mfderiv (hu _ h'y)
    exact hy.mdifferentiableAt two_ne_zero
  · rw [insert_eq_of_mem hx₀]
    filter_upwards [nhdsWithin_le_nhds ((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1
      (hf.of_le (le_minSmoothness.trans hn))), self_mem_nhdsWithin] with y hy h'y
    simp only [mpullback, mpullbackWithin]
    congr
    apply mfderivWithin_eq_mfderiv (hu _ h'y)
    exact hy.mdifferentiableAt two_ne_zero

Goal state after:
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
f : M → N
hf : ContMDiff IM IN ∞ f
x : ↑↑(locallyRingedSpace IM M).toPresheafedSpace
a : ↑((locallyRingedSpace IN N).presheaf.stalk ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x))
ha :
  ¬(smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
        ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x)) a) =
      0
⊢ (smoothSheafCommRing.eval IN 𝓘(𝕜, 𝕜) N 𝕜 ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x)) a =
    (smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x)) a)

Tactic:
exact (congr($(stalkMap_locallyRingedSpaceMapAux f hf x) a)).symm

Goal state after: