case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
⊢ (x, y) ∈ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
s : Set B
⊢ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ
ext ⟨x, y⟩
case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
⊢ x ∈ e.baseSet → (proj (↑(LocalEquiv.symm e.toLocalEquiv) (x, y)) ∈ s ↔ x ∈ s)
case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
⊢ (x, y) ∈ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ
suffices x ∈ e.baseSet → (proj (e.toLocalEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
  simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true_iff, mem_univ, and_congr_left_iff]
case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj (↑(LocalEquiv.symm e.toLocalEquiv) (x, y)) ∈ s ↔ x ∈ s
case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
⊢ x ∈ e.baseSet → (proj (↑(LocalEquiv.symm e.toLocalEquiv) (x, y)) ∈ s ↔ x ∈ s)
intro h
no goals
case h.mk
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj (↑(LocalEquiv.symm e.toLocalEquiv) (x, y)) ∈ s ↔ x ∈ s
rw [e.proj_symm_apply' h]
no goals
ι : Type ?u.9734
B : Type u_1
F : Type u_2
E : B → Type ?u.9745
Z : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x✝ : Z
s : Set B
x : B
y : F
this : x ∈ e.baseSet → (proj (↑(LocalEquiv.symm e.toLocalEquiv) (x, y)) ∈ s ↔ x ∈ s)
⊢ (x, y) ∈ ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ
simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true_iff, mem_univ, and_congr_left_iff]