-- Mathlib/Topology/Irreducible.lean
theorem IsPreirreducible.subset_irreducible {S U : Set X} (ht : IsPreirreducible t)
    (hU : U.Nonempty) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ t) : IsIrreducible S

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsPreirreducible S

Tactic:
rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U ∈ {U✝, u, v}
⊢ (t ∩ U).Nonempty

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at H

Result:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U = U✝ ∨ U = u ∨ U = v
⊢ (t ∩ U).Nonempty

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsIrreducible S

Tactic:
refine ⟨⟨z, h₁ hz⟩, ?_⟩

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsPreirreducible S

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, (t ∩ u_1).Nonempty

Tactic:
intro U H

Result:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U ∈ {U✝, u, v}
⊢ (t ∩ U).Nonempty

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU : U.Nonempty
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
⊢ IsIrreducible S

Tactic:
obtain ⟨z, hz⟩ := hU

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
⊢ IsIrreducible S

Proof state:
case refine_2.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S : Set X
h₂ : S ⊆ t
z : X
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
hz : z ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
v : Set X
hv : IsOpen v
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hu : IsOpen U
hx' : x ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inr
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u : Set X
hu : IsOpen u
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
U : Set X
hv : IsOpen U
hy' : y ∈ U
⊢ (t ∩ U).Nonempty

Tactic:
exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ (t ∩ ⋂₀ ↑{U, u, v}).Nonempty

Tactic:
refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, IsOpen u_1

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, (t ∩ u_1).Nonempty

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ ↑{U, u, v}
⊢ x ∈ U ∧ x ∈ u ∧ x ∈ v

Tactic:
simpa using hx'

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ ↑{U, u, v}
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, IsOpen u_1

Tactic:
simp [*]

Result:
no goals

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U = U✝ ∨ U = u ∨ U = v
⊢ (t ∩ U).Nonempty

Tactic:
rcases H with (rfl | rfl | rfl)

Result:
case refine_2.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S : Set X
h₂ : S ⊆ t
z : X
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
hz : z ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inl
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
v : Set X
hv : IsOpen v
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hu : IsOpen U
hx' : x ∈ U
⊢ (t ∩ U).Nonempty

case refine_2.inr.inr
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u : Set X
hu : IsOpen u
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
U : Set X
hv : IsOpen U
hy' : y ∈ U
⊢ (t ∩ U).Nonempty

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
⊢ IsIrreducible S

Tactic:
replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsIrreducible S