mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Instances.Icc

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

Tactic:
apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
      · have : ContDiff ℝ n (fun y ↦ -x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
      · have : ContDiff ℝ n (fun y ↦ x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ, Homeomorph.addLeft]

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

Goal state before:
pp: case neg
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ¬↑z < y
⊢ EqOn
    (↑((Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target

pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ¬↑z < y
⊢ (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph ∈ maximalAtlas 𝓘(ℝ, ℝ) n ℝ

Tactic:
;

Goal state after:
case neg
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ¬↑z < y
⊢ EqOn
    (↑((Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target

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
⊢ (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph ∈ maximalAtlas 𝓘(ℝ, ℝ) n ℝ
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContinuousAt (projIcc x y ⋯) z

Tactic:
;

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContinuousAt (projIcc x y ⋯) z
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

pp: case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ (mfderiv% f (projIcc x y ⋯ ↑w) ∘SL mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

pp: case pos.hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ MDiffAt f (projIcc x y ⋯ ↑w)

pp: case pos.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) ↑w

pp: case pos.hxs
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ UniqueMDiffAt[Icc x y] ↑w

Tactic:
;

Goal state after:
case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ (mfderiv% f (projIcc x y ⋯ ↑w) ∘SL mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

case pos.hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ MDiffAt f (projIcc x y ⋯ ↑w)

case pos.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) ↑w

case pos.hxs
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ UniqueMDiffAt[Icc 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
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ stereoInvFun hv w ≠ ⟨v, ⋯⟩

Tactic:
refine Subtype.coe_ne_coe.1 ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ ↑(stereoInvFun hv w) ≠ ↑⟨v, ⋯⟩
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ × Rˣ
⊢ (val ∘ fun x ↦ x.1 * x.2) x✝ = ((fun x ↦ x.1 * x.2) ∘ fun x ↦ (↑x.1, ↑x.2)) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ × Rˣ
⊢ (val ∘ fun x ↦ x.1 * x.2) x✝ = ((fun x ↦ x.1 * x.2) ∘ fun x ↦ (↑x.1, ↑x.2)) x✝
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R) n fun p ↦ p.1 * p.2

Tactic:
by
    apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val
    have : (val : Rˣ → R) ∘ (fun x : Rˣ × Rˣ => x.1 * x.2) =
      (fun x : R × R => x.1 * x.2) ∘ (fun x : Rˣ × Rˣ => (x.1, x.2)) := by ext; simp
    rw [this]
    have : ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R × R) n
      (fun x : Rˣ × Rˣ => ((x.1 : R), (x.2 : R))) :=
      (contMDiff_val.comp contMDiff_fst).prodMk_space (contMDiff_val.comp contMDiff_snd)
    refine ContMDiff.comp ?_ this
    rw [contMDiff_iff_contDiff]
    exact contDiff_mul

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ
⊢ (val ∘ fun x ↦ x⁻¹) x✝ = (Ring.inverse ∘ val) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ
⊢ (val ∘ fun x ↦ x⁻¹) x✝ = (Ring.inverse ∘ val) x✝
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
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
constructor
  · 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⟩
  · rintro ⟨s, hs, h⟩
    rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]
    obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs
    refine ⟨s', h2.mem_nhds h3, ?_⟩
    intro t ht
    apply (h t (h1 ht)).hasMFDerivAt
    rw [mem_nhds_iff]
    exact ⟨s', h1, h2, ht⟩

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Tactic:
rw [contMDiff_iff]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ Continuous Subtype.val ∧
    ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
      ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
        ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)
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₀ dt : ℝ
⊢ IsMIntegralCurveAt (γ ∘ fun x ↦ x + dt) v (t₀ - dt) ↔ IsMIntegralCurveAt γ v t₀

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
  convert! hγ.comp_add (-dt)
  · ext t
    simp only [Function.comp_apply, neg_add_cancel_right]
  · simp only [sub_neg_eq_add, sub_add_cancel]

Goal state after:
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
hγ : IsMIntegralCurve γ v
a : ℝ
⊢ IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)

Tactic:
by
  rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *
  exact hγ.comp_mul _

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val
⊢ ContMDiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ω fun z ↦ z.1 * z.2

Tactic:
rw [contMDiff_iff]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val
⊢ (Continuous fun z ↦ z.1 * z.2) ∧
    ∀ (x : ℂ × ℂ) (y : ℂ),
      ContDiffOn ℝ ω (↑(extChartAt 𝓘(ℝ, ℂ) y) ∘ (fun z ↦ z.1 * z.2) ∘ ↑(extChartAt (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) x).symm)
        ((extChartAt (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) x).target ∩
          ↑(extChartAt (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) x).symm ⁻¹' (fun z ↦ z.1 * z.2) ⁻¹' (extChartAt 𝓘(ℝ, ℂ) y).source)
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: case neg
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 t : ℝ
ht : t ∈ Ioo (-a) a
hlt : a ≤ |t| + 1
⊢ (fun t ↦ γ (|t| + 1) t) t = γ a t

Tactic:
exact eqOn_of_isMIntegralCurveOn_Ioo hv γ hγx hγ
      (neg_lt_self_iff.mp <| lt_trans ht.1 ht.2) hlt ht |>.symm

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

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
⊢ ⇑(equivTangentBundleProd I M I' M') = fun p ↦ (⟨p.proj.1, p.snd.1⟩, ⟨p.proj.2, p.snd.2⟩)

Tactic:
;

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
⊢ ⇑(equivTangentBundleProd I M I' M') = fun p ↦ (⟨p.proj.1, p.snd.1⟩, ⟨p.proj.2, p.snd.2⟩)
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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

Tactic:
;

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
⊢ 0 < ε / 2
Module: Mathlib.Geometry.Manifold.Metrizable

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
this : LocallyCompactSpace H
⊢ MetrizableSpace M

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
this : LocallyCompactSpace H
⊢ MetrizableSpace M
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 c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ (∫⁻ (a : ℝ) in Icc a b, ‖(mfderiv% γ a) 1‖ₑ) + ∫⁻ (a : ℝ) in Ioc b c, ‖(mfderiv% γ a) 1‖ₑ =
    pathELength I γ a b + pathELength I γ b c

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 c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ Disjoint (Icc a b) (Ioc b c)

Tactic:
;

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)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ (∫⁻ (a : ℝ) in Icc a b, ‖(mfderiv% γ a) 1‖ₑ) + ∫⁻ (a : ℝ) in Ioc b c, ‖(mfderiv% γ a) 1‖ₑ =
    pathELength I γ a b + pathELength I γ b c

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 c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ Disjoint (Icc a b) (Ioc b c)
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ ⨅ γ, ⨅ (_ : ContMDiff (𝓡∂ 1) I 1 ⇑γ), ∫⁻ (x_2 : ↑unitInterval), ‖(mfderiv% ⇑γ x_2) 1‖ₑ ≤
    ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ

Tactic:
;

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)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ ⨅ γ, ⨅ (_ : ContMDiff (𝓡∂ 1) I 1 ⇑γ), ∫⁻ (x_2 : ↑unitInterval), ‖(mfderiv% ⇑γ x_2) 1‖ₑ ≤
    ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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

Tactic:
apply Monotone.monotoneOn
      apply Real.smoothTransition.monotone.comp
      intro t u htu
      dsimp only
      gcongr

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

Goal state before:
pp: case hγ
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
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ MDiff[Icc 0 1] γ

Tactic:
apply γ_smooth.mdifferentiableOn one_ne_zero

Goal state after: