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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
linarith : r' < 0 → -1 + (1 - r') + (r' - 0) = 0
⊢ 0 ≤ r'

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
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
apply :
  ∀ (v : E x),
    norm (E := 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) :
              (a : E x) → E y)
            v :
          E y) ≤
      r' * ‖v‖
⊢ 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:
apply (opNorm_le_bound _ (by linarith) (fun v ↦ ?_)).trans_lt r'r

Premises used: ContinuousLinearMap.opNorm_le_bound, LE.le.trans_lt
-- 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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this_2 : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
this :
  HPow.hPow (β := ℕ)
      (norm.{u_3} (E := E y)
        (((Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y)) :
              (a : F) → E y)
            w :
          E y))
      2 ≤
    HPow.hPow (β := ℕ) r' 2 * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ HPow.hPow (β := ℕ)
      (norm (E := 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) :
              (a : E x) → E y)
            v :
          E y))
      2 ≤
    HPow.hPow (β := ℕ) (r' * ‖v‖) 2

Tactic:
simpa [mul_pow]

Premises used: mul_pow
-- 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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this_2 : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
this :
  HPow.hPow (β := ℕ)
      (norm.{u_3} (E := E y)
        (((Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y)) :
              (a : F) → E y)
            w :
          E y))
      2 ≤
    HPow.hPow (β := ℕ) r' 2 * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 ≤ r' * ‖v‖

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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
suffices :
  HPow.hPow (β := ℕ)
      (norm.{u_3} (E := E y)
        (((Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y)) :
              (a : F) → E y)
            w :
          E y))
      2 ≤
    HPow.hPow (β := ℕ) r' 2 * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ norm (E := 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) :
            (a : E x) → E y)
          v :
        E y) ≤
    r' * ‖v‖

Tactic:
suffices ‖((trivializationAt F E x).symmL ℝ y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2 from
    le_of_sq_le_sq (by simpa [mul_pow]) (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
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
simp :
  (((g y : (a : E y) → E y →L[ℝ] ℝ) (Trivialization.symm (E := E) (trivializationAt F E x) y w) : E y →L[ℝ] ℝ) :
        (a : E y) → ℝ)
      (Trivialization.symm (E := E) (trivializationAt F E x) y w) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2)
      ((((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) v : ℝ)
⊢ HPow.hPow (β := ℕ)
      (norm.{u_3} (E := E y)
        (((Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y)) :
              (a : F) → E y)
            w :
          E y))
      2 ≤
    HPow.hPow (β := ℕ) r' 2 * HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
simp only [Trivialization.symmL_apply, ← real_inner_self_eq_norm_sq, hg]

Premises used: real_inner_self_eq_norm_sq, Bundle.Trivialization.symmL_apply
-- 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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
rw :
  Eq (α := ℝ) ((((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) v : ℝ)
    (((Trivialization.linearMapAt ℝ (E := fun (x : B) ↦ ℝ) (trivializationAt ℝ (fun (x : B) ↦ ℝ) x) x : ℝ →ₗ[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        ((((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) :
          ℝ) :
      ℝ)
⊢ Eq (α := ℝ) ((((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) v : ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]

Premises used: inCoordinates_apply_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 : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
⊢ ((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)
      (((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)
        v) =
    v

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

Premises used: Real, FiberBundle.trivializationAt, Bundle.Trivialization.continuousLinearEquivAt, ContinuousLinearEquiv.symm_apply_apply
-- 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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
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.symm (E := E) (trivializationAt F E x) x
      (((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)
        v) =
    v

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

Premises used: Real, FiberBundle.trivializationAt, Bundle.Trivialization.continuousLinearEquivAt, ContinuousLinearEquiv.symm_apply_apply
-- 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'δ : 1 + δ * C < HPow.hPow (β := ℕ) r' 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun (y : B) ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun (x : B) ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this_1 : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ Trivialization.baseSet (trivializationAt F E x)
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F :=
  ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    v
⊢ 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