awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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_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
have 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 ℝ)
Tactic: convert! contMDiffAt_const (c := innerSL ℝ)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
⊢ 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 ℝ)
have 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 : ℝ)
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x
have 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
Tactic: rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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 IM IB n b s x
have 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
Tactic: simp only [contMDiffWithinAt_totalSpace] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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 IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x
have hb : ContMDiffWithinAt IM IB n b s x
Tactic: have hb : ContMDiffWithinAt IM IB n b s x := by
    simp only [contMDiffWithinAt_totalSpace] at hv
    exact hv.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x
have simp : ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n
  (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s x
Tactic: simp only [hg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM (IB.prod 𝓘(ℝ, ℝ)) (M' := TotalSpace ℝ (Trivial B ℝ)) n
    (fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    s x
have hψ : ContMDiffWithinAt IM (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 (x : B) ↦ E x →L[ℝ] E x →L[ℝ] Trivial B ℝ x) n
  (fun (m : M) ↦ ⟨b m, g (b m)⟩) s x
Tactic: apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hb : ContMDiffWithinAt IM IB n b s x
hψ :
  ContMDiffWithinAt IM (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 (x : B) ↦ E x →L[ℝ] E x →L[ℝ] Trivial B ℝ x) n
    (fun (m : M) ↦ ⟨b m, g (b m)⟩) s x
⊢ ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM (IB.prod 𝓘(ℝ, ℝ)) (M' := TotalSpace ℝ (Trivial B ℝ)) n
    (fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    s x
have hv₁ : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x
Tactic: apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hb : ContMDiffWithinAt IM IB n b s x
hψ :
  ContMDiffWithinAt IM (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 (x : B) ↦ E x →L[ℝ] E x →L[ℝ] Trivial B ℝ x) n
    (fun (m : M) ↦ ⟨b m, g (b m)⟩) s x
hv₁ : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x
⊢ ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM (IB.prod 𝓘(ℝ, ℝ)) (M' := TotalSpace ℝ (Trivial B ℝ)) n
    (fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    s x
have hw₁ : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x
Tactic: apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s
    x
have this : ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM (IB.prod 𝓘(ℝ, ℝ)) (M' := TotalSpace ℝ (Trivial B ℝ)) n
  (fun (m : M) ↦
    ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
  s x
Tactic: have : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ)) n
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x := by
    apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
    · exact ContMDiffAt.comp_contMDiffWithinAt x g_smooth.contMDiffAt hb
    · exact hv
    · exact hw
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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
hb : ContMDiffWithinAt IM IB n b s x
this :
  ContMDiffWithinAt.{0, u_6, u_7, u_8, u_1, u_2, u_3} IM (IB.prod 𝓘(ℝ, ℝ)) (M' := TotalSpace ℝ (Trivial B ℝ)) n
    (fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s
    x
have this₁ : 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 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (x_1 : M) ↦
      ((↑(trivializationAt ℝ (Trivial B ℝ) (b x)) : TotalSpace ℝ (Trivial B ℝ) → B × ℝ)
          ⟨b x_1,
            (((g (b x_1) : (a : E (b x_1)) → E (b x_1) →L[ℝ] ℝ) (v x_1) : E (b x_1) →L[ℝ] ℝ) : (a : E (b x_1)) → ℝ)
              (w x_1)⟩).2)
    s x
Tactic: simp only [contMDiffWithinAt_totalSpace] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
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 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) x
⊢ (MDiffAt[s] fun (m : M) ↦ ⟪v m, w m⟫) x
have 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[ℝ] ℝ) 1 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),
  (MDiffAt[s] fun (m : M) ↦ ⟪v m, w m⟫) x
Tactic: rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
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 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) 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[ℝ] ℝ) 1 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
⊢ MDiffAt[s] b x
have hv₁ : (MDiffAt[s] fun (x : M) ↦ b x) x ∧
  (MDiffAt[s] fun (x_1 : M) ↦ ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) ⟨b x_1, v x_1⟩).2) x
Tactic: simp only [mdifferentiableWithinAt_totalSpace] at hv
Cleared hypotheses: hv