awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have refine_2 : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have refine_2₃ : ∀ ⦃my_y : B⦄,
  (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: mfld_set_tac
-- 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
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
⊢ MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)]
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
have h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
Tactic: have h₁ := contMDiffOn_coordChangeL (IB := IB) e₁' e₁ (n := 1) |>.mdifferentiableOn one_ne_zero
-- 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
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
⊢ MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)]
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
have h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
Tactic: have h₂ := contMDiffOn_coordChangeL (IB := IB) e₂ e₂' (n := 1) |>.mdifferentiableOn one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
⊢ MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)]
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
have refine_1 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
Tactic: refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
refine_1 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
⊢ MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)]
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
have refine_2 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
Tactic: refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have refine_1 : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
refine_1 refine_1₁ refine_1₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have refine_1₃ : ∀ ⦃my_y : B⦄,
  (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have refine_2 : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (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_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle 1 F₁ E₁ IB
inst_23 : ContMDiffVectorBundle 1 F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ : MDiff[e₁'.baseSet ∩ e₁.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)
h₂ : MDiff[e₂.baseSet ∩ e₂'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have refine_2₃ : ∀ ⦃my_y : B⦄,
  (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: mfld_set_tac
-- 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)) s m₀
hv : ContMDiffWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) s m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ s m₀
⊢ 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 m₀
have rw : ∀
  (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 IM (IB₁.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b₁ m, v m⟩) (insert m₀ s) m₀)
  (hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀),
  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)⟩) (insert m₀ s) m₀
Tactic: rw [← contMDiffWithinAt_insert_self] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