case left
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source =
    (trivChange Z i j).toLocalEquiv.source

case right
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ EqOn (↑(LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)))
    (↑(trivChange Z i j).toLocalEquiv)
    (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j) ≈
    (trivChange Z i j).toLocalEquiv
constructor
case left.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x ∈ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source ↔
    x ∈ (trivChange Z i j).toLocalEquiv.source
case left
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source =
    (trivChange Z i j).toLocalEquiv.source
ext x
case left.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x.fst ∈ baseSet Z i ∧ ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) x ∈ (localTrivAsLocalEquiv Z j).source ↔
    x.fst ∈ baseSet Z i ∧ x.fst ∈ baseSet Z j
case left.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x ∈ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source ↔
    x ∈ (trivChange Z i j).toLocalEquiv.source
simp only [mem_localTrivAsLocalEquiv_target, mfld_simps]
no goals
case left.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x.fst ∈ baseSet Z i ∧ ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) x ∈ (localTrivAsLocalEquiv Z j).source ↔
    x.fst ∈ baseSet Z i ∧ x.fst ∈ baseSet Z j
rfl
case right.mk
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B
v : F
hx : (x, v) ∈ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source
⊢ ↑(LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)) (x, v) =
    ↑(trivChange Z i j).toLocalEquiv (x, v)
case right
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ EqOn (↑(LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)))
    (↑(trivChange Z i j).toLocalEquiv)
    (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source
rintro ⟨x, v⟩ hx
no goals
case right.mk
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32818
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ coordChange Z (indexAt Z x) j x (coordChange Z i (indexAt Z x) x v) = coordChange Z i j x v
simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]