awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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.{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

Premises used: FiberBundle.continuousWithinAt_totalSpace
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 := 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
⊢ 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:
this.2

Premises used: And.right
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 := 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
⊢ 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:
exact this.2

Premises used: And.right
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
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
⊢ ContinuousAt (Y := ℝ) (fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) x

Tactic:
simp only [← continuousWithinAt_univ] at hv hw ⊢

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 : 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:
ContinuousWithinAt.inner_bundle hv hw

Premises used: ContinuousWithinAt.inner_bundle
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 : 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:
exact ContinuousWithinAt.inner_bundle hv hw

Premises used: ContinuousWithinAt.inner_bundle
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
hv : ContinuousOn (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s
hw : ContinuousOn (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s
⊢ ContinuousOn (Y := ℝ) (fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) s

Tactic:
fun x hx ↦ (hv x hx).inner_bundle (hw x hx)

Premises used: ContinuousOn, ContinuousWithinAt.inner_bundle
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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)
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
⊢ Continuous[inst_8, _] fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫

Tactic:
simp only [continuous_iff_continuousAt] at hv hw ⊢

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 : ∀ (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:
fun x ↦ (hv x).inner_bundle (hw x)

Premises used: ContinuousAt.inner_bundle
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 : ∀ (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:
exact fun x ↦ (hv x).inner_bundle (hw x)

Premises used: ContinuousAt.inner_bundle
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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' : ℝ), 1 < r' ∧ r' < r

Tactic:
exists_between hr

Premises used: exists_between
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
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
⊢ ∀ᶠ (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

Premises used: exists_between
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
⊢ x ∈ Trivialization.baseSet (trivializationAt F E x)

Tactic:
have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ

Tactic:
have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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 < δ
h₁ : Tendsto (fun (δ : ℝ) ↦ 1 - δ * C) (𝓝 0) (𝓝 (1 - 0 * C))
⊢ Tendsto (fun (δ : ℝ) ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C))

Tactic:
apply tendsto_inf_left

Premises used: Filter.tendsto_inf_left
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))

Tactic:
tendsto_const_nhds.sub (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.sub
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))

Tactic:
exact tendsto_const_nhds.sub (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.sub
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))

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)
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))
a : (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - 0 * C
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C

Tactic:
apply (tendsto_order.1 B).1

Premises used: tendsto_order, And.left, Iff.mp
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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
nlinarith₁ : HPow.hPow (β := ℕ) r' 2 ≤ 1 → GT.gt (α := ℝ) 2 0
⊢ 1 < HPow.hPow (β := ℕ) r' 2

Tactic:
nlinarith
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))
⊢ (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - 0 * C

Tactic:
simpa using inv_lt_one_of_one_lt₀ (by nlinarith)

Premises used: inv_lt_one_of_one_lt₀
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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

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)
-- Module: Mathlib.Topology.VectorBundle.Riemannian
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))
B' : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C
⊢ ∃ (δ : ℝ), 0 < δ ∧ (HPow.hPow (β := ℕ) r' 2)⁻¹ < 1 - δ * C

Tactic:
(A.and B').exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists