Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).1 =
    (Prod.map Subtype.val id x).1

pp: case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).2 =
    (Prod.map Subtype.val id x).2

Tactic:
<;>

Goal state after:
case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).1 =
    (Prod.map Subtype.val id x).1

case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).2 =
    (Prod.map Subtype.val id x).2