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 𝕜
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 E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ e.coordChange e' (f x) (g x) =
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)

Tactic:
exact (Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm

Premises used: And.intro, Bundle.Trivialization.coordChangeL_apply', Eq.symm
-- 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 e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → B
g : M → F
x : M
hf : ContMDiffAt IM IB n f x
hg : ContMDiffAt IM 𝓘(𝕜, F) n g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ ContMDiffAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) x

Tactic:
hf.coordChange hg he he'

Premises used: ContMDiffWithinAt.coordChange, 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 e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
hf : ContMDiffOn IM IB n f s
hg : ContMDiffOn IM 𝓘(𝕜, F) n g s
he : MapsTo f s e.baseSet
he' : MapsTo f s e'.baseSet
⊢ ContMDiffOn IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) s

Tactic:
fun x hx ↦
  (hf x hx).coordChange (hg x hx) (he hx) (he' hx)

Premises used: ContMDiffWithinAt.coordChange, 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 e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → B
g : M → F
hf : ContMDiff IM IB n f
hg : ContMDiff IM 𝓘(𝕜, F) n g
he : ∀ (x : M), f x ∈ e.baseSet
he' : ∀ (x : M), f x ∈ e'.baseSet
⊢ ContMDiff IM 𝓘(𝕜, F) (M' := F) n fun (y : M) ↦ e.coordChange e' (f y) (g y)

Tactic:
fun x ↦
  (hf x).coordChange (hg x) (he x) (he' x)

Premises used: ContMDiff, ContMDiffAt.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'
⊢ MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet)

Tactic:
have Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet) := fun x hx ↦
    ⟨e.mem_target.1 hx.1, e'.mem_target.1 hx.2⟩
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet)
⊢ MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet

Tactic:
rw [mapsTo_inter] at Hmaps

Premises used: Set.mapsTo_inter
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F)
    (e.target ∩ e'.target)

Tactic:
(contMDiffOn_fst.prodMk
    (contMDiffOn_fst.coordChange contMDiffOn_snd Hmaps.1 Hmaps.2)).congr ?_

Premises used: ContMDiffOn.prodMk, contMDiffOn_fst, And.right, And.left, ContMDiffOn.congr, ContMDiffOn.coordChange, contMDiffOn_snd
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
refine :
  ∀ y ∈ e.target ∩ e'.target,
    (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) y = (y.1, e.coordChange e' y.1 y.2)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F)
    (e.target ∩ e'.target)

Tactic:
refine (contMDiffOn_fst.prodMk
    (contMDiffOn_fst.coordChange contMDiffOn_snd Hmaps.1 Hmaps.2)).congr ?_

Premises used: ContMDiffOn.prodMk, contMDiffOn_fst, And.right, And.left, ContMDiffOn.congr, ContMDiffOn.coordChange, contMDiffOn_snd
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
⊢ (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) (b, x) = ((b, x).1, e.coordChange e' (b, x).1 (b, x).2)

Tactic:
Prod.ext ?_ rfl

Premises used: Prod.ext, rfl
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
refine :
  ((↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) (b, x)).1 =
    ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1
⊢ (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) (b, x) = ((b, x).1, e.coordChange e' (b, x).1 (b, x).2)

Tactic:
refine Prod.ext ?_ rfl

Premises used: Prod.ext, rfl
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, x)).proj (E := E) ∈ e'.baseSet

Tactic:
simp_all only [Trivialization.mem_target, mfld_simps]

Premises used: Bundle.Trivialization.mem_target
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, x)).proj (E := E) ∈ e'.baseSet

Tactic:
have : (e.toOpenPartialHomeomorph.symm (b, x)).1 ∈ e'.baseSet := by
    simp_all only [Trivialization.mem_target, mfld_simps]
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
this : ((↑e.symm : B × F → TotalSpace F E) (b, x)).proj (E := E) ∈ e'.baseSet
⊢ ((↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) (b, x)).1 =
    ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1

Tactic:
(e'.coe_fst' this).trans (e.proj_symm_apply hb.1)

Premises used: Bundle.Trivialization.coe_fst', OpenPartialHomeomorph.toFun', And.left, Bundle.Trivialization.proj_symm_apply, Eq.trans
-- 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'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
b : B
x : F
hb : (b, x) ∈ e.target ∩ e'.target
this : ((↑e.symm : B × F → TotalSpace F E) (b, x)).proj (E := E) ∈ e'.baseSet
⊢ ((↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) (b, x)).1 =
    ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1

Tactic:
exact (e'.coe_fst' this).trans (e.proj_symm_apply hb.1)

Premises used: Bundle.Trivialization.coe_fst', And.left, Bundle.Trivialization.proj_symm_apply, Eq.trans
-- 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 e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj (E := E) ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e : TotalSpace F E → B × F) (f y)).2) s x
he : f x ∈ e.source
he' : f x ∈ e'.source
⊢ (f x).proj (E := E) ∈ e.baseSet

Tactic:
rw [Trivialization.mem_source] at he he'

Premises used: Bundle.Trivialization.mem_source
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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 E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj (E := E) ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e : TotalSpace F E → B × F) (f y)).2) s x
he : f x ∈ e.source
he' : f x ∈ e'.source
he₁ : (f x).proj (E := E) ∈ e.baseSet
⊢ (f x).proj (E := E) ∈ e'.baseSet

Tactic:
rw [Trivialization.mem_source] at he he'

Premises used: Bundle.Trivialization.mem_source
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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 E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj (E := E) ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e : TotalSpace F E → B × F) (f y)).2) s x
he : (f x).proj (E := E) ∈ e.baseSet
he' : (f x).proj (E := E) ∈ e'.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (f x)).2 =
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) x) ((↑e : TotalSpace F E → B × F) (f x)).2

Tactic:
simp [he]