awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ edist x y ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))
have refine_1 : ‖e 1 - e 0‖ₑ ≤
  ∫⁻ (t : ℝ) in Icc 0 1,
    enorm (E := F)
      ((fderivWithin ℝ
              (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 sorry))
              (Icc 0 1) t :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) →
              TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 sorry) t))
          1 :
        TangentSpace 𝓘(ℝ, F) (M := F)
          (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 sorry) t))
Tactic: conv_lhs =>
      rw [edist_comm, edist_eq_enorm_sub, show x = e 0 by simp [e], show y = e 1 by simp [e]]
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
have apply : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, F) (M' := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)
Tactic: apply riemannianEDist_le_pathELength ?_ (by simp [γ, ContinuousAffineMap.coe_lineMap_eq])
        (by simp [γ, ContinuousAffineMap.coe_lineMap_eq]) zero_le_one
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, F) (M' := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)
have rw : ContDiffOn ℝ (E := ℝ) (F := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)
Tactic: rw [contMDiffOn_iff_contDiffOn]
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ edist x y
have this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
Tactic: have : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) γ 0 1 := by
      apply riemannianEDist_le_pathELength ?_ (by simp [γ, ContinuousAffineMap.coe_lineMap_eq])
        (by simp [γ, ContinuousAffineMap.coe_lineMap_eq]) zero_le_one
      rw [contMDiffOn_iff_contDiffOn]
      exact γ.contDiff.contDiffOn
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ edist x y
have refine_2 : pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1 = edist x y
Tactic: apply this.trans_eq
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
⊢ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1 = edist x y
have refine_2 : ∫⁻ (t : ℝ) in Icc 0 1,
    enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F))
      ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F) (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
          1 :
        TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
  edist x y
Tactic: rw [pathELength_eq_lintegral_mfderivWithin_Icc]
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F) (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y
have refine_2 : ∫⁻ (t : ℝ) in Icc 0 1,
    enorm (E := F)
      ((fderivWithin ℝ (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
          1 :
        TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
  edist x y
Tactic: simp only [mfderivWithin_eq_fderivWithin, enorm_tangentSpace_vectorSpace]
-- 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
x : M
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        C
have rcases : ∀ (C : ℝ) (C_pos : C > 0)
  (hC :
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] E)
          (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
            (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
        C),
  ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        C
Tactic: rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
    with ⟨C, C_pos, hC⟩
-- 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        C
have refine : ∀ᶠ (y : M) in 𝓝 x,
  norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y) <
    C
Tactic: refine ⟨C, C_pos, ?_⟩
-- 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
have hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
Tactic: have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
⊢ ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
have h : ∀ (y : M)
  (hy :
    norm (E := TangentSpace I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C)
  (h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source),
  norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y) <
    C
Tactic: filter_upwards [hC, hx] with y hy h'y
-- 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
x : M
⊢ ∃ C > 0,
    ∀ᶠ (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∞)
have rcases : ∀ (C : ℝ) (C_pos : C > 0)
  (hC :
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        C),
  ∃ C > 0,
    ∀ᶠ (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∞)
Tactic: rcases eventually_norm_mfderiv_extChartAt_lt I x with ⟨C, C_pos, hC⟩
-- 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
⊢ ∃ C > 0,
    ∀ᶠ (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∞)
have lift : ∀ (C : ℝ≥0) (C_pos : (↑C : ℝ) > 0)
  (hC :
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ)),
  ∃ C > 0,
    ∀ᶠ (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∞)
Tactic: lift C to ℝ≥0 using C_pos.le
Cleared hypotheses: C, C_pos, hC
-- 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
x : M
C : ℝ≥0
C_pos : (↑C : ℝ) > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
⊢ ∃ C > 0,
    ∀ᶠ (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∞)
have C_pos₁ : 0 < C
Tactic: simp only [gt_iff_lt, NNReal.coe_pos] at C_pos
Cleared hypotheses: C_pos
-- 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
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
⊢ ∃ C > 0,
    ∀ᶠ (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∞)
have refine : ∀ᶠ (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∞)
Tactic: refine ⟨C, C_pos, ?_⟩
-- 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
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
⊢ ∀ᶠ (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∞)
have h : ∀ (y : M)
  (hy :
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)),
  enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y) <
    (↑C : ℝ≥0∞)
Tactic: filter_upwards [hC] with y hy
-- 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
x : M
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E :=
          TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
            TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) y)) <
        C
have rcases : ∀ (C : ℝ) (C_pos : C > 0)
  (hC :
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := E →L[ℝ] TangentSpace I y)
          (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
            (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
        C),
  ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E :=
          TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
            TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) y)) <
        C
Tactic: rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
    with ⟨C, C_pos, hC⟩
-- 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E :=
          TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
            TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) y)) <
        C
have refine : ∀ᶠ (y : M) in 𝓝 x,
  norm (E :=
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y)) <
    C
Tactic: refine ⟨C, C_pos, ?_⟩
-- 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ ∀ᶠ (y : M) in 𝓝 x,
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
have hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
Tactic: have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds 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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
⊢ ∀ᶠ (y : M) in 𝓝 x,
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
have h : ∀ (y : M)
  (hy :
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C)
  (h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source),
  norm (E :=
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y)) <
    C
Tactic: filter_upwards [hC, hx] with y hy h'y