case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hZ : IsPreirreducible Z
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
⊢ IsIrreducible S
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hZ : IsPreirreducible Z
hU : Set.Nonempty U
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
⊢ IsIrreducible S
obtain ⟨z, hz⟩ := hU
case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
⊢ IsIrreducible S
case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hZ : IsPreirreducible Z
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
⊢ IsIrreducible S
replace hZ : IsIrreducible Z := ⟨⟨z, h₂ (h₁ hz)⟩, hZ⟩
case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
⊢ IsPreirreducible S
case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
⊢ IsIrreducible S
refine' ⟨⟨z, h₁ hz⟩, _⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ Set.Nonempty (S ∩ (u ∩ v))
case intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
⊢ IsPreirreducible S
rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ Set.Nonempty (Z ∩ ⋂₀ ↑{U, u, v})

case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
a : α
ha' : a ∈ ⋂₀ ↑{U, u, v}
⊢ Set.Nonempty (S ∩ (u ∩ v))
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ Set.Nonempty (S ∩ (u ∩ v))
obtain ⟨a, -, ha'⟩ : Set.Nonempty (Z ∩ ⋂₀ ↑({U, u, v} : Finset (Set α)))
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
a : α
ha' : a ∈ U ∧ a ∈ u ∧ a ∈ v
⊢ Set.Nonempty (S ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
a : α
ha' : a ∈ ⋂₀ ↑{U, u, v}
⊢ Set.Nonempty (S ∩ (u ∩ v))
replace ha' : a ∈ U ∧ a ∈ u ∧ a ∈ v := by simpa using ha'
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
a : α
ha' : a ∈ U ∧ a ∈ u ∧ a ∈ v
⊢ Set.Nonempty (S ∩ (u ∩ v))
exact ⟨a, h₁ ha'.1, ha'.2⟩
case refine_1
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ (u_1 : Set α), u_1 ∈ {U, u, v} → IsOpen u_1

case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ (u_1 : Set α), u_1 ∈ {U, u, v} → Set.Nonempty (Z ∩ u_1)
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ Set.Nonempty (Z ∩ ⋂₀ ↑{U, u, v})
refine isIrreducible_iff_sInter.mp hZ {U, u, v} ?_ ?_
no goals
case refine_1
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ (u_1 : Set α), u_1 ∈ {U, u, v} → IsOpen u_1
simp [*]
case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
H : U ∈ {U✝, u, v}
⊢ Set.Nonempty (Z ∩ U)
case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ (u_1 : Set α), u_1 ∈ {U, u, v} → Set.Nonempty (Z ∩ u_1)
intro U H
case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
H : U = U✝ ∨ U = u ∨ U = v
⊢ Set.Nonempty (Z ∩ U)
case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
H : U ∈ {U✝, u, v}
⊢ Set.Nonempty (Z ∩ U)
simp only [Finset.mem_insert, Finset.mem_singleton] at H
case refine_2.inl
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S Z : Set α
h₂ : S ⊆ Z
z : α
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
hU' : IsOpen U
h₁ : U ⊆ S
hz : z ∈ U
⊢ Set.Nonempty (Z ∩ U)

case refine_2.inr.inl
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
v : Set α
hv : IsOpen v
x : α
hx : x ∈ S
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
hu : IsOpen U
hx' : x ∈ U
⊢ Set.Nonempty (Z ∩ U)

case refine_2.inr.inr
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u : Set α
hu : IsOpen u
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
U : Set α
hv : IsOpen U
hy' : y ∈ U
⊢ Set.Nonempty (Z ∩ U)
case refine_2
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
H : U = U✝ ∨ U = u ∨ U = v
⊢ Set.Nonempty (Z ∩ U)
rcases H with (rfl | rfl | rfl)
no goals
case refine_2.inl
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S Z : Set α
h₂ : S ⊆ Z
z : α
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
hU' : IsOpen U
h₁ : U ⊆ S
hz : z ∈ U
⊢ Set.Nonempty (Z ∩ U)

case refine_2.inr.inl
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
v : Set α
hv : IsOpen v
x : α
hx : x ∈ S
y : α
hy : y ∈ S
hy' : y ∈ v
U : Set α
hu : IsOpen U
hx' : x ∈ U
⊢ Set.Nonempty (Z ∩ U)

case refine_2.inr.inr
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U✝ Z : Set α
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U✝
hZ : IsIrreducible Z
u : Set α
hu : IsOpen u
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
U : Set α
hv : IsOpen U
hy' : y ∈ U
⊢ Set.Nonempty (Z ∩ U)
exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
no goals
α : Type u
β : Type v
ι : Type ?u.204765
π : ι → Type ?u.204770
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U Z : Set α
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ Z
z : α
hz : z ∈ U
hZ : IsIrreducible Z
u v : Set α
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ S
hx' : x ∈ u
y : α
hy : y ∈ S
hy' : y ∈ v
a : α
ha' : a ∈ ⋂₀ ↑{U, u, v}
⊢ a ∈ U ∧ a ∈ u ∧ a ∈ v
simpa using ha'