awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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
refine_2₃ 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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_11
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₂
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
f : M → TotalSpace (F₁ →L[𝕜] F₂) fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)
s : Set M
x₀ : M
⊢ ContMDiffWithinAt IM (E' := EB × (F₁ →L[𝕜] F₂)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f s x₀ ↔
    ContMDiffWithinAt.{u_1, u_10, u_11, u_5, u_8, u_9, u_2} IM IB (M' := B) n
        (fun (x : M) ↦
          (f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        s x₀ ∧
      ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
        (fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
        s x₀

Tactic:
contMDiffWithinAt_totalSpace

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.inCoordinates, Bundle.contMDiffWithinAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_11
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₂
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
f : M → TotalSpace (F₁ →L[𝕜] F₂) fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)
x₀ : M
⊢ ContMDiffAt IM (E' := EB × (F₁ →L[𝕜] F₂)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f x₀ ↔
    ContMDiffAt.{u_1, u_10, u_11, u_5, u_8, u_9, u_2} IM IB (M' := B) n
        (fun (x : M) ↦
          (f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        x₀ ∧
      ContMDiffAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
        (fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
        x₀

Tactic:
contMDiffAt_totalSpace

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.inCoordinates, Bundle.contMDiffAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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] 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
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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] 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
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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₂')

Tactic:
(h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)

Premises used: MDifferentiableOn.mono, ContinuousLinearEquiv.arrowCongr, MDifferentiableOn.cle_arrowCongr, Bundle.Pretrivialization.continuousLinearMapCoordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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
refine_2 : 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₂')

Tactic:
refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)

Premises used: MDifferentiableOn.mono, MDifferentiableOn.cle_arrowCongr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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
refine_1₃ 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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
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
refine_2₃ 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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_11
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₂
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
f : M → TotalSpace (F₁ →L[𝕜] F₂) fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)
s : Set M
x₀ : M
⊢ MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun (x : M) ↦
          (f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        x₀ ∧
      (MDiffAt[s] fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
        x₀

Tactic:
mdifferentiableWithinAt_totalSpace IB ..

Premises used: ContinuousLinearMap.comp, mdifferentiableWithinAt_totalSpace, ContinuousLinearMap.inCoordinates
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_11
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₂
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
f : M → TotalSpace (F₁ →L[𝕜] F₂) fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)
x₀ : M
⊢ MDiffAt f x₀ ↔
    (MDiffAt fun (x : M) ↦
          (f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        x₀ ∧
      (MDiffAt fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x₀).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
            ((f x).snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
        x₀

Tactic:
mdifferentiableAt_totalSpace ..

Premises used: ContinuousLinearMap.comp, mdifferentiableAt_totalSpace, ContinuousLinearMap.inCoordinates