awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
⊢ Z ∈ S
have obtain : ∀ (W : Set X) (hWS : W ∈ hS.toFinset (s := S)) (hZW : Z ⊆ W), Z ∈ S
Tactic: obtain ⟨W, hWS, hZW⟩ := isIrreducible_iff_sUnion_isClosed.mp hZ.1 hS.toFinset
    (fun W hW ↦ isClosed_of_mem_irreducibleComponents W (hSα (hS.mem_toFinset.mp hW)))
    (hS.coe_toFinset.symm ▸ hZS)
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ hS.toFinset (s := S)
hZW : Z ⊆ W
⊢ Z ∈ S
have hWS₁ : W ∈ S
Tactic: rw [hS.mem_toFinset] at hWS
Cleared hypotheses: hWS, hZW
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
have rw : {Z} ⊆ irreducibleComponents X
Tactic: rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.diff_union_of_subset, sUnion_irreducibleComponents]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z
have h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
Tactic: have h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z := by
    rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.diff_union_of_subset, sUnion_irreducibleComponents]
    rwa [Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z
have h₁ : closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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₁ : closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z
have h₂ : Z ⊆ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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 ⊆ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
have h₂ : Z ⊆ closure[inst] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
Tactic: rw [← Set.inter_eq_right.mpr h]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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 ⊆ closure[inst] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
have h₂ : IsOpen[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
Tactic: apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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}))ᶜ
⊢ Z ⊆ closure[inst] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
have h₃ : (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty
Tactic: apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsOpen[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
have h₂ : IsClosed[inst] (⋃ i ∈ irreducibleComponents X \ {Z}, i)
Tactic: rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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}))ᶜ).Nonempty
have h₂ : ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})
Tactic: rw [Set.inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ IsIrreducible S
have obtain : ∀ (z : X) (hz : z ∈ U), IsIrreducible S
Tactic: obtain ⟨z, hz⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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 S
have ht₁ : IsIrreducible t
Tactic: replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
have refine : IsPreirreducible S
Tactic: refine ⟨⟨z, h₁ hz⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
have refine_1 : ∀ (u_1 : Set X), Membership.mem (γ := Finset (Set X)) {U, u, v} u_1 → IsOpen[inst] u_1
Tactic: refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (t ∩ ⋂₀ (↑{U, u, v} : Set (Set X))).Nonempty
have refine_2 : ∀ (u_1 : Set X), Membership.mem (γ := Finset (Set X)) {U, u, v} u_1 → (t ∩ u_1).Nonempty
Tactic: refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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
⊢ (t ∩ U).Nonempty
have H₁ : U = U_1 ∨ U = u ∨ U = v
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (t ∩ U).Nonempty
have refine_2 : ∀ (hU' : IsOpen[inst] U) (h₁ : U ⊆ S) (hz : z ∈ U), (t ∩ U).Nonempty
Tactic: rcases H with (rfl | rfl | rfl)
Cleared hypotheses: U_1, hU', h₁, hz, H
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (t ∩ U).Nonempty
have refine_2₁ : ∀ (hu : IsOpen[inst] U) (hx' : x ∈ U), (t ∩ U).Nonempty
Tactic: rcases H with (rfl | rfl | rfl)
Cleared hypotheses: u, hu, hx', H
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (t ∩ U).Nonempty
have refine_2₂ : ∀ (hv : IsOpen[inst] U) (hy' : y ∈ U), (t ∩ U).Nonempty
Tactic: rcases H with (rfl | rfl | rfl)
Cleared hypotheses: v, hv, hy', H
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (S ∩ (u ∩ v)).Nonempty
have obtain : ∀ (x : X) (hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))), (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'⟩]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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))
⊢ (S ∩ (u ∩ v)).Nonempty
have hx'₁ : x ∈ U ∧ x ∈ u ∧ x ∈ v
Tactic: replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (S ∩ (u ∩ v)).Nonempty
have obtain : (t ∩ ⋂₀ (↑{U, u, v} : Set (Set X))).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⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (S ∩ (u ∩ v)).Nonempty
have obtain₁ : ∀ (x : X) (hx' : x ∈ ⋂₀ (↑{U, u, v} : Set (Set X))), (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⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (S ∩ (u ∩ v)).Nonempty
have obtain₂ : ∀ (x : X) (hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v), (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⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
have obtain : ∀ (z : Y) (hzV : z ∈ V) (hz₁ : z ∈ f '' U₁) (hz₂ : z ∈ f '' U₂), (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⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
have 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
Tactic: obtain ⟨z, ⟨⟨z₁, hz₁, e₁⟩, ⟨z₂, hz₂, e₂⟩⟩, hzV, hz⟩ :=
    mem_closure_iff.mp (hf'' hzV) _ ((hf' _ hU₁).inter (hf' _ hU₂)) ⟨hz₁, hz₂⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
have obtain : ∀ (z₃ : X) (hz₃ : z₃ ∈ f ⁻¹' {z}) (hz₃' : z₃ ∈ U₁ ∩ U₂), (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
Tactic: obtain ⟨z₃, hz₃, hz₃'⟩ := hz _ _ hU₁ hU₂ ⟨z₁, e₁, hz₁⟩ ⟨z₂, e₂, hz₂⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
have refine : V ⊆ closure[inst_1] (V ∩ {x : Y | IsPreirreducible (f ⁻¹' {x})})
Tactic: refine hV.preimage_of_dense_isPreirreducible_fiber f hf' ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
have refine : (f ⁻¹' t).Nonempty
Tactic: refine ⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (f ⁻¹' t).Nonempty
have obtain : ∀ (x : Y) (hx : f x ∈ t), (f ⁻¹' t).Nonempty
Tactic: obtain ⟨-, hx, x, rfl⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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.{u_2} (X := Y) univ
have rw : IsPreirreducible (f ⁻¹' univ)
Tactic: rw [← Set.preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
have refine : ∀ (u : Set Y) (hu : IsIrreducible u) (htu : f ⁻¹' t ≤ u), t ≤ closure[inst] (f '' u)
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 ?_))⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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] (f '' u)
have suffices : t ≤ closure[inst] (f '' f ⁻¹' t)
Tactic: suffices t ≤ closure (f '' f ⁻¹' t) from this.trans (closure_mono (image_mono htu))
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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] (f '' f ⁻¹' t)
have rw : t ≤ closure[inst] (t ∩ range f)
Tactic: rw [image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ closure[inst] (f '' f ⁻¹' s) = s
have refine : s ⊆ closure[inst] (f '' f ⁻¹' s)
Tactic: refine subset_antisymm (closure_minimal (by simp) hs') ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
have refine_1 : (s ∩ range f).Nonempty
Tactic: refine subset_trans (subset_closure_inter_of_isPreirreducible_of_isOpen hs h.isOpen_range ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ s ⊆ closure[inst] (f '' f ⁻¹' s)
have refine_2 : closure[inst] (s ∩ range f) ⊆ closure[inst] (f '' f ⁻¹' s)
Tactic: refine subset_trans (subset_closure_inter_of_isPreirreducible_of_isOpen hs h.isOpen_range ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ closure[inst] (s ∩ range f) ⊆ closure[inst] (f '' f ⁻¹' s)
have refine_2 : s ∩ range f ⊆ f '' f ⁻¹' s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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).Nonempty
have obtain : ∀ (x : X) (hx : x ∈ V), (f ⁻¹' Z).Nonempty
Tactic: obtain ⟨x, hx⟩ := hV.1.1
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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
⊢ Z ≤ f '' V
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ Z ≤ f '' V
have rw : f '' f ⁻¹' Z ≤ f '' V
Tactic: rw [← Set.image_preimage_eq Z hf₄]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
have refine : IsIrreducible (f ⁻¹' f '' (↑W : Set X))
Tactic: refine (Set.subset_preimage_image _ _).antisymm' (W.2.2 ?_ (Set.subset_preimage_image _ _))
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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))
have refine : (f ⁻¹' f '' (↑W : Set X)).Nonempty
Tactic: refine ⟨?_, (W.2.1.image _ hf₁.continuousOn).2.preimage_of_isPreirreducible_fiber _ hf₂ hf₃⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
⊢ (f ⁻¹' f '' (↑W : Set X)).Nonempty
have obtain : ∀ (x : X) (hx : x ∈ (↑W : Set X)), (f ⁻¹' f '' (↑W : Set X)).Nonempty
Tactic: obtain ⟨x, hx⟩ := W.2.1.1