awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
hϕ : ContinuousAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContinuousAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) m₀
hb₂ : ContinuousAt b₂ m₀
⊢ ContinuousAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) m₀
have rw : ∀
  (hϕ :
    ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
      univ m₀)
  (hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) univ m₀)
  (hb₂ : ContinuousWithinAt b₂ univ m₀),
  ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) univ m₀
Tactic: rw [← continuousWithinAt_univ] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B
inst_14 : TopologicalSpace M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousWithinAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    s x
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s x
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) s x
have hϕ₁ : ContinuousWithinAt.{u_13, u_9} (Y := B) (fun (x : M) ↦ b x) s x ∧
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (x_1 : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1))
    s x
Tactic: simp only [continuousWithinAt_hom_bundle] at hϕ
Cleared hypotheses: hϕ
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B
inst_14 : TopologicalSpace M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    x
hv : ContinuousAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) x
⊢ ContinuousAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) x
have simp : ∀
  (hϕ :
    ContinuousWithinAt (Y :=
      TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
      (fun (m : M) ↦
        TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
          (F₁ →L[𝕜] F₂) (b m) (ϕ m))
      univ x)
  (hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ x),
  ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) univ x
Tactic: simp only [← continuousWithinAt_univ] at hϕ hv ⊢
Cleared hypotheses: hϕ, hv
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B
inst_14 : TopologicalSpace M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  Continuous[inst_14, ContinuousLinearMap.topologicalSpaceTotalSpace (RingHom.id 𝕜) F₁ E₁ F₂ E₂] fun (m : M) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
      (F₁ →L[𝕜] F₂) (b m) (ϕ m)
hv : Continuous[inst_14, inst_5] fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)
⊢ Continuous[inst_14, inst_11] fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))
have simp : ∀
  (hϕ :
    ContinuousOn (Y :=
      TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
      (fun (m : M) ↦
        TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
          (F₁ →L[𝕜] F₂) (b m) (ϕ m))
      univ)
  (hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ),
  ContinuousOn (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) univ
Tactic: simp only [← continuousOn_univ] at hϕ hv ⊢
Cleared hypotheses: hϕ, hv
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
⊢ IsContinuousRiemannianBundle F₁ (Trivial B F₁)
have refine : Continuous[inst,
    topologicalSpaceTotalSpace (RingHom.id ℝ) F₁ (Trivial B F₁) (F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] ℝ]
  fun (x : B) ↦
  TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
    ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)
Tactic: refine ⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
⊢ Continuous[inst,
      topologicalSpaceTotalSpace (RingHom.id ℝ) F₁ (Trivial B F₁) (F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] ℝ]
    fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
      ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)
have rw : ∀ (x : B),
  ContinuousAt (Y :=
    TotalSpace.{u_1, u_4, u_4} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
    (fun (x : B) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
        ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x))
    x
Tactic: rw [continuous_iff_continuousAt]
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
x : B
⊢ ContinuousAt (Y :=
    TotalSpace.{u_1, u_4, u_4} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
    (fun (x : B) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
        ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x))
    x
have rw : ContinuousAt (Y := B)
    (fun (x : B) ↦
      TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
        (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)))
    x ∧
  ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                  Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
                    x ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
    x
Tactic: rw [FiberBundle.continuousAt_totalSpace]
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
x : B
⊢ ContinuousAt (Y := B)
      (fun (x : B) ↦
        TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)))
      x ∧
    ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      (fun (x_1 : B) ↦
        ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                    Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                    (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                      (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
                      ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
            (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
              ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
      x
have refine : ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
  (fun (x_1 : B) ↦
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
              (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
                  ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
        (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
  x
Tactic: refine ⟨continuousAt_id, ?_⟩
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
x : B
⊢ ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                  Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
                    x ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
    x
have h : ∀ (x_1 : B),
  Eq.{u_4 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
              (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
                  ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
        (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2
    (innerSL ℝ)
Tactic: convert! continuousAt_const (y := innerSL ℝ)
-- 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
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
x x_1 : B
⊢ Eq.{u_4 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
              (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
                  ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
        (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2
    (innerSL ℝ)
have h : ∀ (v w : F₁),
  Eq (α := ℝ)
    ((((((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                          (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                            Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                            (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                              (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
                              ((fun (x : B) ↦ (innerSL ℝ : 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[ℝ] ℝ))
                    (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                      (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
                      ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2 :
                (a : F₁) → F₁ →L[ℝ] ℝ)
              v :
            F₁ →L[ℝ] ℝ) :
          (a : F₁) → ℝ)
        w :
      ℝ)
    ((((innerSL ℝ : (a : F₁) → F₁ →L[ℝ] ℝ) v : F₁ →L[ℝ] ℝ) : (a : F₁) → ℝ) w : ℝ)
Tactic: ext v w
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x
have rcases : ∀ (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),
  ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x
Tactic: rcases h.exists_continuous with ⟨g, g_cont, hg⟩
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
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
⊢ ContinuousWithinAt b s x
have hv₁ : ContinuousWithinAt.{u_4, u_1} (Y := B) (fun (x : M) ↦ b x) s x ∧
  ContinuousWithinAt.{u_4, u_2} (Y := F)
    (fun (x_1 : M) ↦
      ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b x_1) (v x_1))).2)
    s x
Tactic: simp only [FiberBundle.continuousWithinAt_totalSpace] at hv
Cleared hypotheses: hv