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
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ ContMDiffWithinAt IM (ModelWithCorners.prod 𝓘(𝕜, EB) 𝓘(𝕜, F)) (M' := EB × F) n
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
        (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀

Tactic:
(contMDiffWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)

Premises used: contMDiffWithinAt_prod_iff, Iff.rfl, setOf, instTopologicalSpaceModelProd._aux_1, Iff.trans, ModelProd, and_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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
refine :
  ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀
⊢ ContMDiffWithinAt IM (ModelWithCorners.prod 𝓘(𝕜, EB) 𝓘(𝕜, F)) (M' := EB × F) n
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
        (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀

Tactic:
refine (contMDiffWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)

Premises used: contMDiffWithinAt_prod_iff, Iff.rfl, Iff.trans, and_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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀

Tactic:
have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
    ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
      ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
⊢ ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀

Tactic:
EventuallyEq.contMDiffWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_

Premises used: Filter.eventually_of_mem, Filter.EventuallyEq.contMDiffWithinAt_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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
refine_1 :
  (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
      ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1 =
    (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))
⊢ Eq.{u_7 + 1} (α := EB)
    (Function.comp (β := EB × F) Prod.fst
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      x)
    ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)

Tactic:
simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]

Premises used: OpenPartialHomeomorph.coe_coe, Function.comp, Bundle.Trivialization.coe_coe
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
refine_1 : (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))
⊢ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
      ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1 =
    (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))

Tactic:
rw [Trivialization.coe_fst']

Premises used: Bundle.Trivialization.coe_fst'
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))

Tactic:
hx

Premises used: Set.Mem, setOf, Set.preimage
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))

Tactic:
exact hx
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
⊢ Function.comp (β := EB × F) Prod.fst
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      x₀ =
    (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x₀).proj (E := E))

Tactic:
simp only [mfld_simps]
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f univ x₀ ↔
    ContMDiffWithinAt.{u_1, u_10, u_11, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) univ
        x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) univ x₀

Tactic:
contMDiffWithinAt_totalSpace

Premises used: Bundle.contMDiffWithinAt_totalSpace
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f univ x₀ ↔
    ContMDiffWithinAt.{u_1, u_10, u_11, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) univ
        x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) univ x₀

Tactic:
exact contMDiffWithinAt_totalSpace

Premises used: Bundle.contMDiffWithinAt_totalSpace
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
simp_rw :
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a
      x₀ →
    ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ x) a x₀
⊢ 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) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀

Tactic:
simp_rw [contMDiffWithinAt_totalSpace, and_iff_right_iff_imp]

Premises used: Bundle.contMDiffWithinAt_totalSpace, and_iff_right_iff_imp
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
h :
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ x) a x₀

Tactic:
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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
h :
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ x) a x₀

Tactic:
exact 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
x₀ : B
simp_rw :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) x₀ →
    ContMDiffAt IB IB (M' := B) n (fun (x : B) ↦ x) x₀
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x₀ ↔
    ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) x₀

Tactic:
simp_rw [contMDiffAt_totalSpace, and_iff_right_iff_imp]

Premises used: Bundle.contMDiffAt_totalSpace, and_iff_right_iff_imp
-- 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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
x₀ : B
h :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) x₀
⊢ ContMDiffAt IB IB (M' := B) n (fun (x : B) ↦ x) x₀

Tactic:
contMDiffAt_id

Premises used: contMDiffAt_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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
x₀ : B
h :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) x₀
⊢ ContMDiffAt IB IB (M' := B) n (fun (x : B) ↦ x) x₀

Tactic:
exact contMDiffAt_id

Premises used: contMDiffAt_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 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x

Tactic:
have : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x := contMDiffAt_id