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 𝕜
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
this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x

Tactic:
rw [contMDiffAt_totalSpace] at this

Premises used: Bundle.contMDiffAt_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
x : TotalSpace F E
this :
  ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) x

Tactic:
this.1

Premises used: And.left
-- 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
this :
  ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) x

Tactic:
exact this.1

Premises used: And.left
-- 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 : Set (TotalSpace F E)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) s

Tactic:
(contMDiff_proj E).contMDiffOn

Premises used: ContMDiff.contMDiffOn, Bundle.contMDiff_proj
-- 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
p : TotalSpace F E
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) p

Tactic:
(contMDiff_proj E).contMDiffAt

Premises used: Bundle.contMDiff_proj, ContMDiff.contMDiffAt
-- 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 : Set (TotalSpace F E)
p : TotalSpace F E
⊢ ContMDiffWithinAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) s p

Tactic:
(contMDiffAt_proj E).contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Bundle.contMDiffAt_proj
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
rw :
  ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk (E := E) x 0) x

Tactic:
rw [contMDiffAt_section]

Premises used: Bundle.contMDiffAt_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 𝕜
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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
apply :
  EventuallyEq.{u_2, u_4} (β := F) (𝓝 x)
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2)
    fun (x : B) ↦ 0
⊢ ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x

Tactic:
apply (contMDiffAt_const (c := 0)).congr_of_eventuallyEq

Premises used: contMDiffAt_const, ContMDiffAt.congr_of_eventuallyEq
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x y : B
hy : y ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) y 0)).2 = 0

Tactic:
congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

Premises used: Bundle.zeroSection, Bundle.Trivialization.zeroSection, congr_arg, FiberBundle.trivializationAt, Prod.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 𝕜
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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
h :
  ∀ (a : B),
    Membership.mem (γ := Set B)
      {x_1 : B |
        x_1 ∈ Trivialization.baseSet (trivializationAt F E x) →
          Membership.mem (γ := Set B)
            {x_2 : B |
              (fun (x_3 : B) ↦
                  Eq.{u_4 + 1} (α := F)
                    ((fun (x_4 : B) ↦
                        ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_4 0)).2)
                      x_3)
                    ((fun (x : B) ↦ (0 : F)) x_3))
                x_2}
            x_1}
      a
h₁ h₂ :
  ∀ (y : B) (hy : y ∈ Trivialization.baseSet (trivializationAt F E x)),
    ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) y 0)).2 = 0
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝 x)
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2)
    fun (x : B) ↦ 0

Tactic:
filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds
    (mem_baseSet_trivializationAt F E x)] with y hy
    using congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

Premises used: Bundle.Trivialization.open_baseSet, congr_arg, FiberBundle.trivializationAt, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt, Prod.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 𝕜
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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
t : Set B
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) t

Tactic:
(contMDiff_zeroSection _ _).contMDiffOn

Premises used: ContMDiff.contMDiffOn, Bundle.contMDiff_zeroSection
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) x

Tactic:
(contMDiff_zeroSection _ _).contMDiffAt

Premises used: Bundle.contMDiff_zeroSection, ContMDiff.contMDiffAt
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
t : Set B
x : B
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) t x

Tactic:
(contMDiff_zeroSection _ _ x).contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Bundle.contMDiff_zeroSection
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
𝕜 : 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
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffVectorBundle n F E IB
⊢ ContMDiffVectorBundle m F E IB

Tactic:
⟨fun e e' _ _ ↦ (h.contMDiffOn_coordChangeL e e').of_le hmn⟩

Premises used: ContMDiffOn.of_le, ContMDiffVectorBundle.mk, ContMDiffVectorBundle.contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
a : ℕ∞ω
inst_19 : ContMDiffVectorBundle ∞ F E IB
h : ENat.LEInfty a
⊢ ContMDiffVectorBundle a F E IB

Tactic:
ContMDiffVectorBundle.of_le h.out

Premises used: ENat.LEInfty.out, ContMDiffVectorBundle.of_le
-- 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
a : ℕ∞ω
inst_19 : ContMDiffVectorBundle ω F E IB
⊢ ContMDiffVectorBundle a F E IB

Tactic:
ContMDiffVectorBundle.of_le le_top

Premises used: le_top, ContMDiffVectorBundle.of_le
-- 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 2 F E IB
⊢ ContMDiffVectorBundle 1 F E IB

Tactic:
ContMDiffVectorBundle.of_le one_le_two

Premises used: one_le_two, ContMDiffVectorBundle.of_le
-- 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
contMDiffOn_coordChangeL :
  ∀ (e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)))
    [inst_19 : MemTrivializationAtlas (E := E) e] [inst_20 : MemTrivializationAtlas (E := E) e'],
    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) 0
      (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
⊢ ContMDiffVectorBundle 0 F E IB

Tactic:
constructor
-- 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
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
he' : MemTrivializationAtlas (E := E) e'
contMDiffOn_coordChangeL :
  ContinuousOn.{u_2, u_4} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
⊢ 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) 0
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
rw [contMDiffOn_zero_iff]

Premises used: contMDiffOn_zero_iff
-- 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
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
he' : MemTrivializationAtlas (E := E) e'
⊢ ContinuousOn.{u_2, u_4} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
VectorBundle.continuousOn_coordChange' e e'

Premises used: VectorBundle.continuousOn_coordChange'
-- 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
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
he' : MemTrivializationAtlas (E := E) e'
⊢ ContinuousOn.{u_2, u_4} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
exact VectorBundle.continuousOn_coordChange' e e'

Premises used: VectorBundle.continuousOn_coordChange'
-- 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 e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
⊢ 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 := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
ContMDiffVectorBundle.contMDiffOn_coordChangeL e e'

Premises used: ContMDiffVectorBundle.contMDiffOn_coordChangeL