awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h h₁ h₂ h₃ h₄ : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

Tactic:
rwa [(isClosed_of_mem_irreducibleComponents Z hZ).closure_subset_iff]

Premises used: isClosed_of_mem_irreducibleComponents, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₂ : Z ⊆ closure[inst] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
⊢ Z ⊆ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
rw [← Set.inter_eq_right.mpr h]

Premises used: Iff.mpr, Set.inter_eq_right
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₂ : IsOpen[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
h₃ : (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty
⊢ Z ⊆ closure[inst] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)

Tactic:
apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, And.right, And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₂ : IsClosed[inst] (⋃ i ∈ irreducibleComponents X \ {Z}, i)
⊢ IsOpen[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]

Premises used: Set.sUnion_eq_biUnion, isOpen_compl_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst] (⋃ i ∈ irreducibleComponents X \ {Z}, i)

Tactic:
hX.diff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst] (⋃ i ∈ irreducibleComponents X \ {Z}, i)

Tactic:
exact hX.diff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₂ : ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})
⊢ (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty

Tactic:
rw [Set.inter_compl_nonempty_iff]

Premises used: Set.inter_compl_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})

Tactic:
mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.diff Set.diff_subset)
        (Set.notMem_diff_of_mem (Set.mem_singleton Z))

Premises used: Set.mem_singleton, Set.diff_subset, mem_of_subset_sUnion_irreducibleComponents, Set.notMem_diff_of_mem, mt, Set.Finite.diff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})

Tactic:
exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.diff Set.diff_subset)
        (Set.notMem_diff_of_mem (Set.mem_singleton Z))

Premises used: Set.mem_singleton, Set.diff_subset, mem_of_subset_sUnion_irreducibleComponents, Set.notMem_diff_of_mem, mt, Set.Finite.diff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU : U.Nonempty
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
obtain : ∀ (z : X) (hz : z ∈ U), IsIrreducible S
⊢ IsIrreducible S

Tactic:
obtain ⟨z, hz⟩ := hU
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
⊢ IsIrreducible t

Tactic:
replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsIrreducible S

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

Premises used: IsIrreducible, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
refine : IsPreirreducible S
⊢ IsIrreducible S

Tactic:
refine ⟨⟨z, h₁ hz⟩, ?_⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ (t ∩ ⋂₀ (↑{U, u, v} : Set (Set X))).Nonempty

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

Premises used: isIrreducible_iff_sInter, Insert.insert, Iff.mp, Singleton.singleton
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
refine_1 : ∀ (u_1 : Set X), Membership.mem (γ := Finset (Set X)) {U, u, v} u_1 → IsOpen[inst] u_1
refine_2 : ∀ (u_1 : Set X), Membership.mem (γ := Finset (Set X)) {U, u, v} u_1 → (t ∩ u_1).Nonempty
⊢ (t ∩ ⋂₀ (↑{U, u, v} : Set (Set X))).Nonempty

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

Premises used: isIrreducible_iff_sInter, Insert.insert, Iff.mp, Singleton.singleton
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ (u_1 : Set X), Membership.mem (γ := Finset (Set X)) {U, u, v} u_1 → IsOpen[inst] u_1

