-- Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean
theorem ContMDiffFiberwiseLinear.locality_aux₂
    (n : WithTop ℕ∞) (e : PartialHomeomorph (B × F) (B × F)) (U : Set B) (hU : e.source = U ×ˢ univ)
    (h : ∀ 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)) :
    ∃ (Φ : 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.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)
U : Set B
hU : e.source = U ×ˢ univ
h :
  ∀ 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 ⋯ ⋯)
⊢ ∃ Φ 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.EqOnSource (FiberwiseLinear.partialHomeomorph Φ hU₀ ⋯ ⋯)

Tactic:
classical
rw [SetCoe.forall'] at h
choose! φ u hu hUu hux hφ h2φ heφ using h
have heuφ : ∀ x : U, EqOn e (fun q => (q.1, φ x q.1 q.2)) (u x ×ˢ univ) := fun x p hp ↦ by
  refine (heφ x).2 ?_
  rw [(heφ x).1]
  exact hp
have huφ : ∀ (x x' : U) (y : B), y ∈ u x → y ∈ u x' → φ x y = φ x' y := fun p p' y hyp hyp' ↦ by
  ext v
  have h1 : e (y, v) = (y, φ p y v) := heuφ _ ⟨(id hyp : (y, v).fst ∈ u p), trivial⟩
  have h2 : e (y, v) = (y, φ p' y v) := heuφ _ ⟨(id hyp' : (y, v).fst ∈ u p'), trivial⟩
  exact congr_arg Prod.snd (h1.symm.trans h2)
have hUu' : U = ⋃ i, u i := by
  ext x
  rw [mem_iUnion]
  refine ⟨fun h => ⟨⟨x, h⟩, hux _⟩, ?_⟩
  rintro ⟨x, hx⟩
  exact hUu x hx
have hU' : IsOpen U := by
  rw [hUu']
  apply isOpen_iUnion hu
let Φ₀ : U → F ≃L[𝕜] F := iUnionLift u (fun x => φ x ∘ (↑)) huφ U hUu'.le
let Φ : B → F ≃L[𝕜] F := fun y =>
  if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
have hΦ : ∀ (y) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩ := fun y hy => dif_pos hy
have hΦφ : ∀ x : U, ∀ y ∈ u x, Φ y = φ x y := by
  intro x y hyu
  refine (hΦ y (hUu x hyu)).trans ?_
  exact iUnionLift_mk ⟨y, hyu⟩ _
have hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => (Φ y : F →L[𝕜] F)) U := by
  apply contMDiffOn_of_locally_contMDiffOn
  intro x hx
  refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
  refine (ContMDiffOn.congr (hφ ⟨x, hx⟩) ?_).mono inter_subset_right
  intro y hy
  rw [hΦφ ⟨x, hx⟩ y hy]
have h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ((Φ y).symm : F →L[𝕜] F)) U := by
  apply contMDiffOn_of_locally_contMDiffOn
  intro x hx
  refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
  refine (ContMDiffOn.congr (h2φ ⟨x, hx⟩) ?_).mono inter_subset_right
  intro y hy
  rw [hΦφ ⟨x, hx⟩ y hy]
refine ⟨Φ, U, hU', hΦ, h2Φ, hU, fun p hp => ?_⟩
rw [hU] at hp
rw [heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.2⟩]
congrm (_, ?_)
rw [hΦφ]
apply hux

Result:
no goals

Proof state:
case h.h
𝕜 : 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)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q => (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
p p' : ↑U
y : B
hyp : y ∈ u p
hyp' : y ∈ u p'
v : F
h1 : ↑e (y, v) = (y, (φ p y) v)
h2 : ↑e (y, v) = (y, (φ p' y) v)
⊢ (φ p y) v = (φ p' y) v

Tactic:
exact congr_arg Prod.snd (h1.symm.trans h2)

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)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q => (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x => φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y => if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ✝ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
hΦφ : ∀ (x : ↑U), ∀ y ∈ u x, Φ y = φ x y
hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ↑(Φ y)) U
h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ↑(Φ y).symm) U
p : B × F
hp : p ∈ e.source
⊢ ↑e p = ↑(FiberwiseLinear.partialHomeomorph Φ hU' ⋯ ⋯) p

Tactic:
rw [hU] at hp

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)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 => ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q => (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x => φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y => if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ✝ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
hΦφ : ∀ (x : ↑U), ∀ y ∈ u x, Φ y = φ x y
hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ↑(Φ y)) U
h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ↑(Φ y).symm) U
p : B × F
hp : p ∈ U ×ˢ univ
⊢ ↑e p = ↑(FiberwiseLinear.partialHomeomorph Φ hU' ⋯ ⋯) p