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
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
refine :
  EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) fun (y : M) ↦
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) s x

Tactic:
refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ (by simp [he])

Premises used: ContMDiffWithinAt.coordChange, ContMDiffWithinAt.congr_of_eventuallyEq
-- 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
h :
  ∀ (y : M) (hy : y ∈ TotalSpace.proj (E := E) ∘ f ⁻¹' e.baseSet),
    ((↑e' : TotalSpace F E → B × F) (f y)).2 =
      e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) fun (y : M) ↦
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2

Tactic:
filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy

Premises used: Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds, ContMDiffWithinAt.continuousWithinAt
-- 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
y : M
hy : y ∈ TotalSpace.proj (E := E) ∘ f ⁻¹' e.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (f y)).2 =
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2

Tactic:
simp_all
-- 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
he : f x ∈ e.source
he' : f x ∈ e'.source
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e : TotalSpace F E → B × F) (f y)).2) s x ↔
    ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) s x

Tactic:
⟨(hp.change_section_trivialization · he he'), (hp.change_section_trivialization · he' he)⟩

Premises used: ContMDiffWithinAt.change_section_trivialization, Iff.intro
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
⊢ MemTrivializationAtlas (E := E) e

Tactic:
haveI : MemTrivializationAtlas e := ⟨he⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this : MemTrivializationAtlas (E := E) e
⊢ MemTrivializationAtlas (E := E) e'

Tactic:
haveI : MemTrivializationAtlas e' := ⟨he'⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
rw :
  ∃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen[inst_4] U) (hφ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U)
    (h2φ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U),
    EqOnSource
      (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
        (OpenPartialHomeomorph.symm
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e))
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e'))
      (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ Membership.mem (γ := StructureGroupoid (B × F)) (contMDiffFiberwiseLinear B F IB n)
    (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
      (OpenPartialHomeomorph.symm
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e))
      ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
          e.toOpenPartialHomeomorph)
        e'))

Tactic:
rw [mem_contMDiffFiberwiseLinear_iff]

Premises used: mem_contMDiffFiberwiseLinear_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
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
⊢ ∃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen[inst_4] U) (hφ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U)
    (h2φ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U),
    EqOnSource
      (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
        (OpenPartialHomeomorph.symm
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e))
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e'))
      (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)

Tactic:
⟨_, _, e.open_baseSet.inter e'.open_baseSet, contMDiffOn_coordChangeL e e',
      contMDiffOn_symm_coordChangeL e e', ?_⟩

Premises used: Bundle.Trivialization.open_baseSet, contMDiffOn_symm_coordChangeL, IsOpen.inter, Exists.intro, 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
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
refine :
  EqOnSource
    (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
      (OpenPartialHomeomorph.symm
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e))
      ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
          e.toOpenPartialHomeomorph)
        e'))
    (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') ⋯
      ⋯ ⋯)
⊢ ∃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen[inst_4] U) (hφ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U)
    (h2φ :
    ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U),
    EqOnSource
      (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
        (OpenPartialHomeomorph.symm
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e))
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e'))
      (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)

Tactic:
refine ⟨_, _, e.open_baseSet.inter e'.open_baseSet, contMDiffOn_coordChangeL e e',
      contMDiffOn_symm_coordChangeL e e', ?_⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
⊢ EqOnSource
    (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
      (OpenPartialHomeomorph.symm
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e))
      ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
          e.toOpenPartialHomeomorph)
        e'))
    (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') ⋯
      ⋯ ⋯)

Tactic:
OpenPartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩

Premises used: Setoid.symm, And.intro
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
⊢ (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') ⋯ ⋯
        ⋯).source =
    PartialEquiv.source (β := B × F)
      (toPartialEquiv
        (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
          (OpenPartialHomeomorph.symm
            ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
                e.toOpenPartialHomeomorph)
              e))
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e')))

Tactic:
simp only [FiberwiseLinear.openPartialHomeomorph, trans_toPartialEquiv, symm_toPartialEquiv,
        e.symm_trans_source_eq e']

Premises used: OpenPartialHomeomorph.symm_toPartialEquiv, OpenPartialHomeomorph.trans_toPartialEquiv, FiberwiseLinear.openPartialHomeomorph, Bundle.Trivialization.symm_trans_source_eq