awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)
have refine_2 : ∀ (x : M), f x / (f x + g x) ≤ 1
Tactic: refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x / (f x + g x) ≤ 1
have apply : f x ≤ f x + g x
Tactic: apply div_le_one_of_le₀ _ (A x).le
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ (support (M := ℝ) fun (x : M) ↦ f x / (f x + g x)) = s
have B : Eq.{uM + 1} (α := Set M) (support (M := ℝ) fun (x : M) ↦ f x + g x) univ
Tactic: have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
⊢ ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have rcases : ∀ (f : M → ℝ) (f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f) (f_range : range f ⊆ Icc 0 1) (fs : support f = sᶜ)
  (ft : ∀ (x : M), x ∈ t ↔ f x = 1),
  ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
Tactic: rcases exists_contMDiff_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with
    ⟨f, f_diff, f_range, fs, ft⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ (f : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have refine : ∀ (x : M), x ∈ s ↔ f x = 0
Tactic: refine ⟨f, f_diff, f_range, ?_, ft⟩
-- 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 : F
⊢ IsVonNBounded.{0, u_4} ℝ (E := TangentSpace 𝓘(ℝ, F) x)
    {v : TangentSpace 𝓘(ℝ, F) x |
      LT.lt (α := ℝ)
        ((((innerSL ℝ : (a : TangentSpace 𝓘(ℝ, F) x) → TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) v :
                TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) :
              (a : TangentSpace 𝓘(ℝ, F) x) → ℝ)
            v :
          ℝ)
        (1 : ℝ)}
have change : IsVonNBounded.{0, u_4} ℝ (E := F) {v : F | ⟪v, v⟫ < 1}
Tactic: change IsVonNBounded ℝ {v : F | ⟪v, v⟫ < 1}
-- 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 : F
⊢ Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
have h : ∀ (v : F), Membership.mem (γ := Set F) (Metric.ball 0 1) v ↔ Membership.mem (γ := Set F) {v : F | ⟪v, v⟫ < 1} v
Tactic: ext v
-- 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 v : F
⊢ Membership.mem (γ := Set F) (Metric.ball 0 1) v ↔ Membership.mem (γ := Set F) {v : F | ⟪v, v⟫ < 1} v
have h : √⟪v, v⟫ < 1 ↔ ⟪v, v⟫ < 1
Tactic: simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ),
        RCLike.re_to_real, Set.mem_setOf_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 v : F
| √⟪v, v⟫ < 1
have rw : √⟪v, v⟫ < √1
Tactic: rw [show (1 : ℝ) = √1 by simp]
-- 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 v : F
⊢ √⟪v, v⟫ < 1 ↔ ⟪v, v⟫ < 1
have h : √⟪v, v⟫ < √1 ↔ ⟪v, v⟫ < 1
Tactic: conv_lhs => rw [show (1 : ℝ) = √1 by simp]
-- 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 v : F
⊢ √⟪v, v⟫ < √1 ↔ ⟪v, v⟫ < 1
have h : 0 ≤ ⟪v, v⟫
Tactic: rw [Real.sqrt_lt_sqrt_iff]
-- 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 : F
⊢ IsVonNBounded.{0, u_4} ℝ (E := F) {v : F | ⟪v, v⟫ < 1}
have this : Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
Tactic: have : Metric.ball (0 : F) 1 = {v : F | ⟪v, v⟫ < 1} := by
      ext v
      simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ),
        RCLike.re_to_real, Set.mem_setOf_eq]
      conv_lhs => rw [show (1 : ℝ) = √1 by simp]
      rw [Real.sqrt_lt_sqrt_iff]
      exact real_inner_self_nonneg
