awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ 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') ⋯
      ⋯ ⋯)
have refine_1 : (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') sorry sorry
      sorry).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: refine OpenPartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩
-- 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
⊢ IsManifold (IB.prod 𝓘(𝕜, F)) n (TotalSpace F E)
have refine : ∀ (e : OpenPartialHomeomorph (B × F) (B × F)),
  Membership.mem (γ := StructureGroupoid (B × F)) (contMDiffFiberwiseLinear B F IB n) e →
    ChartedSpace.LiftPropOn (StructureGroupoid.IsLocalStructomorphWithinAt (contDiffGroupoid n (IB.prod 𝓘(𝕜, F))))
      (↑e : B × F → B × F) e.source
Tactic: refine { StructureGroupoid.HasGroupoid.comp (contMDiffFiberwiseLinear B F IB n) ?_ with }
-- 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 : OpenPartialHomeomorph (B × F) (B × F)
he : Membership.mem (γ := StructureGroupoid (B × F)) (contMDiffFiberwiseLinear B F IB n) e
⊢ ChartedSpace.LiftPropOn (StructureGroupoid.IsLocalStructomorphWithinAt (contDiffGroupoid n (IB.prod 𝓘(𝕜, F))))
    (↑e : B × F → B × F) e.source
have he₁ : ∃ (φ : 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),
  e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry)
Tactic: rw [mem_contMDiffFiberwiseLinear_iff] at he
Cleared hypotheses: 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 : OpenPartialHomeomorph (B × F) (B × F)
he :
  ∃ (φ : 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),
    e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ChartedSpace.LiftPropOn (StructureGroupoid.IsLocalStructomorphWithinAt (contDiffGroupoid n (IB.prod 𝓘(𝕜, F))))
    (↑e : B × F → B × F) e.source
have obtain : ∀ (φ : 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)
  (heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry)),
  ChartedSpace.LiftPropOn (StructureGroupoid.IsLocalStructomorphWithinAt (contDiffGroupoid n (IB.prod 𝓘(𝕜, F))))
    (↑e : B × F → B × F) e.source
Tactic: obtain ⟨φ, U, hU, hφ, h2φ, heφ⟩ := he
Cleared hypotheses: 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ChartedSpace.LiftPropOn (StructureGroupoid.IsLocalStructomorphWithinAt (contDiffGroupoid n (IB.prod 𝓘(𝕜, F))))
    (↑e : B × F → B × F) e.source
have rw : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : B × F → B × F) e.source ∧
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm : B × F → B × F) e.target
Tactic: rw [isLocalStructomorphOn_contDiffGroupoid_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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : B × F → B × F) e.source ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm : B × F → B × F) e.target
have refine_1 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
  (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry) : B × F → B × F) e.source
Tactic: refine ⟨ContMDiffOn.congr ?_ (EqOnSource.eqOn heφ),
      ContMDiffOn.congr ?_ (EqOnSource.eqOn (EqOnSource.symm' 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
refine_1 :
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯) : B × F → B × F) e.source
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : B × F → B × F) e.source ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm : B × F → B × F) e.target
have refine_2 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
  (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).symm : B × F → B × F) e.target
Tactic: refine ⟨ContMDiffOn.congr ?_ (EqOnSource.eqOn heφ),
      ContMDiffOn.congr ?_ (EqOnSource.eqOn (EqOnSource.symm' 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯) : B × F → B × F) e.source
have refine_1 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
  (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry) : B × F → B × F)
  (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).source
Tactic: rw [EqOnSource.source_eq 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯) : B × F → B × F)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).source
have refine_1 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ (φ x.1 : (a : F) → F) x.2)
  (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).source
Tactic: apply contMDiffOn_fst.prodMk
-- 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).symm : B × F → B × F) e.target
have refine_2 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
  (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).symm : B × F → B × F)
  (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).target
Tactic: rw [EqOnSource.target_eq 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 : OpenPartialHomeomorph (B × F) (B × F)
φ : 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
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).symm : B × F → B × F)
    (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU ⋯ ⋯).target
have refine_2 : ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n (fun (x : B × F) ↦ ((φ x.1).symm : (a : F) → F) x.2)
  (FiberwiseLinear.openPartialHomeomorph (U := U) φ hU sorry sorry).target
Tactic: apply contMDiffOn_fst.prodMk
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
⊢ ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔
    ContMDiffOn.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s ∧
      ContMDiffOn IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s
have simp : (∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔
  ∀ (x : M) (x_1 : x ∈ s),
    ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) s x
Tactic: simp only [ContMDiffOn, ← forall_and]
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : TotalSpace F E → B × F) e.source
have this : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source
Tactic: have : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source := contMDiffOn_id