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
s : (x : B) → E x
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x))
      e.baseSet ↔
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) e.baseSet

Tactic:
e.contMDiffOn_section_iff e.open_baseSet subset_rfl

Premises used: Bundle.Trivialization.open_baseSet, Bundle.Trivialization.contMDiffOn_section_iff, subset_rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
IB : ModelWithCorners 𝕜 EB HB
h : Z.IsContMDiff IB n
i j : ι
⊢ ContMDiffOn IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)

Tactic:
h.1 i j

Premises used: VectorBundleCore.IsContMDiff.contMDiffOn_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
inst_19 : ContMDiffVectorBundle n F E IB
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
⊢ 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 := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[𝕜] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)

Tactic:
(Z.contMDiffOn_coordChange IB i i').congr fun b hb ↦ ?_

Premises used: VectorBundleCore.contMDiffOn_coordChange, ContMDiffOn.congr
-- 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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
refine :
  ∀ (b : B) (hb : b ∈ Z.baseSet i ∩ Z.baseSet i'),
    (↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
            b) :
        F →L[𝕜] F) =
      Z.coordChange i i' b
⊢ 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 := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[𝕜] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)

Tactic:
refine (Z.contMDiffOn_coordChange IB i i').congr fun b hb ↦ ?_

Premises used: VectorBundleCore.contMDiffOn_coordChange, ContMDiffOn.congr
-- 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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
h :
  ∀ (v : F),
    Eq (α := F)
      (((↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                  (Z.toFiberBundleCore.localTriv i') b) :
              F →L[𝕜] F) :
            (a : F) → F)
          v :
        F)
      ((Z.coordChange i i' b : (a : F) → F) v : F)
⊢ (↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[𝕜] F) =
    Z.coordChange i i' b

Tactic:
ext v
-- 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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)

Tactic:
Z.localTriv_coordChange_eq i i' hb v

Premises used: VectorBundleCore.localTriv, Set.Mem, VectorBundleCore.localTriv_coordChange_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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)

Tactic:
exact Z.localTriv_coordChange_eq i i' hb v

Premises used: VectorBundleCore.localTriv_coordChange_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
e e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he : MemTrivializationAtlas (E := Trivial B F) e
he' : MemTrivializationAtlas (E := Trivial B F) e'
obtain :
  ∀ [he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)],
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
      (Trivialization.baseSet (trivialization B F) ∩ 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) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
obtain rfl := Bundle.Trivial.eq_trivialization B F e

Premises used: Bundle.Trivial.eq_trivialization, rfl
-- 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
e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he' : MemTrivializationAtlas (E := Trivial B F) e'
he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
obtain :
  ∀ [he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)],
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (b : B) ↦
        (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
      (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ e'.baseSet)

Tactic:
obtain rfl := Bundle.Trivial.eq_trivialization B F e'

Premises used: Bundle.Trivial.eq_trivialization, rfl
-- 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
he he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
simp_rw :
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))

Tactic:
simp_rw [Bundle.Trivial.trivialization.coordChangeL]

Premises used: Bundle.Trivial.trivialization.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
inst_19 : ContMDiffVectorBundle n F E IB
he he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))

Tactic:
contMDiff_const.contMDiffOn

Premises used: contMDiff_const, ContMDiff.contMDiffOn
-- 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
he he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))

Tactic:
exact contMDiff_const.contMDiffOn

Premises used: contMDiff_const, ContMDiff.contMDiffOn
-- 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
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ContMDiffOn IB (E' := F₁ × F₂ →L[𝕜] F₁ × F₂) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) (M' := F₁ × F₂ →L[𝕜] F₁ × F₂) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_12, u_14} (E₁ x) (E₂ x))
            (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
        F₁ × F₂ →L[𝕜] F₁ × F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')

Premises used: Bundle.Trivialization.coordChangeL_prod, ContMDiffOn.congr
-- 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
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
refine :
  ContMDiffOn IB (E' := F₁ × F₂ →L[𝕜] F₁ × F₂) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) (M' := F₁ × F₂ →L[𝕜] F₁ × F₂) n
    (fun (y : B) ↦
      ContinuousLinearMap.prodMap (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
⊢ ContMDiffOn IB (E' := F₁ × F₂ →L[𝕜] F₁ × F₂) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) (M' := F₁ × F₂ →L[𝕜] F₁ × F₂) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_12, u_14} (E₁ x) (E₂ x))
            (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
        F₁ × F₂ →L[𝕜] F₁ × F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')

Premises used: Bundle.Trivialization.coordChangeL_prod, ContMDiffOn.congr