awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
this : ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)
⊢ γ t₁ ∈ v
have this₁ : γ' t₁ ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' v
Tactic: have : γ' t₁ ∈ (extChartAt I x).symm ⁻¹' v := by
    apply hr
    rw [← Metric.eball_coe, Metric.mem_eball, edist_eq_enorm_sub]
    convert! this
    simp [γ', hγx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
this_1 : ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)
this : γ' t₁ ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' v
⊢ γ t₁ ∈ v
have h : γ t₁ = (↑(extChartAt I x).symm : E → M) (γ' t₁)
Tactic: convert! mem_preimage.1 this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < c} ⊆ s
have rcases : ∀ (c : ℝ≥0) (c_pos : c > 0) (hc : {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s),
  ∃ c > 0, {y : M | riemannianEDist I x y < c} ⊆ s
Tactic: rcases setOf_riemannianEDist_lt_subset_nhds I hs with ⟨c, c_pos, hc⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
⊢ pathELength I γ a b =
    ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t))
have rw : ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
  ∫⁻ (t : ℝ) in Ioo a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t))
Tactic: rw [pathELength_eq_lintegral_mfderiv_Icc, restrict_Ioo_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
rw :
  ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t))
⊢ pathELength I γ a b =
    ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t))
have rw₁ : ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
  ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t))
Tactic: rw [pathELength_eq_lintegral_mfderiv_Icc, restrict_Ioo_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
⊢ pathELength I γ a b =
    ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
have rw : ∫⁻ (t : ℝ) in Ioo a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
  ∫⁻ (t : ℝ) in Ioo a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
        TangentSpace I (γ t))
Tactic: rw [pathELength_eq_lintegral_mfderiv_Icc, ← restrict_Ioo_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
⊢ ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
have apply : ∀ (t : ℝ) (ht : t ∈ Ioo a b),
  enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
        TangentSpace I (γ t))
Tactic: apply setLIntegral_congr_fun measurableSet_Ioo (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
t : ℝ
ht : t ∈ Ioo a b
⊢ enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
        TangentSpace I (γ t))
