awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
rw :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : B × F) ↦ ((↑e.symm : B × F → TotalSpace F E) x).proj (E := E))
      e.target ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : B × F) ↦ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2) e.target
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm : B × F → TotalSpace F E) e.target

Tactic:
rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.symm_mapsTo]

Premises used: OpenPartialHomeomorph.symm_mapsTo, Bundle.Trivialization.contMDiffOn_iff, Bundle.Trivialization.toOpenPartialHomeomorph
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : B × F) ↦ ((↑e.symm : B × F → TotalSpace F E) x).proj (E := E))
      e.target ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : B × F) ↦ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2) e.target

Tactic:
⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
    contMDiffOn_snd.congr fun x hx ↦ ?_⟩

Premises used: contMDiffOn_fst, ContMDiffOn.congr, And.intro, Bundle.Trivialization.proj_symm_apply, contMDiffOn_snd
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
refine :
  ∀ (x : B × F) (hx : x ∈ e.target), ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2 = x.2
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : B × F) ↦ ((↑e.symm : B × F → TotalSpace F E) x).proj (E := E))
      e.target ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : B × F) ↦ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2) e.target

Tactic:
refine ⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
    contMDiffOn_snd.congr fun x hx ↦ ?_⟩
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
x : B × F
hx : x ∈ e.target
rw rw₁ : x.2 = x.2
⊢ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2 = x.2

Tactic:
rw [e.apply_symm_apply hx]

Premises used: Bundle.Trivialization.apply_symm_apply
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
rw :
  ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ (TotalSpace.mk' (E := E) F x (s x)).proj (E := E)) a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
rw₁ : TotalSpace.mk' (E := E) F x₀ (s x₀) ∈ e.source
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀

Tactic:
rw [e.contMDiffWithinAt_iff]

Premises used: Bundle.Trivialization.contMDiffWithinAt_iff
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
change :
  ContMDiffWithinAt IB IB n id a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ (TotalSpace.mk' (E := E) F x (s x)).proj (E := E)) a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀

Tactic:
change ContMDiffWithinAt IB IB n id a x₀ ∧ _ ↔ _

Premises used: ContMDiffWithinAt, id
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB IB n id a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀

Tactic:
simp [contMDiffWithinAt_id]

Premises used: contMDiffWithinAt_id
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
rwa rwa₁ rwa₂ rwa₃ : (TotalSpace.mk' (E := E) F x₀ (s x₀)).proj (E := E) ∈ e.baseSet
⊢ TotalSpace.mk' (E := E) F x₀ (s x₀) ∈ e.source

Tactic:
rwa [mem_source]

Premises used: Bundle.Trivialization.mem_source
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) univ
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) univ x₀

Tactic:
e.contMDiffWithinAt_section univ hx₀

Premises used: Set.univ, Bundle.Trivialization.contMDiffWithinAt_section
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) univ
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) univ x₀

Tactic:
exact e.contMDiffWithinAt_section univ hx₀

Premises used: Set.univ, Bundle.Trivialization.contMDiffWithinAt_section
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a

Tactic:
⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Premises used: Iff.intro
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
refine_1 :
  ∀ (h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a)
    (x : B) (hx : x ∈ a),
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x
refine_2 :
  ∀
    (h :
      ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a)
    (x : B) (hx : x ∈ a),
    ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
      x
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
x : B
hx : x ∈ a
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x

Tactic:
have := (h x hx).contMDiffAt <| ha.mem_nhds hx
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h :
  ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    a
x : B
hx : x ∈ a
⊢ ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    x

Tactic:
have := (h x hx).contMDiffAt <| ha.mem_nhds hx
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
x : B
hx : x ∈ a
this : ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x

Tactic:
((e.contMDiffAt_section_iff (ha' hx)).mp this).contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Bundle.Trivialization.contMDiffAt_section_iff, Iff.mp
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
x : B
hx : x ∈ a
this : ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x

Tactic:
exact ((e.contMDiffAt_section_iff (ha' hx)).mp this).contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Bundle.Trivialization.contMDiffAt_section_iff, Iff.mp
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h :
  ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    a
x : B
hx : x ∈ a
this :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    x
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a x

Tactic:
((e.contMDiffAt_section_iff (ha' hx)).mpr this).contMDiffWithinAt

Premises used: Iff.mpr, ContMDiffAt.contMDiffWithinAt, Bundle.Trivialization.contMDiffAt_section_iff
-- 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 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_4] a
ha' : a ⊆ e.baseSet
h :
  ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    a
x : B
hx : x ∈ a
this :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    x
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a x

Tactic:
exact ((e.contMDiffAt_section_iff (ha' hx)).mpr this).contMDiffWithinAt

Premises used: Iff.mpr, ContMDiffAt.contMDiffWithinAt, Bundle.Trivialization.contMDiffAt_section_iff