awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 x ∈ v
have refine_2 : x ∈ f ⁻¹' v
Tactic: rw [← mem_preimage]
-- 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 : 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
have refine_2 : x ∈ f ⁻¹' v ∩ s
Tactic: apply mem_of_mem_inter_left
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
⊢ Set.Nonempty (α := (↑s : Type u_1))
    (univ ∩ (val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ∩ val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v))
have 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))
Tactic: rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : PreirreducibleSpace.{u_1} (↑s : Type u_1)
⊢ IsPreirreducible s
have rw : IsPreirreducible.{u_1} (X := X) (Set.image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
Tactic: rw [← Subtype.range_coe (s := s), ← Set.image_univ]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
have refine : ContinuousOn.{u_1, u_1} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ
Tactic: refine PreirreducibleSpace.isPreirreducible_univ.image Subtype.val ?_
-- 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
inst_2 : IndiscreteTopology X
u v : Set X
⊢ IsOpen[inst] u → IsOpen[inst] v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty
have simp : u = ∅ ∨ u = univ → v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Tactic: simp only [IndiscreteTopology.isOpen_iff, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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)
⊢ IsOpen u → IsOpen v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty
have simp : (u.Nonempty → uᶜ.Finite) → (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Tactic: simp only [CofiniteTopology.isOpen_iff, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
have 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
Tactic: refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
have 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
Tactic: refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
have 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
Tactic: refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ (s ∩ ⋂₀ (↑(insert u U) : Set (Set X))).Nonempty
have refine_1 : (s ∩ (u ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty
Tactic: rw [Finset.coe_insert, sInter_insert]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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
⊢ (s ∩ (u ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty
have hu₁ : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
Tactic: rw [Finset.forall_mem_insert] at hu hU
Cleared hypotheses: hu, hU
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
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 ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty
have hU₁ : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
Tactic: rw [Finset.forall_mem_insert] at hu hU
Cleared hypotheses: hu, hU
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
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
have refine_1 : ∀ (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: induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
Cleared hypotheses: U, hu, hU
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
U : Finset (Set X)
hu : ∀ u ∈ U, IsOpen[inst] u
hU : ∀ u ∈ U, (s ∩ u).Nonempty
refine_1 :
  ∀ (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
⊢ (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
have refine_1₁ : ∀ (u : Set X) (U : Finset (Set X)),
  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),
      (s ∩ ⋂₀ (↑(insert u U) : Set (Set X))).Nonempty
Tactic: induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
Cleared hypotheses: U, hu, hU
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
have 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
Tactic: classical
  refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
  · simpa using h ∅
  · intro u v hu hv hu' hv'
    simpa [*] using h {u, v}
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
have 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
Tactic: classical
  refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
  · simpa using h ∅
  · intro u v hu hv hu' hv'
    simpa [*] using h {u, v}
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
have 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
Tactic: classical
  refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
  · simpa using h ∅
  · intro u v hu hv hu' hv'
    simpa [*] using h {u, v}
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have refine : ∀ (z₁ z₂ : Set X),
  IsOpen[inst] z₁ᶜ → IsOpen[inst] z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Tactic: refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsOpen[inst] z₁ᶜ → IsOpen[inst] z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have simp : IsClosed[inst] z₁ → IsClosed[inst] z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
  IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Tactic: simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsClosed[inst] z₁ → IsClosed[inst] z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have refine : IsClosed[inst] z₁ → IsClosed[inst] z₂ → (¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂)
Tactic: refine forall₂_congr fun _ _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
h : IsClosed[inst] z₁
h_1 : IsClosed[inst] z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have rw : ¬s ⊆ z₁ ∧ ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
h : IsClosed[inst] z₁
h_1 : IsClosed[inst] z₂
rw : ¬s ⊆ z₁ ∧ ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have rw₁ : ¬(s ⊆ z₁ ∨ s ⊆ z₂) → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
h : IsClosed[inst] z₁
h_1 : IsClosed[inst] z₂
rw : ¬s ⊆ z₁ ∧ ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
rw₁ : ¬(s ⊆ z₁ ∨ s ⊆ z₂) → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
have rw₂ : s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z
have simp : (∀ (U : Finset (Set X)),
    (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty) ↔
  ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z
Tactic: simp only [isIrreducible_iff_sInter]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z
have refine : ∀ {t : Finset (Set X)},
  (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ (z : Set X),
        Membership.mem (γ := Finset (Set X))
            ((Equiv.finsetCongr (Function.Involutive.toPerm compl sorry) : (a : Finset (Set X)) → Finset (Set X)) t :
              Finset (Set X))
            z →
          IsClosed[inst] z) →
      s ⊆
          ⋃₀
            (↑((Equiv.finsetCongr (Function.Involutive.toPerm compl sorry) : (a : Finset (Set X)) → Finset (Set X)) t :
                  Finset (Set X)) :
              Set (Set X)) →
        ∃ (z : Set X),
          Membership.mem (γ := Finset (Set X))
              ((Equiv.finsetCongr (Function.Involutive.toPerm compl sorry) : (a : Finset (Set X)) → Finset (Set X)) t :
                Finset (Set X))
              z ∧
            s ⊆ z
Tactic: refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ (z : Set X),
        Membership.mem (γ := Finset (Set X))
            ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
              Finset (Set X))
            z →
          IsClosed[inst] z) →
      s ⊆
          ⋃₀
            (↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                  Finset (Set X)) :
              Set (Set X)) →
        ∃ (z : Set X),
          Membership.mem (γ := Finset (Set X))
              ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                Finset (Set X))
              z ∧
            s ⊆ z
have simp_rw : (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
  (∀ u ∈ t, IsOpen[inst] u) → s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ → ∃ a ∈ t, s ⊆ aᶜ
Tactic: simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
    sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
    exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst] u) → s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ → ∃ a ∈ t, s ⊆ aᶜ
have refine : (∀ u ∈ t, IsOpen[inst] u) →
  ((∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ)
Tactic: refine forall_congr' fun _ => Iff.trans ?_ not_imp_not
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
⊢ S ⊆ closure[inst] (S ∩ U)
have by_contra : ∀ (h' : ¬S ⊆ closure[inst] (S ∩ U)), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst] (S ∩ U)
⊢ False
have obtain : ∀ (x : X) (h₁ : x ∈ S) (h₂ : x ∈ U) (h₃ : x ∈ (closure[inst] (S ∩ U))ᶜ), False
Tactic: obtain ⟨x, h₁, h₂, h₃⟩ :=
    hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
have refine_1 : ∀ (h : IsPreirreducible S) (x : Set X), IsOpen[inst] x → (S ∩ x).Nonempty → S ⊆ closure[inst] (S ∩ x)
Tactic: refine ⟨fun h _ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
refine_1 : ∀ (h : IsPreirreducible S) (x : Set X), IsOpen[inst] x → (S ∩ x).Nonempty → S ⊆ closure[inst] (S ∩ x)
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
have refine_2 : ∀ (h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)), IsPreirreducible S
Tactic: refine ⟨fun h _ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
⊢ (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
have refine_2 : ∀ (p : X) (pS : p ∈ S) (pa : p ∈ a), (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
Tactic: ⟨p, pS, pa⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
⊢ (S ∩ (a ∩ b)).Nonempty
have refine_2 : ∀ (h0 : S ∩ (a ∩ b) = ∅), False
Tactic: by_contra! h0
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ False
have refine_2 : p ∉ closure[inst] (S ∩ b)
Tactic: suffices p ∉ closure (S ∩ b) from this <| (h b hb bS) pS
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ p ∉ closure[inst] (S ∩ b)
have refine_2 : ∃ (x : Set X), IsClosed[inst] x ∧ S ∩ b ⊆ x ∧ p ∉ x
Tactic: simp only [closure, mem_sInter, mem_setOf_eq, and_imp, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ ∃ (x : Set X), IsClosed[inst] x ∧ S ∩ b ⊆ x ∧ p ∉ x
have h₁ : IsClosed[inst] aᶜ ∧ S ∩ b ⊆ aᶜ ∧ p ∉ aᶜ
Tactic: use aᶜ
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U
have rw : (∀ (U : Set X), IsOpen[inst] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst] (univ ∩ U)) ↔
  ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U
Tactic: rw [preirreducibleSpace_iff, isPreirreducible_iff_subset_closure_inter_open]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ (∀ (U : Set X), IsOpen[inst] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U
have simp : (∀ (U : Set X), IsOpen[inst] U → U.Nonempty → closure[inst] U = univ) ↔
  ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → ∀ (x : X), x ∈ closure[inst] U
Tactic: simp only [univ_inter, univ_subset_iff, Dense]