awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsClosed[inst] (irreducibleComponent x)

Tactic:
isClosed_of_mem_irreducibleComponents _ (irreducibleComponent_mem_irreducibleComponents x)

Premises used: isClosed_of_mem_irreducibleComponents, irreducibleComponent_mem_irreducibleComponents
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : IrreducibleSpace X
⊢ IsIrreducible.{u_3} (X := X) univ

Tactic:
⟨univ_nonempty, PreirreducibleSpace.isPreirreducible_univ⟩

Premises used: IsIrreducible, PreirreducibleSpace.isPreirreducible_univ, Set.univ_nonempty, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ IrreducibleSpace X ↔ IsIrreducible.{u_3} (X := X) ⊤

Tactic:
⟨@IrreducibleSpace.isIrreducible_univ X _, fun h =>
    haveI : PreirreducibleSpace X := ⟨h.2⟩
    ⟨⟨h.1.some⟩⟩⟩

Premises used: IrreducibleSpace.isIrreducible_univ, Nonempty.intro, And.left, Iff.intro, IrreducibleSpace.mk, Set.Nonempty.some
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ ⦃U V : Set X⦄, IsOpen[inst] U → IsOpen[inst] V → U.Nonempty → V.Nonempty → (U ∩ V).Nonempty
x : Set X
⊢ ∀ (v : Set X), IsOpen[inst] x → IsOpen[inst] v → (univ ∩ x).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (x ∩ v)).Nonempty

Tactic:
simp_all
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : PreirreducibleSpace X
⊢ IsOpen[inst] s → IsOpen[inst] t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using
    @PreirreducibleSpace.isPreirreducible_univ X _ _ s t

Premises used: Set.univ_subset_iff, PreirreducibleSpace.isPreirreducible_univ, Set.univ_inter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace X
ho : IsOpen[inst] s
hne : s.Nonempty
⊢ Dense s

Tactic:
dense_iff_inter_open.2 fun _t hto htne => nonempty_preirreducible_inter hto ho htne hne

Premises used: Iff.mpr, dense_iff_inter_open, nonempty_preirreducible_inter
-- Module: Mathlib.Topology.Irreducible
Goal:
U : Type u_3
X : Type u_4
inst : TopologicalSpace U
inst_1 : Nonempty U
inst_2 : TopologicalSpace X
f : U → X
hf : IsOpenMap f
inst_3 : PreirreducibleSpace X
⊢ DenseRange f

Tactic:
hf.isOpen_range.dense (Set.range_nonempty f)

Premises used: IsOpen.dense, Set.range_nonempty, DenseRange, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : f x ∈ u
y : X
hy : y ∈ s
hyv : f y ∈ v
rw : ∀ (hxu : x ∈ f ⁻¹' u) (y : X) (hy : y ∈ s) (hyv : y ∈ f ⁻¹' v), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rw [← mem_preimage] at hxu hyv

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
rcases : ∀ (u' : Set X) (hu' : IsOpen[inst] u') (u'_eq : f ⁻¹' u ∩ s = u' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
rcases : ∀ (v' : Set X) (hv' : IsOpen[inst] v') (v'_eq : f ⁻¹' v ∩ s = v' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ (s ∩ u').Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty

Tactic:
have := H u' v' hu' hv'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (s ∩ u').Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty

Tactic:
rw [inter_comm s u', ← u'_eq] at this

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty

Tactic:
rw [inter_comm s v', ← v'_eq] at this

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
rcases : ∀ (x : X) (hxs : x ∈ s) (hxu' : x ∈ u') (hxv' : x ∈ v'), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩

Premises used: Set.Nonempty, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_1 : f x ∈ u
refine_2 : f x ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_1 : x ∈ f ⁻¹' u
⊢ f x ∈ u

Tactic:
rw [← mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_1 : x ∈ f ⁻¹' u ∩ s
refine_1₁ : Set X
⊢ x ∈ f ⁻¹' u

Tactic:
apply mem_of_mem_inter_left

Premises used: Set.mem_of_mem_inter_left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' u ∩ s

Tactic:
simp [*]
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_2 : x ∈ f ⁻¹' v
⊢ f x ∈ v

Tactic:
rw [← mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_2 : x ∈ f ⁻¹' v ∩ s
refine_2₁ : Set X
⊢ x ∈ f ⁻¹' v

Tactic:
apply mem_of_mem_inter_left

Premises used: Set.mem_of_mem_inter_left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' v ∩ s

Tactic:
simp [*]
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsIrreducible s
f : X → Y
hf : ContinuousOn f s
⊢ IsIrreducible (f '' s)

Tactic:
⟨H.nonempty.image _, H.isPreirreducible.image f hf⟩

Premises used: IsPreirreducible.image, IsIrreducible, IsIrreducible.nonempty, Set.Nonempty.image, IsIrreducible.isPreirreducible, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst] u
v : Set X
hv : IsOpen[inst] v
x : X
hxs : x ∈ s
hxu :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u) (mk (p := fun (x : X) ↦ x ∈ s) x hxs)
y : X
hys : y ∈ s
hyv :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v) (mk (p := fun (x : X) ↦ x ∈ s) y hys)
rcases :
  ∀ (x : X) (hxs : x ∈ s) (hxu : x ∈ u) (hxv : x ∈ v),
    Set.Nonempty (α := (↑s : Type u_1))
      (univ ∩ (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ∩ val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v))
⊢ Set.Nonempty (α := (↑s : Type u_1))
    (univ ∩ (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ∩ val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v))

Tactic:
rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst] u
v : Set X
hv : IsOpen[inst] v
x_1 : X
hxs_1 : x_1 ∈ s
hxu_1 :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
    (mk (p := fun (x : X) ↦ x ∈ s) x_1 hxs_1)
y : X
hys : y ∈ s
hyv :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v) (mk (p := fun (x : X) ↦ x ∈ s) y hys)
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ Set.Nonempty (α := (↑s : Type u_1))
    (univ ∩ (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ∩ val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v))

Tactic:
⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩

Premises used: Subtype.mk, Set.Nonempty, And.intro, Exists.intro, Set.mem_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst] u
v : Set X
hv : IsOpen[inst] v
x_1 : X
hxs_1 : x_1 ∈ s
hxu_1 :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
    (mk (p := fun (x : X) ↦ x ∈ s) x_1 hxs_1)
y : X
hys : y ∈ s
hyv :
  Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v) (mk (p := fun (x : X) ↦ x ∈ s) y hys)
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ Set.Nonempty (α := (↑s : Type u_1))
    (univ ∩ (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ∩ val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v))

