-- Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean
theorem ContMDiffFiberwiseLinear.locality_aux₁
    (n : WithTop ℕ∞) (e : PartialHomeomorph (B × F) (B × F))
    (h : ∀ p ∈ e.source, ∃ s : Set (B × F), IsOpen s ∧ p ∈ s ∧
      ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen u)
        (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x : F →L[𝕜] F)) u)
        (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ((φ x).symm : F →L[𝕜] F)) u),
          (e.restr s).EqOnSource
            (FiberwiseLinear.partialHomeomorph φ hu hφ.continuousOn h2φ.continuousOn)) :
    ∃ U : Set B, e.source = U ×ˢ univ ∧ ∀ x ∈ U,
        ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) (_huU : u ⊆ U) (_hux : x ∈ u),
          ∃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x : F →L[𝕜] F)) u)
            (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ((φ x).symm : F →L[𝕜] F)) u),
            (e.restr (u ×ˢ univ)).EqOnSource
              (FiberwiseLinear.partialHomeomorph φ hu hφ.continuousOn h2φ.continuousOn)

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : WithTop ℕ∞
e : PartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
p : ↑e.source
⊢ e.source ∩ s p = u p ×ˢ univ

Tactic:
rw [← e.restr_source' (s _) (hs _)]

Result:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : WithTop ℕ∞
e : PartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
p : ↑e.source
⊢ (e.restr (s p)).source = u p ×ˢ univ

Proof state:
case intro.intro.refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : WithTop ℕ∞
e : PartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ
hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p
heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source
he : e.source = (Prod.fst '' e.source) ×ˢ univ
p : B × F
hp : p ∈ e.source
y : B
hy : y ∈ u ⟨p, hp⟩
⊢ y ∈ Prod.fst '' e.source

Tactic:
exact ⟨(y, 0), heu ⟨p, hp⟩ ⟨_, _⟩ hy, rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : WithTop ℕ∞
e : PartialHomeomorph (B × F) (B × F)
h :
  ∀ (x : ↑e.source),
    ∃ s,
      IsOpen s ∧
        ↑x ∈ s ∧
          ∃ φ u,
            ∃ (hu : IsOpen u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x)) u) (h2φ :
              ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x).symm) u),
              (e.restr s).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
⊢ ∃ U,
    e.source = U ×ˢ univ ∧
      ∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x)) u) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x).symm) u),
            (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)

Tactic:
choose s hs hsp φ u hu hφ h2φ heφ using h

Result:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : WithTop ℕ∞
e : PartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
⊢ ∃ U,
    e.source = U ×ˢ univ ∧
      ∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x)) u) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x).symm) u),
            (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)