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
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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
grw :
  HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2) ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2) ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
grw [this]
-- 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
δ : ℝ
δ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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
ha : LE.le (α := ℝ) (0 : ℝ) ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hbc : (1 - δ * C)⁻¹ ≤ HPow.hPow (β := ℕ) r' 2
⊢ HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2) ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
gcongr
-- 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
δ : ℝ
δ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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
ha : 0 ≤ HPow.hPow (β := ℕ) ‖v‖ 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
rw [← hgy, ← hg, real_inner_self_eq_norm_sq]

Premises used: real_inner_self_eq_norm_sq
-- 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
δ : ℝ
δ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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
positivity
-- 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
δ : ℝ
δ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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ 0 < HPow.hPow (β := ℕ) r' 2

Tactic:
positivity
-- 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
δ : ℝ
δ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)
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_2 : ‖g' x - g' y‖ ≤ δ
v : E y
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) :
      (a : E y) → F)
    v
hgy :
  Eq (α := ℝ) ((((g y : (a : E y) → E y →L[ℝ] ℝ) v : E y →L[ℝ] ℝ) : (a : E y) → ℝ) v : ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
hgx :
  Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) x w) : E x →L[ℝ] ℝ) :
          (a : E x) → ℝ)
        (Trivialization.symm (E := E) (trivializationAt F E x) x w) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this_3 :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HAdd.hAdd (β := ℝ) (HMul.hMul (β := ℝ) (δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
      ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
this :
  (((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
    HMul.hMul (β := ℝ) (1 - δ * C)⁻¹ ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ (1 - δ * C)⁻¹ ≤ HPow.hPow (β := ℕ) r' 2

Tactic:
exact inv_le_of_inv_le₀ (by positivity) hδ.le

Premises used: LT.lt.le, inv_le_of_inv_le₀
-- 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
⊢ (1 +
        norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
            ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)) *
      2 >
    0

Tactic:
positivity
-- 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
refine :
  ∀ᶠ (y : B) in 𝓝 x,
    norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
          ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) <
      (1 +
          norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
              ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)) *
        2
⊢ ∃ C > 0,
    ∀ᶠ (y : B) in 𝓝 x,
      norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
            ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) <
        C

Tactic:
refine ⟨(1 + ‖(trivializationAt F E x).continuousLinearMapAt ℝ  x‖) * 2, by positivity, ?_⟩
-- 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
h₁ :
  ∀ (y : B)
    (hy :
      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) <
        2),
    norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
          ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) <
      (1 +
          norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
              ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)) *
        2
⊢ ∀ᶠ (y : B) in 𝓝 x,
    norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y :
          ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F) <
      (1 +
          norm (E := ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
              ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F)) *
        2

Tactic:
filter_upwards [eventually_norm_symmL_trivializationAt_self_comp_lt F E x one_lt_two] with y hy

Premises used: eventually_norm_symmL_trivializationAt_self_comp_lt, one_lt_two
-- 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 y : B
hy :
  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) <
    2
h₁ :
  ∀ (v : F),
    Eq (α := F)
      (((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
                ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) ∘SL
              (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) :
            (a : F) → F)
          v :
        F)
      ((ContinuousLinearMap.id ℝ F : (a : F) → F) v : F)
⊢ Eq (α := F →L[ℝ] F)
    ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) ∘SL
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))
    (ContinuousLinearMap.id ℝ F)

Tactic:
ext v
-- 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 y : B
hy :
  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) <
    2
v : F
⊢ x ∈ Trivialization.baseSet (trivializationAt F E x)

Tactic:
have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x