case refine_1
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
U : Finset (Set α)
hu : ∀ (u : Set α), u ∈ U → IsOpen u
hU : ∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑U)

case refine_2
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
⊢ Set.Nonempty s

case refine_3
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
⊢ IsPreirreducible s
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
case refine_1.empty
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
hu : ∀ (u : Set α), u ∈ ∅ → IsOpen u
hU : ∀ (u : Set α), u ∈ ∅ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑∅)

case refine_1.insert
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝¹ t s : Set α
h : IsIrreducible s
a✝² : Set α
s✝ : Finset (Set α)
a✝¹ : ¬a✝² ∈ s✝
a✝ : (∀ (u : Set α), u ∈ s✝ → IsOpen u) → (∀ (u : Set α), u ∈ s✝ → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑s✝)
hu : ∀ (u : Set α), u ∈ insert a✝² s✝ → IsOpen u
hU : ∀ (u : Set α), u ∈ insert a✝² s✝ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑(insert a✝² s✝))
case refine_1
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
U : Finset (Set α)
hu : ∀ (u : Set α), u ∈ U → IsOpen u
hU : ∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑U)
induction U using Finset.induction_on
case refine_1.insert
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝¹ t s : Set α
h : IsIrreducible s
a✝² : Set α
s✝ : Finset (Set α)
a✝¹ : ¬a✝² ∈ s✝
a✝ : (∀ (u : Set α), u ∈ s✝ → IsOpen u) → (∀ (u : Set α), u ∈ s✝ → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑s✝)
hu : ∀ (u : Set α), u ∈ insert a✝² s✝ → IsOpen u
hU : ∀ (u : Set α), u ∈ insert a✝² s✝ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑(insert a✝² s✝))
case refine_1.empty
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
hu : ∀ (u : Set α), u ∈ ∅ → IsOpen u
hU : ∀ (u : Set α), u ∈ ∅ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑∅)

case refine_1.insert
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝¹ t s : Set α
h : IsIrreducible s
a✝² : Set α
s✝ : Finset (Set α)
a✝¹ : ¬a✝² ∈ s✝
a✝ : (∀ (u : Set α), u ∈ s✝ → IsOpen u) → (∀ (u : Set α), u ∈ s✝ → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑s✝)
hu : ∀ (u : Set α), u ∈ insert a✝² s✝ → IsOpen u
hU : ∀ (u : Set α), u ∈ insert a✝² s✝ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑(insert a✝² s✝))
case empty => simpa using h.nonempty
no goals
case refine_1.insert
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝¹ t s : Set α
h : IsIrreducible s
a✝² : Set α
s✝ : Finset (Set α)
a✝¹ : ¬a✝² ∈ s✝
a✝ : (∀ (u : Set α), u ∈ s✝ → IsOpen u) → (∀ (u : Set α), u ∈ s✝ → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑s✝)
hu : ∀ (u : Set α), u ∈ insert a✝² s✝ → IsOpen u
hU : ∀ (u : Set α), u ∈ insert a✝² s✝ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑(insert a✝² s✝))
case insert u U _ IH =>
  rw [Finset.coe_insert, sInter_insert]
  rw [Finset.forall_mem_insert] at hu hU
  exact h.2 _ _ hu.1 (isOpen_sInter U.finite_toSet hu.2) hU.1 (IH hu.2 hU.2)
no goals
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
hu : ∀ (u : Set α), u ∈ ∅ → IsOpen u
hU : ∀ (u : Set α), u ∈ ∅ → Set.Nonempty (s ∩ u)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑∅)
simpa using h.nonempty
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
u : Set α
U : Finset (Set α)
a✝ : ¬u ∈ U
IH : (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
hu : ∀ (u_1 : Set α), u_1 ∈ insert u U → IsOpen u_1
hU : ∀ (u_1 : Set α), u_1 ∈ insert u U → Set.Nonempty (s ∩ u_1)
⊢ Set.Nonempty (s ∩ (u ∩ ⋂₀ ↑U))
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
u : Set α
U : Finset (Set α)
a✝ : ¬u ∈ U
IH : (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
hu : ∀ (u_1 : Set α), u_1 ∈ insert u U → IsOpen u_1
hU : ∀ (u_1 : Set α), u_1 ∈ insert u U → Set.Nonempty (s ∩ u_1)
⊢ Set.Nonempty (s ∩ ⋂₀ ↑(insert u U))
rw [Finset.coe_insert, sInter_insert]
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
u : Set α
U : Finset (Set α)
a✝ : ¬u ∈ U
IH : (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
hu : IsOpen u ∧ ∀ (x : Set α), x ∈ U → IsOpen x
hU : Set.Nonempty (s ∩ u) ∧ ∀ (x : Set α), x ∈ U → Set.Nonempty (s ∩ x)
⊢ Set.Nonempty (s ∩ (u ∩ ⋂₀ ↑U))
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
u : Set α
U : Finset (Set α)
a✝ : ¬u ∈ U
IH : (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
hu : ∀ (u_1 : Set α), u_1 ∈ insert u U → IsOpen u_1
hU : ∀ (u_1 : Set α), u_1 ∈ insert u U → Set.Nonempty (s ∩ u_1)
⊢ Set.Nonempty (s ∩ (u ∩ ⋂₀ ↑U))
rw [Finset.forall_mem_insert] at hu hU
no goals
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsIrreducible s
u : Set α
U : Finset (Set α)
a✝ : ¬u ∈ U
IH : (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
hu : IsOpen u ∧ ∀ (x : Set α), x ∈ U → IsOpen x
hU : Set.Nonempty (s ∩ u) ∧ ∀ (x : Set α), x ∈ U → Set.Nonempty (s ∩ x)
⊢ Set.Nonempty (s ∩ (u ∩ ⋂₀ ↑U))
exact h.2 _ _ hu.1 (isOpen_sInter U.finite_toSet hu.2) hU.1 (IH hu.2 hU.2)
no goals
case refine_2
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
⊢ Set.Nonempty s
simpa using h ∅
case refine_3
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
u v : Set α
hu : IsOpen u
hv : IsOpen v
hu' : Set.Nonempty (s ∩ u)
hv' : Set.Nonempty (s ∩ v)
⊢ Set.Nonempty (s ∩ (u ∩ v))
case refine_3
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
⊢ IsPreirreducible s
intro u v hu hv hu' hv'
no goals
case refine_3
α : Type u
β : Type v
ι : Type ?u.192116
π : ι → Type ?u.192121
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)
u v : Set α
hu : IsOpen u
hv : IsOpen v
hu' : Set.Nonempty (s ∩ u)
hv' : Set.Nonempty (s ∩ v)
⊢ Set.Nonempty (s ∩ (u ∩ v))
simpa [*] using h {u, v}