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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x
have hf : ContinuousWithinAt b s x
Tactic: have hf : ContinuousWithinAt b s x := by
    simp only [FiberBundle.continuousWithinAt_totalSpace] at hv
    exact hv.1
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
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
hf : ContinuousWithinAt b s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x
have simp : ContinuousWithinAt (Y := ℝ)
  (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s x
Tactic: simp only [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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
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
hf : ContinuousWithinAt b s x
⊢ ContinuousWithinAt (Y := ℝ)
    (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s
    x
have this : ContinuousWithinAt.{u_4, u_1} (Y := TotalSpace ℝ (Trivial B ℝ))
  (fun (m : M) ↦
    TotalSpace.mk' (E := Trivial B ℝ) ℝ (b m)
      ((((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)))
  s x
Tactic: have : ContinuousWithinAt
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x :=
    (g_cont.continuousAt.comp_continuousWithinAt hf).clm_bundle_apply₂ (F₁ := F) (F₂ := F) hv hw
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
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
hf : ContinuousWithinAt b s x
this :
  ContinuousWithinAt.{u_4, u_1} (Y := TotalSpace ℝ (Trivial B ℝ))
    (fun (m : M) ↦
      TotalSpace.mk' (E := Trivial B ℝ) ℝ (b m)
        ((((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)))
    s x
⊢ ContinuousWithinAt (Y := ℝ)
    (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s
    x
have this₁ : ContinuousWithinAt.{u_4, u_1} (Y := B) (fun (x : M) ↦ b x) s x ∧
  ContinuousWithinAt (Y := ℝ)
    (fun (x_1 : M) ↦
      ((↑(trivializationAt ℝ (Trivial B ℝ) (b x)) : TotalSpace ℝ (Trivial B ℝ) → B × ℝ)
          (TotalSpace.mk' (E := Trivial B ℝ) ℝ (b x_1)
            ((((g (b x_1) : (a : E (b x_1)) → E (b x_1) →L[ℝ] ℝ) (v x_1) : E (b x_1) →L[ℝ] ℝ) : (a : E (b x_1)) → ℝ)
              (w x_1)))).2)
    s x
Tactic: simp only [FiberBundle.continuousWithinAt_totalSpace] at this
Cleared hypotheses: this
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
x : M
hv : ContinuousAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) x
hw : ContinuousAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) x
⊢ ContinuousAt (Y := ℝ) (fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) x
have simp : ∀ (hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) Set.univ x)
  (hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) Set.univ x),
  ContinuousWithinAt (Y := ℝ) (fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) Set.univ x
Tactic: simp only [← continuousWithinAt_univ] at hv hw ⊢
Cleared hypotheses: hv, hw
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
hv : Continuous[inst_8, inst_3] fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)
hw : Continuous[inst_8, inst_3] fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)
⊢ Continuous[inst_8, _] fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫
have simp : ∀ (hv : ∀ (x : M), ContinuousAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) x)
  (hw : ∀ (x : M), ContinuousAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) x) (x : M),
  ContinuousAt (Y := ℝ) (fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) x
Tactic: simp only [continuous_iff_continuousAt] at hv hw ⊢
Cleared hypotheses: hv, hw
-- 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
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      r
have obtain : ∀ (r' : ℝ) (hr' : 1 < r') (r'r : r' < r),
  ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      r
Tactic: obtain ⟨r', hr', r'r⟩ : ∃ r', 1 < r' ∧ r' < r := exists_between hr
-- 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 y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      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 < δ ∧ (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
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 < δ ∧ (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
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.sub (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, (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
have a : (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - 0 * C
Tactic: apply (tendsto_order.1 B).1
-- 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))
⊢ 1 < HPow.hPow (β := ℕ) r' 2
have nlinarith : HPow.hPow (β := ℕ) r' 2 ≤ 1 → 2 * (1 - r') + (HPow.hPow (β := ℕ) r' 2 - 1) + (0 - (1 - r') * (1 - r')) = 0
Tactic: nlinarith
-- 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))
nlinarith : HPow.hPow (β := ℕ) r' 2 ≤ 1 → 2 * (1 - r') + (HPow.hPow (β := ℕ) r' 2 - 1) + (0 - (1 - r') * (1 - r')) = 0
⊢ 1 < HPow.hPow (β := ℕ) r' 2
have nlinarith₁ : HPow.hPow (β := ℕ) r' 2 ≤ 1 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- 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 < δ ∧ (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
have B' : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
Tactic: have B' : ∀ᶠ δ in 𝓝[>] 0, (r' ^ 2)⁻¹ < 1 - δ * C := by
      apply (tendsto_order.1 B).1
      simpa using inv_lt_one_of_one_lt₀ (by nlinarith)
-- 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 y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      r
have obtain : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C),
  ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      r
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ (r' ^ 2)⁻¹ < 1 - δ * C := 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.sub (tendsto_id.mul tendsto_const_nhds)
    have B' : ∀ᶠ δ in 𝓝[>] 0, (r' ^ 2)⁻¹ < 1 - δ * C := by
      apply (tendsto_order.1 B).1
      simpa using inv_lt_one_of_one_lt₀ (by nlinarith)
    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δ : (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := E y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      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 y →L[ℝ] E x)
        (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) x)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
          E y →L[ℝ] E x) <
      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δ : (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
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)