-- 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 : F
this : Eq.{u_4 + 1} (α := Set F) (Metric.ball 0 1) {v : F | ⟪v, v⟫ < 1}
⊢ IsVonNBounded.{0, u_4} ℝ (E := F) {v : F | ⟪v, v⟫ < 1}
have rw : IsVonNBounded.{0, u_4} ℝ (E := F) (Metric.ball 0 1)
Tactic: rw [← 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
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 : F
⊢ ContMDiffAt 𝓘(ℝ, F) (E' := F × (F →L[ℝ] F →L[ℝ] ℝ)) (ModelWithCorners.prod 𝓘(ℝ, F) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (b : F) ↦ TangentSpace 𝓘(ℝ, F) b →L[ℝ] TangentSpace 𝓘(ℝ, F) b →L[ℝ] ℝ) ω
    (fun (b : F) ↦ ⟨b, innerSL ℝ⟩) x
have rw : ContMDiffAt 𝓘(ℝ, F) (E' := F →L[ℝ] F →L[ℝ] ℝ) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ) (M' := F →L[ℝ] F →L[ℝ] ℝ) ω
  (fun (x_1 : F) ↦
    ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ) (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ)
              x) :
          (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
            F × (F →L[ℝ] F →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2)
  x
Tactic: rw [contMDiffAt_section]
-- 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 : F
⊢ ContMDiffAt 𝓘(ℝ, F) (E' := F →L[ℝ] F →L[ℝ] ℝ) 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ) (M' := F →L[ℝ] F →L[ℝ] ℝ) ω
    (fun (x_1 : F) ↦
      ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
            (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
              F × (F →L[ℝ] F →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2)
    x
have h : ∀ (x_1 : F),
  Eq (α := F →L[ℝ] F →L[ℝ] ℝ)
    ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ) (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ)
              x) :
          (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
            F × (F →L[ℝ] F →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2
    (innerSL ℝ)
Tactic: convert! contMDiffAt_const (c := innerSL ℝ)
-- 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 x_1 : F
⊢ Eq (α := F →L[ℝ] F →L[ℝ] ℝ)
    ((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ) (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ)
              x) :
          (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
            F × (F →L[ℝ] F →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2
    (innerSL ℝ)
have h : ∀ (v w : F),
  Eq (α := ℝ)
    ((((((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                          (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
                      (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦
                          TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
                        F × (F →L[ℝ] F →L[ℝ] ℝ))
                    ⟨x_1, innerSL ℝ⟩).2 :
                (a : F) → F →L[ℝ] ℝ)
              v :
            F →L[ℝ] ℝ) :
          (a : F) → ℝ)
        w :
      ℝ)
    ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) v : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ ‖v‖ = ‖v‖
have rw : √⟪v, v⟫ = ‖v‖
Tactic: rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
rw : √⟪v, v⟫ = ‖v‖
⊢ ‖v‖ = ‖v‖
have rw₁ : √⟪v, v⟫ = √⟪v, v⟫
Tactic: rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    edist x y
have this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
Tactic: have : edist x y = ∫⁻ t in Icc (0 : ℝ) 1, ‖y - x‖ₑ := by
    simp [edist_comm x y, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    edist x y
have rw : ∫⁻ (t : ℝ) in Icc 0 1,
    enorm (E := E)
      ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
  ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
have apply : ∀ (z : ℝ) (hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z),
  enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    ‖y - x‖ₑ
Tactic: apply setLIntegral_congr_fun measurableSet_Icc (fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
⊢ enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    ‖y - x‖ₑ
have rw : enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
  enorm (E := E) ((fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z : (a : ℝ) → E) 1 : E)
Tactic: rw [show y - x = fderiv ℝ (ContinuousAffineMap.lineMap (R := ℝ) x y) z 1 by simp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
⊢ enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    enorm (E := E) ((fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z : (a : ℝ) → E) 1 : E)
have e_a : Eq (α := ℝ →L[ℝ] E) (fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z)
  (fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z)
Tactic: congr
-- 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
⊢ IsRiemannianManifold 𝓘(ℝ, F) F
have refine_1 : ∀ (x y : F), edist x y ≤ riemannianEDist 𝓘(ℝ, F) x y
Tactic: refine ⟨fun x y ↦ le_antisymm ?_ ?_⟩
-- 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
refine_1 : ∀ (x y : F), edist x y ≤ riemannianEDist 𝓘(ℝ, F) x y
⊢ IsRiemannianManifold 𝓘(ℝ, F) F
have refine_2 : ∀ (x y : F), riemannianEDist 𝓘(ℝ, F) x y ≤ edist x y
Tactic: refine ⟨fun x y ↦ le_antisymm ?_ ?_⟩
-- 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
⊢ edist x y ≤ riemannianEDist 𝓘(ℝ, F) x y
have refine_1 : ∀ (i : Path x y)
  (i_1 :
    ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
      (M' := F) 1 (⇑i : (a : (↑unitInterval : Type)) → F)),
  edist x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((i : (a : (↑unitInterval : Type)) → F) x_1 : F))
        ((mfderiv% (⇑i : (a : (↑unitInterval : Type)) → F) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace 𝓘(ℝ, F) ((i : (a : (↑unitInterval : Type)) → F) x_1))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((i : (a : (↑unitInterval : Type)) → F) x_1 : F))
Tactic: simp only [riemannianEDist, le_iInf_iff]
-- 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
γ : 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 ⋯)
⊢ edist x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))
        ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → F) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace 𝓘(ℝ, F) ((γ : (a : (↑unitInterval : Type)) → F) x_1))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))
have D : ContDiffOn ℝ 1 e (Icc 0 1)
Tactic: have D : ContDiffOn ℝ 1 e (Icc 0 1) :=
      contMDiffOn_iff_contDiffOn.mp (hγ.comp_contMDiffOn contMDiffOn_projIcc)
-- 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 ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))
        ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → F) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace 𝓘(ℝ, F) ((γ : (a : (↑unitInterval : Type)) → F) x_1))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))
have refine_1 : edist x y ≤
  ∫⁻ (t : ℝ) in Icc 0 1,
    enorm (E :=
      TangentSpace 𝓘(ℝ, F) (M := F)
        (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 sorry) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F)
              (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: rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc,
      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
γ : 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
have rw : ‖e 1 - e 0‖ₑ
Tactic: rw [edist_comm, edist_eq_enorm_sub, show x = e 0 by simp [e], show y = e 1 by simp [e]]