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 : ℕ∞ω
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

Tactic:
have hb : ContMDiffWithinAt IM IB n b s x := by
    simp only [contMDiffWithinAt_totalSpace] at hv
    exact hv.1
-- 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
hb : ContMDiffWithinAt IM IB n b s x
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
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) (M' := ℝ) n (fun (m : M) ↦ ⟪v m, w m⟫) s x

Tactic:
simp only [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 : ℕ∞ω
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
hw₁ : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w 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

Tactic:
apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)

Premises used: ContMDiffWithinAt.clm_bundle_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
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 (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:
ContMDiffAt.comp_contMDiffWithinAt x g_smooth.contMDiffAt hb

Premises used: ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- 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
hb : ContMDiffWithinAt IM IB n b s x
⊢ 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:
exact ContMDiffAt.comp_contMDiffWithinAt x g_smooth.contMDiffAt hb

Premises used: ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- 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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x

Tactic:
hv
-- 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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, v m⟩) s x

Tactic:
exact hv
-- 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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x

Tactic:
hw
-- 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
hb : ContMDiffWithinAt IM IB n b s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) (M' := TotalSpace F E) n (fun (m : M) ↦ ⟨b m, w m⟩) s x

Tactic:
exact hw
-- 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
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

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
-- 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
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.{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

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
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 (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
⊢ 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:
this.2

Premises used: And.right
-- 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
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 (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
⊢ 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:
exact this.2

Premises used: And.right