awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
h : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
rcases :
  ∀ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ)
    (g_smooth :
      ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
        TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩)
    (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),
    IsContMDiffRiemannianBundle IB n' F E
⊢ IsContMDiffRiemannianBundle IB n' F E

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩

Premises used: IsContMDiffRiemannianBundle.exists_contMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
h : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩
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
⊢ IsContMDiffRiemannianBundle IB n' F E

Tactic:
⟨g, g_smooth.of_le h', hg⟩

Premises used: And.intro, Exists.intro, ContMDiff.of_le, IsContMDiffRiemannianBundle.mk
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
h : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩
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
⊢ IsContMDiffRiemannianBundle IB n' F E

Tactic:
exact ⟨g, g_smooth.of_le h', hg⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
a : ℕ∞ω
inst_12 : IsContMDiffRiemannianBundle IB ∞ F E
h : LEInfty a
⊢ IsContMDiffRiemannianBundle IB a F E

Tactic:
IsContMDiffRiemannianBundle.of_le h.out

Premises used: ENat.LEInfty.out, IsContMDiffRiemannianBundle.of_le
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
a : ℕ∞ω
inst_12 : IsContMDiffRiemannianBundle IB ω F E
⊢ IsContMDiffRiemannianBundle IB a F E

Tactic:
IsContMDiffRiemannianBundle.of_le le_top

Premises used: IsContMDiffRiemannianBundle.of_le, le_top
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
inst_12 : IsContMDiffRiemannianBundle IB 1 F E
⊢ IsContMDiffRiemannianBundle IB 0 F E

Tactic:
IsContMDiffRiemannianBundle.of_le zero_le_one

Premises used: IsContMDiffRiemannianBundle.of_le, zero_le_one
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
inst_12 : IsContMDiffRiemannianBundle IB 2 F E
⊢ IsContMDiffRiemannianBundle IB 1 F E

Tactic:
IsContMDiffRiemannianBundle.of_le one_le_two

Premises used: IsContMDiffRiemannianBundle.of_le, one_le_two
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
inst_12 : IsContMDiffRiemannianBundle IB 3 F E
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LE.le (α := ℕ) 2 3
⊢ LE.le (α := ℕ∞ω) 2 3

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
⊢ IsContMDiffRiemannianBundle IB n F₁ (Trivial B F₁)

Tactic:
⟨fun x ↦ innerSL ℝ, fun x ↦ ?_, fun x v w ↦ rfl⟩

Premises used: Real, innerSL, And.intro, Exists.intro, IsContMDiffRiemannianBundle.mk, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
refine :
  ∀ (x : B),
    ContMDiffAt IB (E' := Prod.{u_1, u_6} EB (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (M' :=
      TotalSpace.{u_3, u_6, u_6} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (b : B) ↦ Trivial B F₁ b →L[ℝ] Trivial B F₁ b →L[ℝ] ℝ) n
      (fun (b : B) ↦ ⟨b, (fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) b⟩) x
⊢ IsContMDiffRiemannianBundle IB n F₁ (Trivial B F₁)

Tactic:
refine ⟨fun x ↦ innerSL ℝ, fun x ↦ ?_, fun x v w ↦ rfl⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x : B
simp :
  ContMDiffAt.{0, u_1, u_2, u_3, u_6, u_6, u_6} IB (E' := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (M' :=
    F₁ →L[ℝ] F₁ →L[ℝ] ℝ) n
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2)
    x
⊢ ContMDiffAt IB (E' := Prod.{u_1, u_6} EB (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_6, u_6} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (b : B) ↦ Trivial B F₁ b →L[ℝ] Trivial B F₁ b →L[ℝ] ℝ) n
    (fun (b : B) ↦ ⟨b, (fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) b⟩) x

Tactic:
simp only [contMDiffAt_section]

Premises used: Bundle.contMDiffAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x : B
⊢ ContMDiffAt.{0, u_1, u_2, u_3, u_6, u_6, u_6} IB (E' := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (M' :=
    F₁ →L⋆[ℝ] F₁ →L[ℝ] ℝ) n (fun (x : B) ↦ innerSL ℝ) x

Tactic:
contMDiffAt_const (c := innerSL ℝ)

Premises used: contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x : B
h :
  ∀ (x_1 : B),
    Eq.{u_6 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2
      (innerSL ℝ)
⊢ ContMDiffAt.{0, u_1, u_2, u_3, u_6, u_6, u_6} IB (E' := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (M' :=
    F₁ →L[ℝ] F₁ →L[ℝ] ℝ) n
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          ⟨x_1, innerSL ℝ⟩).2)
    x

Tactic:
convert! contMDiffAt_const (c := innerSL ℝ)

Premises used: contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x x_1 : B
h :
  ∀ (v w : F₁),
    Eq (α := ℝ)
      ((((((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
                        (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                          B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
                      ⟨x_1, innerSL ℝ⟩).2 :
                  (a : F₁) → F₁ →L[ℝ] ℝ)
                v :
              F₁ →L[ℝ] ℝ) :
            (a : F₁) → ℝ)
          w :
        ℝ)
      ((((innerSL ℝ : (a : F₁) → F₁ →L[ℝ] ℝ) v : F₁ →L[ℝ] ℝ) : (a : F₁) → ℝ) w : ℝ)
⊢ Eq.{u_6 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
          (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
            B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2
    (innerSL ℝ)

Tactic:
ext v w
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x x_1 : B
v w : F₁
⊢ Eq (α := ℝ)
    ((((((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
                      (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                        B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
                    ⟨x_1, innerSL ℝ⟩).2 :
                (a : F₁) → F₁ →L[ℝ] ℝ)
              v :
            F₁ →L[ℝ] ℝ) :
          (a : F₁) → ℝ)
        w :
      ℝ)
    ((((innerSL ℝ : (a : F₁) → F₁ →L[ℝ] ℝ) v : F₁ →L[ℝ] ℝ) : (a : F₁) → ℝ) w : ℝ)

Tactic:
simp [hom_trivializationAt_apply, inCoordinates]

Premises used: ContinuousLinearMap.inCoordinates, hom_trivializationAt_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x
rcases :
  ∀ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ)
    (g_smooth :
      ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
        TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩)
    (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),
    ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩

Premises used: IsContMDiffRiemannianBundle.exists_contMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩
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
⊢ ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM IB (M' := B) n (fun (x : M) ↦ b x) s x ∧
    ContMDiffWithinAt IM 𝓘(ℝ, F) (M' := F) n
      (fun (x_1 : M) ↦ ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) ⟨b x_1, v x_1⟩).2) s x

Tactic:
simp only [contMDiffWithinAt_totalSpace] at hv

Premises used: Bundle.contMDiffWithinAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩
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
hv :
  ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM IB (M' := B) n (fun (x : M) ↦ b x) s x ∧
    ContMDiffWithinAt IM 𝓘(ℝ, F) (M' := F) n
      (fun (x_1 : M) ↦ ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) ⟨b x_1, v x_1⟩).2) s x
⊢ ContMDiffWithinAt IM IB n b s x

Tactic:
hv.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩
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
hv :
  ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM IB (M' := B) n (fun (x : M) ↦ b x) s x ∧
    ContMDiffWithinAt IM 𝓘(ℝ, F) (M' := F) n
      (fun (x_1 : M) ↦ ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) ⟨b x_1, v x_1⟩).2) s x
⊢ ContMDiffWithinAt IM IB n b s x

Tactic:
exact hv.1

Premises used: And.left