awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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
he he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContMDiffOn.{u_1, u_7, u_8, 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 := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
have simp_rw : ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
  (fun (b : B) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
  (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
Tactic: simp_rw [Bundle.Trivial.trivialization.coordChangeL]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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 (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_12, u_14} (E₁ x) (E₂ x))
            (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
        F₁ × F₂ →L[𝕜] F₁ × F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
have refine : 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: refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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)
have refine_1 : 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.clm_prodMap ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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)
have refine_1 : (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₁.baseSet ∩ e₁'.baseSet
Tactic: refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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₂'
⊢ 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.Basic (goal)
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
⊢ 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.Basic (goal)
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)
have refine_2 : (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₂.baseSet ∩ e₂'.baseSet
Tactic: refine (contMDiffOn_coordChangeL e₂ e₂').mono ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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₂'
⊢ 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.Basic (goal)
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
⊢ 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