awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ContMDiffOn IB (E' := F₁ × F₂ →L[𝕜] F₁ × F₂) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) (M' := F₁ × F₂ →L[𝕜] F₁ × F₂) n
    (fun (y : B) ↦
      ContinuousLinearMap.prodMap (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
ContMDiffOn.clm_prodMap ?_ ?_

Premises used: setOf, ContMDiffOn.clm_prodMap
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_11, u_11, u_11} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
(contMDiffOn_coordChangeL e₁ e₁').mono ?_

Premises used: ContMDiffOn.mono, contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
refine_1 :
  (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₁.baseSet ∩ e₁'.baseSet
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_11, u_11, u_11} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_

Premises used: ContMDiffOn.mono, contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
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.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_13, u_13, u_13} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
(contMDiffOn_coordChangeL e₂ e₂').mono ?_

Premises used: ContMDiffOn.mono, contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
refine_2 :
  (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₂.baseSet ∩ e₂'.baseSet
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_13, u_13, u_13} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
refine (contMDiffOn_coordChangeL e₂ e₂').mono ?_

Premises used: ContMDiffOn.mono, contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
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.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
⊢ ContMDiffOn IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) n (contMDiffCoordChange n (E := E) IB a he he')
    (e.baseSet ∩ e'.baseSet)

Tactic:
(Classical.choose_spec (ha.exists_contMDiffCoordChange e he e' he')).1

Premises used: Classical.choose_spec, And.left, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, VectorPrebundle.contMDiffCoordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2

Tactic:
(Classical.choose_spec (ha.exists_contMDiffCoordChange e he e' he')).2 b hb v

Premises used: Classical.choose_spec, And.right, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
fst :
  ((b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
snd :
  (b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
⊢ (b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
fst : ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
⊢ ((b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1

Tactic:
rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]

Premises used: And.left, Bundle.Pretrivialization.coe_fst', Bundle.Pretrivialization.proj_symm_apply', Bundle.Pretrivialization.mk_symm