awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContMDiffWithinAt.{u_1, u_13, u_14, u_6, u_9, u_10, u_4} IM IB₁ (M' := B₁) n
      (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) (M' := F₁) n
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      (insert m₀ s) m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
have a : Membership.mem (γ := Filter B₁) (𝓝 ((fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀))
  (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))
Tactic: apply hv.1.continuousWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContMDiffWithinAt.{u_1, u_13, u_14, u_6, u_9, u_10, u_4} IM IB₁ (M' := B₁) n
      (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) (M' := F₁) n
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      (insert m₀ s) m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
⊢ Membership.mem (γ := Filter B₁)
    (𝓝 ((fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀))
    (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))
have a : (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∈
  Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
Tactic: apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContMDiffWithinAt.{u_1, u_13, u_14, u_6, u_9, u_10, u_4} IM IB₁ (M' := B₁) n
      (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) (M' := F₁) n
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      (insert m₀ s) m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
have a : Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)
Tactic: apply hb₂.continuousWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContMDiffWithinAt.{u_1, u_13, u_14, u_6, u_9, u_10, u_4} IM IB₁ (M' := B₁) n
      (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) (M' := F₁) n
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      (insert m₀ s) m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
⊢ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)
have a : b₂ m₀ ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
Tactic: apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
hϕ :
  ContMDiffAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContMDiffAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : ContMDiffAt IM IB₂ n b₂ m₀
⊢ ContMDiffAt IM (IB₂.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n
    (fun (m : M) ↦ ⟨b₂ m, (ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)⟩) m₀
have hϕ₁ : ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
  (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) univ m₀
Tactic: rw [← contMDiffWithinAt_univ] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
hϕ :
  ContMDiffAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContMDiffAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : ContMDiffAt IM IB₂ n b₂ m₀
hϕ₁ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) univ m₀
⊢ ContMDiffAt IM (IB₂.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n
    (fun (m : M) ↦ ⟨b₂ m, (ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)⟩) m₀
have hv₁ : ContMDiffWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) univ m₀
Tactic: rw [← contMDiffWithinAt_univ] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
hϕ :
  ContMDiffAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContMDiffAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : ContMDiffAt IM IB₂ n b₂ m₀
hϕ₁ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) univ m₀
hv₁ : ContMDiffWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) univ m₀
⊢ ContMDiffAt IM (IB₂.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n
    (fun (m : M) ↦ ⟨b₂ m, (ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)⟩) m₀
have hb₃ : ContMDiffWithinAt IM IB₂ n b₂ univ m₀
Tactic: rw [← contMDiffWithinAt_univ] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (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_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_10
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_11
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
EM : Type u_12
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_13
inst_20 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_21 : TopologicalSpace M
inst_22 : ChartedSpace HM M
inst_23 : FiberBundle F₁ E₁
inst_24 : VectorBundle 𝕜 F₁ E₁
inst_25 : FiberBundle F₂ E₂
inst_26 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_8} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_8} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContMDiffWithinAt IM (E' := EB × (F₁ →L[𝕜] F₂)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) (M' :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ x) (E₂ x)) n
    (fun (m : M) ↦ ⟨b m, ϕ m⟩) s x
hv : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b m, v m⟩) s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n
    (fun (m : M) ↦ ⟨b m, (ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m)⟩) s x
have hϕ₁ : ContMDiffWithinAt.{u_1, u_12, u_13, u_6, u_10, u_11, u_2} IM IB (M' := B) n (fun (x : M) ↦ b x) s x ∧
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (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 [contMDiffWithinAt_hom_bundle] at hϕ
Cleared hypotheses: hϕ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (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_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_10
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_11
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
EM : Type u_12
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_13
inst_20 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_21 : TopologicalSpace M
inst_22 : ChartedSpace HM M
inst_23 : FiberBundle F₁ E₁
inst_24 : VectorBundle 𝕜 F₁ E₁
inst_25 : FiberBundle F₂ E₂
inst_26 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_8} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_8} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ : MDiffAt[s] (T% ϕ) x
hv : MDiffAt[s] (T% v) x
⊢ (MDiffAt[s] fun (m : M) ↦ ⟨b m, (ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m)⟩) x
have hϕ₁ : (MDiffAt[s] fun (x : M) ↦ b x) x ∧
  (MDiffAt[s] fun (x_1 : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) x
Tactic: simp only [mdifferentiableWithinAt_hom_bundle] at hϕ
Cleared hypotheses: hϕ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s' x_1 x
have this : LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s x_1 x
Tactic: have := hs.linearIndependent hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s' x_1 x))
have this : LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s x_1 x))
Tactic: have := hs.generating hx