Tactic:
simp [*]
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U_1 : Set X
hU' : IsOpen[inst] U_1
h₁ : U_1 ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U_1
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : Membership.mem (γ := Finset (Set X)) {U_1, u, v} U
⊢ U = U_1 ∨ U = u ∨ U = v

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

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U_1 : Set X
hU' : IsOpen[inst] U_1
h₁ : U_1 ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U_1
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U = U_1 ∨ U = u ∨ U = v
refine_2 : ∀ (hU' : IsOpen[inst] U) (h₁ : U ⊆ S) (hz : z ∈ U), (t ∩ U).Nonempty
refine_2₁ : ∀ (hu : IsOpen[inst] U) (hx' : x ∈ U), (t ∩ U).Nonempty
refine_2₂ : ∀ (hv : IsOpen[inst] U) (hy' : y ∈ U), (t ∩ U).Nonempty
⊢ (t ∩ U).Nonempty

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

Premises used: rfl
-- Module: Mathlib.Topology.Irreducible
Goal:
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[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
hz : z ∈ U
⊢ (t ∩ U).Nonempty

Tactic:
⟨z, h₂ (h₁ hz), hz⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U_1 : Set X
hU' : IsOpen[inst] U_1
h₁ : U_1 ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U_1
ht : IsIrreducible t
v : Set X
hv : IsOpen[inst] v
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hu : IsOpen[inst] U
hx' : x ∈ U
⊢ (t ∩ U).Nonempty

Tactic:
⟨x, h₂ hx, hx'⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U_1 : Set X
hU' : IsOpen[inst] U_1
h₁ : U_1 ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U_1
ht : IsIrreducible t
u : Set X
hu : IsOpen[inst] u
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
U : Set X
hv : IsOpen[inst] U
hy' : y ∈ U
⊢ (t ∩ U).Nonempty

Tactic:
⟨y, h₂ hy, hy'⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
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[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
hz : z ∈ U
⊢ (t ∩ U).Nonempty

Tactic:
exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
obtain : ∀ (x : X) (hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))), (S ∩ (u ∩ v)).Nonempty
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) := by
    refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
    · simp [*]
    · intro U H
      simp only [Finset.mem_insert, Finset.mem_singleton] at H
      rcases H with (rfl | rfl | rfl)
      exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]

Premises used: Insert.insert, Inter.inter, Set.Nonempty, SetLike.coe, Singleton.singleton, Set.sInter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x_1 : X
hx : x_1 ∈ S
hx'_1 : x_1 ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))
⊢ x ∈ U ∧ x ∈ u ∧ x ∈ v

Tactic:
simpa using hx'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x_1 : X
hx : x_1 ∈ S
hx'_1 : x_1 ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))
⊢ x ∈ U ∧ x ∈ u ∧ x ∈ v

Tactic:
replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x_1 : X
hx : x_1 ∈ S
hx'_1 : x_1 ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, h₁ hx'.1, hx'.2⟩

Premises used: Set.Nonempty, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x_1 : X
hx : x_1 ∈ S
hx'_1 : x_1 ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, h₁ hx'.1, hx'.2⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
obtain : (t ∩ ⋂₀ (↑{U, u, v} : Set (Set X))).Nonempty
obtain₁ : ∀ (x : X) (hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))), (S ∩ (u ∩ v)).Nonempty
obtain₂ : ∀ (x : X) (hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v), (S ∩ (u ∩ v)).Nonempty
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
classical
  obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) := by
    refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
    · simp [*]
    · intro U H
      simp only [Finset.mem_insert, Finset.mem_singleton] at H
      rcases H with (rfl | rfl | rfl)
      exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
  replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
  exact ⟨x, h₁ hx'.1, hx'.2⟩

Premises used: Insert.insert, Inter.inter, Set.Nonempty, SetLike.coe, Singleton.singleton, Set.sInter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t U : Set X
ht : IsPreirreducible t
hU : IsOpen[inst] U
hU' : U ⊆ t
⊢ IsPreirreducible U

