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
inst_20 : IsManifold IB n B
e : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst_4] U
hφ :
  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 (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ :
  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 (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ (φ x.1 : (a : F) → F) x.2)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).source

Tactic:
exact (hφ.comp contMDiffOn_fst <| prod_subset_preimage_fst _ _).clm_apply contMDiffOn_snd

Premises used: Set.prod_subset_preimage_fst, ContMDiffOn.clm_apply, contMDiffOn_fst, contMDiffOn_snd, ContMDiffOn.comp
-- 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
inst_20 : IsManifold IB n B
e : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst_4] U
hφ :
  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 (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ :
  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 (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
refine_2 :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).symm : B × F → B × F)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).symm : B × F → B × F) e.target

Tactic:
rw [EqOnSource.target_eq heφ]

Premises used: OpenPartialHomeomorph.EqOnSource.target_eq
-- 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
inst_20 : IsManifold IB n B
e : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst_4] U
hφ :
  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 (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ :
  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 (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
refine_2 :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ ((φ x.1).symm : (a : F) → F) x.2)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).symm : B × F → B × F)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target

Tactic:
apply contMDiffOn_fst.prodMk

Premises used: ContMDiffOn.prodMk, contMDiffOn_fst
-- 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
inst_20 : IsManifold IB n B
e : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst_4] U
hφ :
  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 (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ :
  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 (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ ((φ x.1).symm : (a : F) → F) x.2)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target

Tactic:
(h2φ.comp contMDiffOn_fst <| prod_subset_preimage_fst _ _).clm_apply contMDiffOn_snd

Premises used: Set.prod_subset_preimage_fst, ContMDiffOn.clm_apply, contMDiffOn_fst, contMDiffOn_snd, ContMDiffOn.comp
-- 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
inst_20 : IsManifold IB n B
e : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst_4] U
hφ :
  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 (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ :
  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 (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ ((φ x.1).symm : (a : F) → F) x.2)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target

Tactic:
exact (h2φ.comp contMDiffOn_fst <| prod_subset_preimage_fst _ _).clm_apply contMDiffOn_snd

Premises used: Set.prod_subset_preimage_fst, ContMDiffOn.clm_apply, contMDiffOn_fst, contMDiffOn_snd, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
x₀ : M
he : f x₀ ∈ e.source
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
    ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s x₀

Tactic:
contMDiffWithinAt_totalSpace.trans <| and_congr_right fun h ↦
    Trivialization.contMDiffWithinAt_snd_comp_iff₂ h FiberBundle.mem_trivializationAt_proj_source he

Premises used: Bundle.contMDiffWithinAt_totalSpace, and_congr_right, FiberBundle.mem_trivializationAt_proj_source, Iff.trans, Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
x₀ : M
he : f x₀ ∈ e.source
⊢ ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
    ContMDiffAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      ContMDiffAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
e.contMDiffWithinAt_iff he

Premises used: Bundle.Trivialization.contMDiffWithinAt_iff, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
simp :
  (∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s x
⊢ ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔
    ContMDiffOn.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s ∧
      ContMDiffOn IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s

Tactic:
simp only [ContMDiffOn, ← forall_and]

Premises used: forall_and, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
⊢ (∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s x

Tactic:
forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff (he hx)

Premises used: Bundle.Trivialization.contMDiffWithinAt_iff, forall₂_congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
⊢ (∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s x

Tactic:
exact forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff (he hx)

Premises used: Bundle.Trivialization.contMDiffWithinAt_iff, forall₂_congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
he : ∀ (x : M), f x ∈ e.source
⊢ ContMDiff IM (IB.prod 𝓘(𝕜, F)) n f ↔
    (ContMDiff.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n fun (x : M) ↦ (f x).proj (E := E)) ∧
      ContMDiff IM 𝓘(𝕜, F) (M' := F) n fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2

Tactic:
(forall_congr' fun x ↦ e.contMDiffAt_iff (he x)).trans forall_and

Premises used: ContMDiff, Bundle.Trivialization.contMDiffAt_iff, forall_congr', Iff.trans, forall_and
-- 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.prod 𝓘(𝕜, F)) n id e.source

Tactic:
have : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source := contMDiffOn_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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
this : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) e.source ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : TotalSpace F E) ↦ ((↑e : TotalSpace F E → B × F) (id x)).2) e.source

Tactic:
rw [e.contMDiffOn_iff (mapsTo_id _)] at this

Premises used: Set.mapsTo_id, Bundle.Trivialization.contMDiffOn_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
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
this :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) e.source ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : TotalSpace F E) ↦ ((↑e : TotalSpace F E → B × F) (id x)).2) e.source
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : TotalSpace F E → B × F) e.source

Tactic:
(this.1.prodMk this.2).congr fun x hx ↦ (e.mk_proj_snd hx).symm

Premises used: ContMDiffOn.prodMk, And.right, And.left, ContMDiffOn.congr, Eq.symm, Bundle.Trivialization.mk_proj_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
this :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) e.source ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : TotalSpace F E) ↦ ((↑e : TotalSpace F E → B × F) (id x)).2) e.source
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : TotalSpace F E → B × F) e.source

Tactic:
exact (this.1.prodMk this.2).congr fun x hx ↦ (e.mk_proj_snd hx).symm

Premises used: ContMDiffOn.prodMk, And.right, And.left, ContMDiffOn.congr, Eq.symm, Bundle.Trivialization.mk_proj_snd