-- Mathlib/Topology/Irreducible.lean
theorem isIrreducible_iff_sInter :
    IsIrreducible s ↔
      ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) →
        (s ∩ ⋂₀ ↑U).Nonempty

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
U : Finset (Set X)
hu : ∀ u ∈ U, IsOpen u
hU : ∀ u ∈ U, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑U).Nonempty

Tactic:
induction U using Finset.induction_on with
| empty => simpa using h.nonempty
| @insert u U _ IH =>
  rw [Finset.coe_insert, sInter_insert]
  rw [Finset.forall_mem_insert] at hu hU
  exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

Result:
no goals

Proof state:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty

Tactic:
rw [Finset.forall_mem_insert] at hu hU

Result:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : IsOpen u ∧ ∀ x ∈ U, IsOpen x
hU : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty

Proof state:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen u
hv : IsOpen v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
simpa [*] using h {u, v}

Result:
no goals

Proof state:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ IsPreirreducible s

Tactic:
intro u v hu hv hu' hv'

Result:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen u
hv : IsOpen v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ ⋂₀ ↑(insert u U)).Nonempty

Tactic:
rw [Finset.coe_insert, sInter_insert]

Result:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ s.Nonempty

Tactic:
simpa using h ∅

Result:
no goals

Proof state:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : IsOpen u ∧ ∀ x ∈ U, IsOpen x
hU : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty

Tactic:
exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔ ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty

Tactic:
refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
U : Finset (Set X)
hu : ∀ u ∈ U, IsOpen u
hU : ∀ u ∈ U, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑U).Nonempty

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ s.Nonempty

case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ IsPreirreducible s

Proof state:
case refine_1.empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
hu : ∀ u ∈ ∅, IsOpen u
hU : ∀ u ∈ ∅, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑∅).Nonempty

Tactic:
simpa using h.nonempty

Result:
no goals