Tactic:
exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
rw : IsPreirreducible.{u_1} (X := X) (Set.image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
⊢ IsPreirreducible s

Tactic:
rw [← Subtype.range_coe (s := s), ← Set.image_univ]

Premises used: Set.image_univ, Subtype.range_coe
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
⊢ IsPreirreducible.{u_1} (X := X) (Set.image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)

Tactic:
PreirreducibleSpace.isPreirreducible_univ.image Subtype.val ?_

Premises used: IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ, Subtype.val
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
refine : ContinuousOn.{u_1, u_1} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ
⊢ IsPreirreducible.{u_1} (X := X) (Set.image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)

Tactic:
refine PreirreducibleSpace.isPreirreducible_univ.image Subtype.val ?_

Premises used: IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ, Subtype.val
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
⊢ ContinuousOn.{u_1, u_1} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ

Tactic:
continuous_subtype_val.continuousOn

Premises used: Continuous.continuousOn, continuous_subtype_val
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
⊢ ContinuousOn.{u_1, u_1} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ

Tactic:
exact continuous_subtype_val.continuousOn

Premises used: Continuous.continuousOn, continuous_subtype_val
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : IrreducibleSpace.{u_1} (↑s : Type u_1)
⊢ IsIrreducible s

Tactic:
⟨.of_subtype, .of_subtype⟩

Premises used: IsPreirreducible.of_subtype, Set.Nonempty.of_subtype, IsIrreducible, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : IrreducibleSpace.{u_1} (↑s : Type u_1)
⊢ IsIrreducible s

Tactic:
exact ⟨.of_subtype, .of_subtype⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ PreirreducibleSpace.{u_1} (↑s : Type u_1)

Tactic:
⟨Subtype.preirreducibleSpace, fun _ ↦ .of_subtype⟩

Premises used: IsPreirreducible.of_subtype, Iff.intro, Subtype.preirreducibleSpace
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔ IrreducibleSpace.{u_1} (↑s : Type u_1)

Tactic:
⟨Subtype.irreducibleSpace, fun _ ↦ .of_subtype⟩

Premises used: Subtype.irreducibleSpace, IsIrreducible.of_subtype, Iff.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : Subsingleton X
⊢ PreirreducibleSpace X

Tactic:
⟨(Set.subsingleton_univ_iff.mpr ‹_›).isPreirreducible⟩

Premises used: Iff.mpr, Set.subsingleton_univ_iff, PreirreducibleSpace.mk, Set.Subsingleton.isPreirreducible
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : IndiscreteTopology X
u v : Set X
simp : u = ∅ ∨ u = univ → v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
⊢ IsOpen[inst] u → IsOpen[inst] v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [IndiscreteTopology.isOpen_iff, univ_inter]

Premises used: IndiscreteTopology.isOpen_iff, Set.univ_inter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : IndiscreteTopology X
v : Set X
⊢ v = ∅ ∨ v = univ → Set.Nonempty.{u_1} (α := X) ∅ → v.Nonempty → (∅ ∩ v).Nonempty

Tactic:
simp_all
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : IndiscreteTopology X
u v : Set X
h : u = univ
⊢ v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
simp_all
-- Module: Mathlib.Topology.Irreducible
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : Type u_3
inst_2 : Infinite X
u v : Set (CofiniteTopology X)
simp : (u.Nonempty → uᶜ.Finite) → (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
⊢ IsOpen u → IsOpen v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [CofiniteTopology.isOpen_iff, univ_inter]

Premises used: Set.univ_inter, CofiniteTopology.isOpen_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : Type u_3
inst_2 : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
hv' : v.Nonempty
⊢ (u ∩ v).Nonempty

Tactic:
simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty

Premises used: Set.Finite.union, Set.compl_union, compl_compl, Set.Infinite.nonempty, Set.Finite.infinite_compl
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IrreducibleSpace X
⊢ irreducibleComponents X = {univ}

Tactic:
Set.ext fun _ ↦ IsGreatest.maximal_iff (s := {s : Set X | IsIrreducible s})
    ⟨IrreducibleSpace.isIrreducible_univ X, fun _ _ ↦ Set.subset_univ _⟩

Premises used: Set.ext, Set.subset_univ, IrreducibleSpace.isIrreducible_univ, And.intro, IsGreatest.maximal_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty

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

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (h : IsIrreducible s) (U : Finset (Set X)) (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty),
    (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
refine_2 :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    s.Nonempty
refine_3 :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    IsPreirreducible s
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty

Tactic:
refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
hu : ∀ (u : Set X), Membership.mem (γ := Finset (Set X)) ∅ u → IsOpen[inst] u
hU : ∀ (u : Set X), Membership.mem (γ := Finset (Set X)) ∅ u → (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ (↑∅ : Set (Set X))).Nonempty

Tactic:
simpa using h.nonempty

Premises used: IsIrreducible.nonempty
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
h_1 : u ∉ U
IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
refine_1 : (s ∩ (u ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty
⊢ (s ∩ ⋂₀ (↑(insert u U) : Set (Set X))).Nonempty

Tactic:
rw [Finset.coe_insert, sInter_insert]

Premises used: Set.sInter_insert, Finset.coe_insert
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
h_1 : u ∉ U
IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x

Tactic:
rw [Finset.forall_mem_insert] at hu hU

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
h_1 : u ∉ U
IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
hu₁ : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
⊢ (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty

Tactic:
rw [Finset.forall_mem_insert] at hu hU

Premises used: Finset.forall_mem_insert