awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
h₂ h₃ : ∀ (a_1 : ℝ) (ha : a_1 ∈ Ioo a b), γ a_1 = γ' a_1
⊢ γ =ᶠ[𝓝 t] γ'

Tactic:
filter_upwards [Ioo_mem_nhds ht.1 ht.2] with a ha using h ha

Premises used: Ioo_mem_nhds, And.right, And.left
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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 γ γ' (Icc a b)
⊢ pathELength I γ a b = pathELength I γ' a b

Tactic:
pathELength_congr_Ioo (fun _ hx ↦ h ⟨hx.1.le, hx.2.le⟩)

Premises used: Manifold.pathELength_congr_Ioo, LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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 a' b' : ℝ
γ : ℝ → M
h : a' ≤ a
h' : b ≤ b'
⊢ pathELength I γ a b ≤ pathELength I γ a' b'

Tactic:
simpa [pathELength_eq_lintegral_mfderiv_Icc] using lintegral_mono_set (Icc_subset_Icc h h')

Premises used: Set.Icc_subset_Icc, Manifold.pathELength_eq_lintegral_mfderiv_Icc, MeasureTheory.lintegral_mono_set
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
symm : pathELength I γ a c = pathELength I γ a b + pathELength I γ b c
⊢ pathELength I γ a b + pathELength I γ b c = pathELength I γ a c

Tactic:
symm
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
rw₁ : Disjoint (Icc a b) (Ioc b c)
⊢ pathELength I γ a c = pathELength I γ a b + pathELength I γ b c

Tactic:
rw [pathELength, this, lintegral_union measurableSet_Ioc]

Premises used: MeasureTheory.lintegral_union, Manifold.pathELength, measurableSet_Ioc
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ Disjoint (Icc a b) (Ioc b c)

Tactic:
disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)

Premises used: Iff.mpr, And.right, And.left, Set.disjoint_iff_forall_ne, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ Disjoint (Icc a b) (Ioc b c)

Tactic:
exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ (∫⁻ (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:
simp [restrict_Ioc_eq_restrict_Icc, pathELength]

Premises used: Manifold.pathELength, MeasureTheory.restrict_Ioc_eq_restrict_Icc
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
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 ⋯) 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 : (↑(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

Tactic:
rw [pathELength_eq_lintegral_mfderivWithin_Icc]

Premises used: Manifold.pathELength_eq_lintegral_mfderivWithin_Icc
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
simp_rw :
  ∫⁻ (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))
⊢ ∫⁻ (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))

Tactic:
simp_rw [← mfderivWithin_comp_projIcc_one]

Premises used: mfderivWithin_comp_projIcc_one
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
rw :
  ∫⁻ (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 : ℝ))) =
    ∫⁻ (a_1 : { x : ℝ // x ∈ Icc a b }),
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
              (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
⊢ ∫⁻ (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))

Tactic:
rw [← MeasurePreserving.lintegral_comp_emb this
    (MeasurableEmbedding.subtype_coe measurableSet_Icc)]

Premises used: MeasureTheory.MeasurePreserving.lintegral_comp_emb, measurableSet_Icc, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
e_f :
  Eq (α := (↑(Icc a b) : Type) → ℝ≥0∞)
    (fun (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 : ℝ))))
    fun (a_1 : { x : ℝ // x ∈ Icc a b }) ↦
    enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
            (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
⊢ ∫⁻ (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 : ℝ))) =
    ∫⁻ (a_1 : { x : ℝ // x ∈ Icc a b }),
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
              (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
e_f :
  ∀ (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 : ℝ))) =
      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 : ℝ)))
⊢ Eq (α := (↑(Icc a b) : Type) → ℝ≥0∞)
    (fun (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 : ℝ))))
    fun (a_1 : { x : ℝ // x ∈ Icc a b }) ↦
    enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
            (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))

Tactic:
ext t
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
t : (↑(Icc a b) : Type)
⊢ t = projIcc a b ⋯ (↑t : ℝ)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
t : (↑(Icc a b) : Type)
⊢ t = projIcc a b ⋯ (↑t : ℝ)

Tactic:
have : t = projIcc a b h.out.le (t : ℝ) := by simp
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
this_1 :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
t : (↑(Icc a b) : Type)
this : t = projIcc a b ⋯ (↑t : ℝ)
⊢ 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 : ℝ))) =
    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 : ℝ)))

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
inl :
  ∀ (h : a ≤ a) (hf : MonotoneOn f (Icc a a)) (h'f : DifferentiableOn ℝ f (Icc a a)) (hγ : MDiff[Icc (f a) (f a)] γ),
    pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)
inr : ∀ (h : a < b), pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

Tactic:
rcases h.eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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 : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ a
hf : MonotoneOn f (Icc a a)
h'f : DifferentiableOn ℝ f (Icc a a)
hγ : MDiff[Icc (f a) (f a)] γ
⊢ pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
⊢ f '' Icc a b = Icc (f a) (f b)

Tactic:
have f_im : f '' (Icc a b) = Icc (f a) (f b) := h'f.continuousOn.image_Icc_of_monotoneOn h.le hf
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
inr :
  ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (t : ℝ) in f '' Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

Tactic:
simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]

Premises used: Manifold.pathELength_eq_lintegral_mfderivWithin_Icc
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
⊢ ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t

Tactic:
have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
inr :
  ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (x : ℝ) in Icc a b,
      ENNReal.ofReal (derivWithin f (Icc a b) x) *
        enorm (E := TangentSpace I (γ (f x)))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f x) :
                (a : TangentSpace 𝓘(ℝ, ℝ) (f x)) → TangentSpace I (γ (f x)))
              1 :
            TangentSpace I (γ (f x)))
⊢ ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (t : ℝ) in f '' Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))

Tactic:
rw [lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc B hf]

Premises used: MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, measurableSet_Icc