case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
⊢ IsPreirreducible (f ⁻¹' Z)
rintro U V hU hV ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
z : β
h₂ : z ∈ U
h₁ : f z ∈ Z
z' : β
h₃ : z' ∈ V
h₄ : f z' = f z
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
obtain ⟨_, h₁, ⟨z, h₂, rfl⟩, ⟨z', h₃, h₄⟩⟩ :=
  hZ _ _ (hf.isOpenMap _ hU) (hf.isOpenMap _ hV) ⟨f x, hx, Set.mem_image_of_mem f hx'⟩
    ⟨f y, hy, Set.mem_image_of_mem f hy'⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
z : β
h₂ : z ∈ U
h₁ : f z ∈ Z
h₃ : z ∈ V
h₄ : f z = f z
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
z : β
h₂ : z ∈ U
h₁ : f z ∈ Z
z' : β
h₃ : z' ∈ V
h₄ : f z' = f z
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
cases hf.inj h₄
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u
β : Type v
ι : Type ?u.209716
π : ι → Type ?u.209721
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z : Set α
hZ : IsPreirreducible Z
f : β → α
hf : OpenEmbedding f
U V : Set β
hU : IsOpen U
hV : IsOpen V
x : β
hx : x ∈ f ⁻¹' Z
hx' : x ∈ U
y : β
hy : y ∈ f ⁻¹' Z
hy' : y ∈ V
z : β
h₂ : z ∈ U
h₁ : f z ∈ Z
h₃ : z ∈ V
h₄ : f z = f z
⊢ Set.Nonempty (f ⁻¹' Z ∩ (U ∩ V))
exact ⟨z, h₁, h₂, h₃⟩