-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : Prod.{u_1, u_2} { x : B // x ∈ s } F
hx : x ∈ e.target
fst :
  ((↑((↑e : Z → (↑s : Type u_1) × F)
                (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
                  e.invFun
                    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                      (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
                else
                  Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).1 :
          B),
        ((↑e : Z → (↑s : Type u_1) × F)
            (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
              e.invFun
                (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                  (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
            else
              Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).2).1 =
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
snd :
  ((↑((↑e : Z → (↑s : Type u_1) × F)
                (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
                  e.invFun
                    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                      (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
                else
                  Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).1 :
          B),
        ((↑e : Z → (↑s : Type u_1) × F)
            (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
              e.invFun
                (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                  (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
            else
              Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).2).2 =
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2
⊢ ((↑((↑e : Z → (↑s : Type u_1) × F)
              (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
                e.invFun
                  (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
              else
                Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                  (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).1 :
        B),
      ((↑e : Z → (↑s : Type u_1) × F)
          (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
            e.invFun
              (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
          else
            Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
              (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x

Tactic:
ext