Tactic:
U.eq_empty_or_nonempty.elim (fun h => h.symm ▸ isPreirreducible_empty) fun h =>
    (ht.subset_irreducible h hU (fun _ => id) hU').2

Premises used: isPreirreducible_empty, Eq.rec, id, IsPreirreducible.subset_irreducible, Set.eq_empty_or_nonempty, And.right, Or.elim, Eq.symm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set X
ht : IsPreirreducible t
⊢ IsPreirreducible (_root_.interior t)

Tactic:
ht.open_subset isOpen_interior interior_subset

Premises used: interior_subset, isOpen_interior, IsPreirreducible.open_subset
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
obtain : ∀ (z : Y) (hzV : z ∈ V) (hz₁ : z ∈ f '' U₁) (hz₂ : z ∈ f '' U₂), (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
obtain ⟨z, hzV, hz₁, hz₂⟩ :=
    hV _ _ (hf' _ hU₁) (hf' _ hU₂) ⟨f x, hxV, x, hxU₁, rfl⟩ ⟨f y, hyV, y, hyU₂, rfl⟩

Premises used: 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
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z : Y
hzV : z ∈ V
hz₁ : z ∈ f '' U₁
hz₂ : z ∈ f '' U₂
obtain :
  ∀ (z : Y) (z₁ : X) (hz₁ : z₁ ∈ U₁) (e₁ : f z₁ = z) (z₂ : X) (hz₂ : z₂ ∈ U₂) (e₂ : f z₂ = z) (hzV : z ∈ V)
    (hz : Membership.mem (γ := Set Y) {x : Y | IsPreirreducible (f ⁻¹' {x})} z), (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
obtain ⟨z, ⟨⟨z₁, hz₁, e₁⟩, ⟨z₂, hz₂, e₂⟩⟩, hzV, hz⟩ :=
    mem_closure_iff.mp (hf'' hzV) _ ((hf' _ hU₁).inter (hf' _ hU₂)) ⟨hz₁, hz₂⟩

Premises used: mem_closure_iff, And.intro, IsOpen.inter, Iff.mp
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z_1 : Y
hzV_1 : z_1 ∈ V
hz₁_1 : z_1 ∈ f '' U₁
hz₂_1 : z_1 ∈ f '' U₂
z : Y
z₁ : X
hz₁ : z₁ ∈ U₁
e₁ : f z₁ = z
z₂ : X
hz₂ : z₂ ∈ U₂
e₂ : f z₂ = z
hzV : z ∈ V
hz : Membership.mem (γ := Set Y) {x : Y | IsPreirreducible (f ⁻¹' {x})} z
obtain : ∀ (z₃ : X) (hz₃ : z₃ ∈ f ⁻¹' {z}) (hz₃' : z₃ ∈ U₁ ∩ U₂), (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
obtain ⟨z₃, hz₃, hz₃'⟩ := hz _ _ hU₁ hU₂ ⟨z₁, e₁, hz₁⟩ ⟨z₂, e₂, hz₂⟩

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
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z_1 : Y
hzV_1 : z_1 ∈ V
hz₁_1 : z_1 ∈ f '' U₁
hz₂_1 : z_1 ∈ f '' U₂
z : Y
z₁ : X
hz₁ : z₁ ∈ U₁
e₁ : f z₁ = z
z₂ : X
hz₂ : z₂ ∈ U₂
e₂ : f z₂ = z
hzV : z ∈ V
hz : Membership.mem (γ := Set Y) {x : Y | IsPreirreducible (f ⁻¹' {x})} z
z₃ : X
hz₃ : z₃ ∈ f ⁻¹' {z}
hz₃' : z₃ ∈ U₁ ∩ U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
⟨z₃, show f z₃ ∈ _ from (show f z₃ = z from hz₃) ▸ hzV, hz₃'⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z_1 : Y
hzV_1 : z_1 ∈ V
hz₁_1 : z_1 ∈ f '' U₁
hz₂_1 : z_1 ∈ f '' U₂
z : Y
z₁ : X
hz₁ : z₁ ∈ U₁
e₁ : f z₁ = z
z₂ : X
hz₂ : z₂ ∈ U₂
e₂ : f z₂ = z
hzV : z ∈ V
hz : Membership.mem (γ := Set Y) {x : Y | IsPreirreducible (f ⁻¹' {x})} z
z₃ : X
hz₃ : z₃ ∈ f ⁻¹' {z}
hz₃' : z₃ ∈ U₁ ∩ U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
refine ⟨z₃, show f z₃ ∈ _ from (show f z₃ = z from hz₃) ▸ hzV, hz₃'⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
⊢ IsPreirreducible (f ⁻¹' V)

Tactic:
hV.preimage_of_dense_isPreirreducible_fiber f hf' ?_

Premises used: IsPreirreducible.preimage_of_dense_isPreirreducible_fiber
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
refine : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
⊢ IsPreirreducible (f ⁻¹' V)

Tactic:
refine hV.preimage_of_dense_isPreirreducible_fiber f hf' ?_

Premises used: IsPreirreducible.preimage_of_dense_isPreirreducible_fiber
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
⊢ V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})

Tactic:
simp [hf'', subset_closure]

Premises used: subset_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 : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
⊢ IsPreirreducible (f ⁻¹' t)

Tactic:
ht.preimage_of_isPreirreducible_fiber f hf.isOpenMap
    fun _ ↦ (subsingleton_singleton.preimage hf.injective).isPreirreducible

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Set.subsingleton_singleton, Topology.IsEmbedding.injective, Set.Subsingleton.isPreirreducible, IsPreirreducible.preimage_of_isPreirreducible_fiber, 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 : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩

Premises used: IsIrreducible, And.right, And.intro, IsPreirreducible.preimage_of_isPreirreducible_fiber
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
refine : (f ⁻¹' t).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
refine ⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
obtain : ∀ (x : Y) (hx : f x ∈ t), (f ⁻¹' t).Nonempty
⊢ (f ⁻¹' t).Nonempty

Tactic:
obtain ⟨-, hx, x, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
x : Y
hx : f x ∈ t
⊢ (f ⁻¹' t).Nonempty

Tactic:
⟨x, hx⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
x : Y
hx : f x ∈ t
⊢ (f ⁻¹' t).Nonempty

Tactic:
exact ⟨x, hx⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

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

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Set.subsingleton_singleton, IsIrreducible.preimage_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 : IsIrreducible t
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

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

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Set.subsingleton_singleton, IsIrreducible.preimage_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
hf : IsOpenEmbedding f
inst_2 : PreirreducibleSpace X
rw : IsPreirreducible (f ⁻¹' univ)
rw₁ : Type u_1
rw₂ : Y → X
⊢ IsPreirreducible.{u_2} (X := Y) univ

Tactic:
rw [← Set.preimage_univ]

Premises used: Set.preimage_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst_2 : PreirreducibleSpace X
⊢ IsPreirreducible (f ⁻¹' univ)

Tactic:
.preimage PreirreducibleSpace.isPreirreducible_univ hf

Premises used: PreirreducibleSpace.isPreirreducible_univ, IsPreirreducible.preimage