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 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
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
h₁ :
  ((Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
          LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
        (a : E x) → F)
      (Trivialization.symm (E := E) (trivializationAt F E x) x v) =
    v
⊢ 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)

Tactic:
simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      Function.comp_apply, coe_id', id_eq]

Premises used: ContinuousLinearMap.coe_comp', Bundle.Trivialization.continuousLinearMapAt_apply, Bundle.Trivialization.symmL_apply, ContinuousLinearMap.coe_id', Function.comp_apply, id_eq
-- 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
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ ((Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x :
          ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
        (a : E x) → F)
      (((ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x) :
              ContinuousLinearEquiv.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) :
            (a : F) → E x)
          v :
        E x) =
    v

Tactic:
((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v

Premises used: Real, ContinuousLinearEquiv.apply_symm_apply, FiberBundle.trivializationAt, Bundle.Trivialization.continuousLinearEquivAt
-- 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
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
h₁ :
  Eq (α := (a : E x) → F)
    (⇑(Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
          LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    (⇑(Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x :
          ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
⊢ ((Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
          LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
        (a : E x) → F)
      (Trivialization.symm (E := E) (trivializationAt F E x) x v) =
    v

Tactic:
convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v

Premises used: Real, ContinuousLinearEquiv.apply_symm_apply, FiberBundle.trivializationAt, Bundle.Trivialization.continuousLinearEquivAt
-- 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
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ Eq (α := (a : E x) → F)
    (⇑(Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
          LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    (⇑(Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x :
          ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)

Tactic:
simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]

Premises used: Bundle.Trivialization.coe_continuousLinearEquivAt_eq
-- 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
⊢ 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:
have A : ((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L
      ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
    ext v
    have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
    simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      Function.comp_apply, coe_id', id_eq]
    convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'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 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
A :
  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)
⊢ Eq (α := 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)
    (comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.id ℝ F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
      ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)

Tactic:
simp
-- 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
A :
  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)
⊢ Eq (α := 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)
    (comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.id ℝ F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
      ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)

Tactic:
have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
    (ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) := by simp
-- 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
A :
  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)
this :
  Eq (α := 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)
    (comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.id ℝ F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
      ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
h₁ :
  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) *
      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) <
    (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
⊢ 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:
grw [this, ← A, comp_assoc, opNorm_comp_le]

Premises used: ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.comp_assoc
-- 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
A :
  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)
this :
  Eq (α := 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)
    (comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.id ℝ F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
      ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
h₁ :
  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) <
    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)
⊢ 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) *
      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) <
    (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:
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 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
A :
  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)
this :
  Eq (α := 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)
    (comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.id ℝ F)
        (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) y) :
      ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E y) F)
linarith :
  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) ≤
      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) →
    -1 +
        (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) -
          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)) =
      0
⊢ 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) <
    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)

Tactic:
linarith
-- 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 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
⊢ ∀ᶠ (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 ⟨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
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.add (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add
-- 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.add (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add