awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
Tactic: have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
⊢ ∃ (δ : ℝ), 0 < δ ∧ 1 + δ * C < HPow.hPow (β := ℕ) r' 2
have A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
Tactic: have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
⊢ Tendsto (fun (δ : ℝ) ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
have h₁ : Tendsto (fun (δ : ℝ) ↦ 1 + δ * C) (𝓝 0) (𝓝 (1 + 0 * C))
Tactic: apply tendsto_inf_left
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ 1 + δ * C < HPow.hPow (β := ℕ) r' 2
have B₁ : Tendsto (fun (δ : ℝ) ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
Tactic: have B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C)) := by
      apply tendsto_inf_left
      exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B_1) → NormedAddCommGroup (E x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B_1
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun (δ : ℝ) ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 1 + δ * C < HPow.hPow (β := ℕ) r' 2
have a : HPow.hPow (β := ℕ) r' 2 > 1 + 0 * C
Tactic: apply (tendsto_order.1 B).2
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B_1) → NormedAddCommGroup (E x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B_1
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun (δ : ℝ) ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
⊢ ∃ (δ : ℝ), 0 < δ ∧ 1 + δ * C < HPow.hPow (β := ℕ) r' 2
have B' : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 1 + δ * C < HPow.hPow (β := ℕ) r' 2
Tactic: have B' : ∀ᶠ δ in 𝓝[>] 0, 1 + δ * C < r' ^ 2 := by
      apply (tendsto_order.1 B).2
      simpa using hr'.trans_le (le_abs_self _)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have obtain : ∀ (δ : ℝ) (δpos : 0 < δ) (h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2),
  ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
Tactic: obtain ⟨δ, δpos, h'δ⟩ : ∃ δ, 0 < δ ∧ (1 + δ * C) < r' ^ 2 := by
    have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
    have B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C)) := by
      apply tendsto_inf_left
      exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
    have B' : ∀ᶠ δ in 𝓝[>] 0, 1 + δ * C < r' ^ 2 := by
      apply (tendsto_order.1 B).2
      simpa using hr'.trans_le (le_abs_self _)
    exact (A.and B').exists
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have rcases : ∀ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ)
  (g_cont :
    Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x))
  (hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w),
  ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
Tactic: rcases h.exists_continuous with ⟨g, g_cont, hg⟩
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
⊢ ContinuousAt g' x
have W : ContinuousAt (Y := TotalSpace.{u_1, u_2, u_3} (F →L[ℝ] F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ)
  (fun (x : B) ↦ TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)) x
Tactic: have W := g_cont.continuousAt (x := x)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
W :
  ContinuousAt (Y := TotalSpace.{u_1, u_2, u_3} (F →L[ℝ] F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ)
    (fun (x : B) ↦ TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)) x
⊢ ContinuousAt g' x
have W₁ : ContinuousAt (Y := B) (fun (x : B) ↦ x) x ∧
  ContinuousAt.{u_1, u_2} (Y := F →L[ℝ] F →L[ℝ] ℝ)
    (fun (x_1 : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x x_1 x x_1 (g x_1)) x
Tactic: simp only [continuousAt_hom_bundle] at W
Cleared hypotheses: W
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have hg' : ContinuousAt g' x
Tactic: have hg' : ContinuousAt g' x := by
    have W := g_cont.continuousAt (x := x)
    simp only [continuousAt_hom_bundle] at W
    exact W.2
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have this : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
Tactic: have : ∀ᶠ y in 𝓝 x, dist (g' y) (g' x) < δ := by
    rw [Metric.continuousAt_iff'] at hg'
    apply hg' _ δpos
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) <
      r
have h₁ : ∀ (y : B) (hy : dist (g' y) (g' x) < δ) (h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)),
  norm (E := E x →L[ℝ] E y)
      (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
        E x →L[ℝ] E y) <
    r
Tactic: filter_upwards [this, (trivializationAt F E x).open_baseSet.mem_nhds h'x] with y hy h'y
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ norm (E := E x →L[ℝ] E y)
      (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
        E x →L[ℝ] E y) <
    r
have this₁ : ‖g' y - g' x‖ ≤ δ
Tactic: have : ‖g' y - g' x‖ ≤ δ := by rw [← dist_eq_norm]; exact hy.le
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
⊢ 0 ≤ r'
have linarith : r' < 0 → -1 + (1 - r') + (r' - 0) = 0
Tactic: linarith