awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F)
    (e.target ∩ e'.target)
have Hmaps₁ : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
Tactic: rw [mapsTo_inter] at Hmaps
Cleared hypotheses: Hmaps
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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)
have refine : ∀ y ∈ e.target ∩ e'.target,
  (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F) y = (y.1, e.coordChange e' y.1 y.2)
Tactic: refine (contMDiffOn_fst.prodMk
    (contMDiffOn_fst.coordChange contMDiffOn_snd Hmaps.1 Hmaps.2)).congr ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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)
have 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
Tactic: refine Prod.ext ?_ rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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)).1 =
    ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1
have this : ((↑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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) s x
have he₁ : (f x).proj (E := E) ∈ e.baseSet
Tactic: rw [Trivialization.mem_source] at he he'
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) s x
have he'₁ : (f x).proj (E := E) ∈ e'.baseSet
Tactic: rw [Trivialization.mem_source] at he he'
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ ((↑e' : TotalSpace F E → B × F) (f y)).2) s x
have 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
Tactic: refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ (by simp [he])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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
⊢ 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
have 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
Tactic: filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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'
⊢ 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'))
have this : MemTrivializationAtlas (E := E) e
Tactic: haveI : MemTrivializationAtlas e := ⟨he⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
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
⊢ 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'))
have this₁ : MemTrivializationAtlas (E := E) e'
Tactic: haveI : MemTrivializationAtlas e' := ⟨he'⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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'
⊢ 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'))
have 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 sorry sorry)
Tactic: rw [mem_contMDiffFiberwiseLinear_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
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 ⋯ ⋯)
have 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') sorry sorry
    sorry)
Tactic: refine ⟨_, _, e.open_baseSet.inter e'.open_baseSet, contMDiffOn_coordChangeL e e',
      contMDiffOn_symm_coordChangeL e e', ?_⟩