have rw : Icc a b ∈ 𝓝 t
Tactic: rw [mfderivWithin_of_mem_nhds]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
⊢ pathELength I γ a b = pathELength I γ' a b
have simp : ∫⁻ (t : ℝ) in Ioo a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
  ∫⁻ (t : ℝ) in Ioo a b,
    enorm (E := TangentSpace I (γ' t))
      ((mfderiv% γ' t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ' t)) 1 : TangentSpace I (γ' t))
Tactic: simp only [pathELength_eq_lintegral_mfderiv_Ioo]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
⊢ ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    ∫⁻ (t : ℝ) in Ioo a b,
      enorm (E := TangentSpace I (γ' t))
        ((mfderiv% γ' t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ' t)) 1 : TangentSpace I (γ' t))
have apply : ∀ (t : ℝ) (ht : t ∈ Ioo a b),
  enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    enorm (E := TangentSpace I (γ' t))
      ((mfderiv% γ' t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ' t)) 1 : TangentSpace I (γ' t))
Tactic: apply setLIntegral_congr_fun measurableSet_Ioo (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
⊢ enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    enorm (E := TangentSpace I (γ' t))
      ((mfderiv% γ' t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ' t)) 1 : TangentSpace I (γ' t))
have A : γ t = γ' t
Tactic: have A : γ t = γ' t := h ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
⊢ enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    enorm (E := TangentSpace I (γ' t))
      ((mfderiv% γ' t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ' t)) 1 : TangentSpace I (γ' t))
have h₁ : TangentSpace I (γ t) = TangentSpace I (γ' t) →
  (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) = (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ' t)) →
    Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) (mfderiv% γ t) (mfderiv% γ' t)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
e_1 : TangentSpace I (γ t) = TangentSpace I (γ' t)
e_1_1 : (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) = (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ' t))
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) (mfderiv% γ t) (mfderiv% γ' t)
have h₁ : γ =ᶠ[𝓝 t] γ'
Tactic: apply Filter.EventuallyEq.mfderiv_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
e_1 : TangentSpace I (γ t) = TangentSpace I (γ' t)
e_1_1 : (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) = (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ' t))
⊢ γ =ᶠ[𝓝 t] γ'
have h₁ : ∀ (a_1 : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ | x ∈ Ioo a b → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ γ x = γ' x) x} x} a_1
Tactic: filter_upwards [Ioo_mem_nhds ht.1 ht.2] with a ha using h ha
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
e_1 : TangentSpace I (γ t) = TangentSpace I (γ' t)
e_1_1 : (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) = (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ' t))
h₁ :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ | x ∈ Ioo a b → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ γ x = γ' x) x} x} a_1
⊢ γ =ᶠ[𝓝 t] γ'
have h₂ : ∀ a_1 ∈ Ioo a b, γ a_1 = γ' a_1
Tactic: filter_upwards [Ioo_mem_nhds ht.1 ht.2] with a ha using h ha
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
⊢ pathELength I γ a b + pathELength I γ b c = pathELength I γ a c
have symm : pathELength I γ a c = pathELength I γ a b + pathELength I γ b c
Tactic: symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
⊢ pathELength I γ a c = pathELength I γ a b + pathELength I γ b c
have this : Icc a c = Icc a b ∪ Ioc b c
Tactic: have : Icc a c = Icc a b ∪ Ioc b c := (Icc_union_Ioc_eq_Icc h h').symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (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
⊢ pathELength I γ a c = pathELength I γ a b + pathELength I γ b c
have rw : (∫⁻ (a : ℝ) in Icc a b,
      enorm (E := TangentSpace I (γ a))
        ((mfderiv% γ a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 : TangentSpace I (γ a))) +
    ∫⁻ (a : ℝ) in Ioc b c,
      enorm (E := TangentSpace I (γ a))
        ((mfderiv% γ a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 : TangentSpace I (γ a)) =
  pathELength I γ a b + pathELength I γ b c
Tactic: rw [pathELength, this, lintegral_union measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (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
rw :
  (∫⁻ (a : ℝ) in Icc a b,
        enorm (E := TangentSpace I (γ a))
          ((mfderiv% γ a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 : TangentSpace I (γ a))) +
      ∫⁻ (a : ℝ) in Ioc b c,
        enorm (E := TangentSpace I (γ a))
          ((mfderiv% γ a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 : TangentSpace I (γ a)) =
    pathELength I γ a b + pathELength I γ b c
⊢ pathELength I γ a c = pathELength I γ a b + pathELength I γ b c
have rw₁ : Disjoint (Icc a b) (Ioc b c)
Tactic: rw [pathELength, this, lintegral_union measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
⊢ ∫⁻ (t : (↑(Icc a b) : Type)),
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace (𝓡∂ 1) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    pathELength I (γ ∘ projIcc a b ⋯) a b
have rw : ∫⁻ (t : (↑(Icc a b) : Type)),
    enorm (E := TangentSpace I (γ t))
      ((mfderiv% γ t : (a : TangentSpace (𝓡∂ 1) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
  ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I ((γ ∘ projIcc a b sorry) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) t :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ projIcc a b sorry) t))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) t))
Tactic: rw [pathELength_eq_lintegral_mfderivWithin_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
⊢ ∫⁻ (t : (↑(Icc a b) : Type)),
      enorm (E := TangentSpace I (γ t))
        ((mfderiv% γ t : (a : TangentSpace (𝓡∂ 1) t) → TangentSpace I (γ t)) 1 : TangentSpace I (γ t)) =
    ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) t :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ projIcc a b ⋯) t))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) t))
have simp_rw : ∫⁻ (t : (↑(Icc a b) : Type)),
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ))) =
  ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I ((γ ∘ projIcc a b sorry) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) t :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ projIcc a b sorry) t))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) t))
Tactic: simp_rw [← mfderivWithin_comp_projIcc_one]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
⊢ ∫⁻ (t : (↑(Icc a b) : Type)),
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ))) =
    ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) t :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ projIcc a b ⋯) t))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) t))
have this : MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
  (Measure.restrict volume (Icc a b))
Tactic: have : MeasurePreserving (Subtype.val : Icc a b → ℝ) volume
    (volume.restrict (Icc a b)) := measurePreserving_subtype_coe measurableSet_Icc