awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
⟨ht.1.preimage_of_isPreirreducible_fiber f hf₂ hf₃ h, fun u hu htu ↦ image_subset_iff.mp
    (subset_closure.trans (ht.2 (hu.image f hf₁.continuousOn).closure ?_))⟩

Premises used: irreducibleComponents, Continuous.continuousOn, Set.Mem, subset_closure, setOf, HasSubset.Subset.trans, IsIrreducible.image, IsIrreducible.closure, And.right, And.left, And.intro, IsIrreducible.preimage_of_isPreirreducible_fiber, Iff.mp, Maximal, Set.image_subset_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
refine : ∀ (u : Set Y) (hu : IsIrreducible u) (htu : f ⁻¹' t ≤ u), t ≤ closure[inst] (f '' u)
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
refine ⟨ht.1.preimage_of_isPreirreducible_fiber f hf₂ hf₃ h, fun u hu htu ↦ image_subset_iff.mp
    (subset_closure.trans (ht.2 (hu.image f hf₁.continuousOn).closure ?_))⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ≤ u
suffices : t ≤ closure[inst] (f '' f ⁻¹' t)
⊢ t ≤ closure[inst] (f '' u)

Tactic:
suffices t ≤ closure (f '' f ⁻¹' t) from this.trans (closure_mono (image_mono htu))
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ≤ u
rw : t ≤ closure[inst] (t ∩ range f)
⊢ t ≤ closure[inst] (f '' f ⁻¹' t)

Tactic:
rw [image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ≤ u
⊢ t ≤ closure[inst] (t ∩ range f)

Tactic:
subset_closure_inter_of_isPreirreducible_of_isOpen ht.1.2 hf₂.isOpen_range h

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, And.right, And.left, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst_1, inst] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ≤ u
⊢ t ≤ closure[inst] (t ∩ range f)

Tactic:
exact subset_closure_inter_of_isPreirreducible_of_isOpen ht.1.2 hf₂.isOpen_range h

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, And.right, And.left, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
preimage_mem_irreducibleComponents_of_isPreirreducible_fiber ht hf.continuous hf.isOpenMap
    (fun _ ↦ (subsingleton_singleton.preimage hf.injective).isPreirreducible) h

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.continuous, Set.subsingleton_singleton, preimage_mem_irreducibleComponents_of_isPreirreducible_fiber, Topology.IsEmbedding.injective, Set.Subsingleton.isPreirreducible, Set.Subsingleton.preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
refine preimage_mem_irreducibleComponents_of_isPreirreducible_fiber ht hf.continuous hf.isOpenMap
    (fun _ ↦ (subsingleton_singleton.preimage hf.injective).isPreirreducible) h

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.continuous, Set.subsingleton_singleton, preimage_mem_irreducibleComponents_of_isPreirreducible_fiber, Topology.IsEmbedding.injective, Set.Subsingleton.isPreirreducible, Set.Subsingleton.preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
⊢ f '' f ⁻¹' s ⊆ s

Tactic:
simp
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
refine : s ⊆ closure[inst] (f '' f ⁻¹' s)
⊢ closure[inst] (f '' f ⁻¹' s) = s

Tactic:
refine subset_antisymm (closure_minimal (by simp) hs') ?_

Premises used: closure_minimal, subset_antisymm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
⊢ s ⊆ closure[inst] (f '' f ⁻¹' s)

Tactic:
subset_trans (subset_closure_inter_of_isPreirreducible_of_isOpen hs h.isOpen_range ?_) ?_

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, subset_trans, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
refine_1 : (s ∩ range f).Nonempty
refine_2 : closure[inst] (s ∩ range f) ⊆ closure[inst] (f '' f ⁻¹' s)
⊢ s ⊆ closure[inst] (f '' f ⁻¹' s)

Tactic:
refine subset_trans (subset_closure_inter_of_isPreirreducible_of_isOpen hs h.isOpen_range ?_) ?_

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, subset_trans, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
⊢ (f ⁻¹' (s ∩ range f)).Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
⊢ (s ∩ range f).Nonempty

Tactic:
exact Set.nonempty_of_nonempty_preimage (f := f) (by simpa)

Premises used: Set.nonempty_of_nonempty_preimage
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
refine_2 : s ∩ range f ⊆ f '' f ⁻¹' s
⊢ closure[inst] (s ∩ range f) ⊆ closure[inst] (f '' f ⁻¹' s)

Tactic:
gcongr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst] s
⊢ s ∩ range f ⊆ f '' f ⁻¹' s

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
obtain : ∀ (x : X) (hx : x ∈ V), (f ⁻¹' Z).Nonempty
⊢ (f ⁻¹' Z).Nonempty

Tactic:
obtain ⟨x, hx⟩ := hV.1.1

Premises used: And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty

Tactic:
⟨x, hWZ ⟨x, hx, rfl⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty

Tactic:
exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
⊢ f ⁻¹' Z ≤ V

Tactic:
have := hV.2 ⟨(by obtain ⟨x, hx⟩ := hV.1.1; exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩),
      hZ.2.preimage_of_isPreirreducible_fiber f hf₂ hf₃⟩ (Set.image_subset_iff.mp hWZ)
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
this : f ⁻¹' Z ≤ V
rw : f '' f ⁻¹' Z ≤ f '' V
⊢ Z ≤ f '' V

Tactic:
rw [← Set.image_preimage_eq Z hf₄]

Premises used: Set.image_preimage_eq
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
this : f ⁻¹' Z ≤ V
⊢ f '' f ⁻¹' Z ≤ f '' V

Tactic:
Set.image_mono this

Premises used: Set.image_mono
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ≤ Z
this : f ⁻¹' Z ≤ V
⊢ f '' f ⁻¹' Z ≤ f '' V

Tactic:
exact Set.image_mono this

Premises used: Set.image_mono
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents Y) : Type u_2)
⊢ ((↑W : Set Y) ∩ range f).Nonempty

Tactic:
simp [hf₄.range_eq, W.2.1.1]

Premises used: Function.Surjective.range_eq, And.left, Subtype.property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
⊢ (↑((fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
            Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯)
          ((fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
              Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯)
            W)) :
      Set X) =
    (↑W : Set X)

Tactic:
(Set.subset_preimage_image _ _).antisymm' (W.2.2 ?_ (Set.subset_preimage_image _ _))

Premises used: Set.Mem, setOf, And.right, Set.preimage, Set.image, HasSubset.Subset.antisymm', Set.subset_preimage_image, Subtype.property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
refine : IsIrreducible (f ⁻¹' f '' (↑W : Set X))
⊢ (↑((fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
            Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯)
          ((fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
              Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯)
            W)) :
      Set X) =
    (↑W : Set X)

Tactic:
refine (Set.subset_preimage_image _ _).antisymm' (W.2.2 ?_ (Set.subset_preimage_image _ _))

Premises used: And.right, HasSubset.Subset.antisymm', Set.subset_preimage_image, Subtype.property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
⊢ IsIrreducible (f ⁻¹' f '' (↑W : Set X))

Tactic:
⟨?_, (W.2.1.image _ hf₁.continuousOn).2.preimage_of_isPreirreducible_fiber _ hf₂ hf₃⟩

Premises used: Continuous.continuousOn, IsIrreducible, IsIrreducible.image, And.right, And.left, And.intro, IsPreirreducible.preimage_of_isPreirreducible_fiber, Subtype.property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
refine : (f ⁻¹' f '' (↑W : Set X)).Nonempty
⊢ IsIrreducible (f ⁻¹' f '' (↑W : Set X))

Tactic:
refine ⟨?_, (W.2.1.image _ hf₁.continuousOn).2.preimage_of_isPreirreducible_fiber _ hf₂ hf₃⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
obtain : ∀ (x : X) (hx : x ∈ (↑W : Set X)), (f ⁻¹' f '' (↑W : Set X)).Nonempty
⊢ (f ⁻¹' f '' (↑W : Set X)).Nonempty

Tactic:
obtain ⟨x, hx⟩ := W.2.1.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
x : X
hx : x ∈ (↑W : Set X)
⊢ (f ⁻¹' f '' (↑W : Set X)).Nonempty

Tactic:
⟨_, x, hx, rfl⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : (↑(irreducibleComponents X) : Type u_1)
x : X
hx : x ∈ (↑W : Set X)
⊢ (f ⁻¹' f '' (↑W : Set X)).Nonempty

Tactic:
exact ⟨_, x, hx, rfl⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : (↑(irreducibleComponents Y) : Type u_2)
⊢ LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          W :
        (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          Z :
        (↑(irreducibleComponents X) : Type u_1)) ↔
    W ≤ Z

Tactic:
⟨fun H ↦ ?_, Set.preimage_mono⟩

Premises used: Set.preimage_mono, 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
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : (↑(irreducibleComponents Y) : Type u_2)
refine :
  ∀
    (H :
      LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
        (({
                toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                  Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
                invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                  Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
            W :
          (↑(irreducibleComponents X) : Type u_1))
        (({
                toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                  Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
                invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                  Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
            Z :
          (↑(irreducibleComponents X) : Type u_1))),
    W ≤ Z
⊢ LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          W :
        (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          Z :
        (↑(irreducibleComponents X) : Type u_1)) ↔
    W ≤ Z

Tactic:
refine ⟨fun H ↦ ?_, Set.preimage_mono⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : (↑(irreducibleComponents Y) : Type u_2)
H :
  LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
    (({
            toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
            invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
              Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
        W :
      (↑(irreducibleComponents X) : Type u_1))
    (({
            toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
            invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
              Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
        Z :
      (↑(irreducibleComponents X) : Type u_1))
⊢ W ≤ Z

Tactic:
simpa only [Equiv.coe_fn_mk, Set.image_preimage_eq _ hf₄] using Set.image_mono (f := f) H

Premises used: Set.image_mono, Set.image_preimage_eq, Equiv.coe_fn_mk
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
obtain : ∀ (U : Set X) (hU : IsOpen[inst] U) (hUx : U ∩ s = {x}), x = y
⊢ x = y

Tactic:
obtain ⟨U, hU, hUx⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs x hxs

Premises used: isDiscrete_iff_forall_exists_isOpen, Iff.mp
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
obtain : ∀ (V : Set X) (hV : IsOpen[inst] V) (hVy : V ∩ s = {y}), x = y
⊢ x = y

Tactic:
obtain ⟨V, hV, hVy⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs y hys

Premises used: isDiscrete_iff_forall_exists_isOpen, Iff.mp
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
⊢ x ∈ s ∩ U

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
⊢ y ∈ s ∩ V

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
obtain : ∀ (z : X) (hz : z ∈ s ∩ (U ∩ V)), x = y
⊢ x = y

Tactic:
obtain ⟨z, hz⟩ := hs' _ _ hU hV ⟨x, by grind⟩ ⟨y, by grind⟩

Premises used: Exists.intro