awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ (((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 : ℝ)
have rw : (((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w ≤
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: rw [hgx, hgy]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((((g' y - g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
      ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HAdd.hAdd (β := ℝ) (‖g' y - g' x‖ * ‖w‖ * ‖w‖) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have grw : HAdd.hAdd (α := ℝ) (β := ℝ) ((((g' y - g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
  HAdd.hAdd (β := ℝ) (norm (E := ℝ) ((((g' y - g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ))
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: grw [← le_opNorm₂, ← Real.le_norm_self]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HAdd.hAdd (β := ℝ) (‖g' y - g' x‖ * ‖w‖ * ‖w‖) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HAdd.hAdd (β := ℝ) (δ * HPow.hPow (β := ℕ) ‖w‖ 2)
      ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have rw : HAdd.hAdd (β := ℝ) (‖g' y - g' x‖ * (‖w‖ * ‖w‖)) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
  HAdd.hAdd (β := ℝ) (δ * (‖w‖ * ‖w‖)) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: rw [pow_two, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HAdd.hAdd (β := ℝ) (‖g' y - g' x‖ * (‖w‖ * ‖w‖))
      ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HAdd.hAdd (β := ℝ) (δ * (‖w‖ * ‖w‖)) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have bc : 0 ≤ ‖w‖ * ‖w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HAdd.hAdd (β := ℝ) (δ * HPow.hPow (β := ℕ) ‖w‖ 2)
      ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HAdd.hAdd (β := ℝ)
      (δ * HPow.hPow (β := ℕ) (‖(↑G : E x →L[ℝ] F)‖ * norm.{u_3} (E := E x) ((G.symm : (a : F) → E x) w : E x)) 2)
      ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have grw : HAdd.hAdd (β := ℝ) (δ * HPow.hPow (β := ℕ) ‖w‖ 2) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
  HAdd.hAdd (β := ℝ)
    (δ *
      HPow.hPow (β := ℕ)
        (norm.{u_2} (E := F) (((↑G : E x →L[ℝ] F) : (a : E x) → F) ((G.symm : (a : F) → E x) w : E x) : F)) 2)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: grw [← le_opNorm]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HAdd.hAdd (β := ℝ)
      (HMul.hMul (β := ℝ) (δ * C)
        ((((g x : (a : E x) → E x →L[ℝ] ℝ) ((G.symm : (a : F) → E x) w : E x) : E x →L[ℝ] ℝ) : (a : E x) → ℝ)
            ((G.symm : (a : F) → E x) w : E x) :
          ℝ))
      ((((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' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have e_a : Eq (α := ℝ)
  ((((g x : (a : E x) → E x →L[ℝ] ℝ) ((G.symm : (a : F) → E x) w : E x) : E x →L[ℝ] ℝ) : (a : E x) → ℝ)
      ((G.symm : (a : F) → E x) w : E x) :
    ℝ)
  ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ Eq (α := ℝ)
    ((((g x : (a : E x) → E x →L[ℝ] ℝ) ((G.symm : (a : F) → E x) w : E x) : E x →L[ℝ] ℝ) : (a : E x) → ℝ)
        ((G.symm : (a : F) → E x) w : E x) :
      ℝ)
    ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have e_a : Eq (α := ℝ)
  ((((g x : (a : E x) → E x →L[ℝ] ℝ) ((G.symm : (a : F) → E x) w : E x) : E x →L[ℝ] ℝ) : (a : E x) → ℝ)
      ((G.symm : (a : F) → E x) w : E x) :
    ℝ)
  (((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) :
        ℝ) :
    ℝ)
Tactic: rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ HMul.hMul (β := ℝ) (1 + δ * C) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) r' 2) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have ha : LE.le (α := ℝ) (0 : ℝ) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
G : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x
C : ℝ := HPow.hPow (β := ℕ) ‖(↑G : E x →L[ℝ] F)‖ 2
δ : ℝ
δpos : 0 < δ
h'δ : 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
hgx :
  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 : ℝ)
hgy :
  Eq (α := ℝ)
    ((((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) :
      ℝ)
    ((((g' y : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((((g' x : (a : F) → F →L[ℝ] ℝ) w : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
have ha : 0 ≤ HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: rw [← hgx, ← hg, real_inner_self_eq_norm_sq]