awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
inst_2 : AddGroup R
inst_3 : AddGroup M
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup M
⊢ IsUniformAddGroup (tsze R M)

Tactic:
inferInstanceAs <| IsUniformAddGroup (R × M)

Premises used: _private.0.TrivSqZeroExt.instIsUniformAddGroup._proof_1
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
⊢ Eq (α := Filter (tsze R M × tsze R M)) (𝓤 (tsze R M))
    (Filter.comap (fun (p : tsze R M × tsze R M) ↦ (p.1.fst, p.2.fst)) (𝓤 R) ⊓
      Filter.comap (fun (p : tsze R M × tsze R M) ↦ (p.1.snd, p.2.snd)) (𝓤 M))

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, Set.Mem, uniformity, setOf, TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
⊢ UniformContinuous (α := tsze R M) fst

Tactic:
uniformContinuous_fst

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, TrivSqZeroExt.fst, uniformContinuous_fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
⊢ UniformContinuous (α := tsze R M) snd

Tactic:
uniformContinuous_snd

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, uniformContinuous_snd, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
inst_2 : Zero M
⊢ UniformContinuous (α := R) (β := tsze R M) inl

Tactic:
uniformContinuous_id.prodMk uniformContinuous_const

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, UniformContinuous.prodMk, TrivSqZeroExt.inl, uniformContinuous_id, uniformContinuous_const, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
inst_2 : Zero R
⊢ UniformContinuous (α := M) (β := tsze R M) inr

Tactic:
uniformContinuous_const.prodMk uniformContinuous_id

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.inr, TrivSqZeroExt, setOf, UniformContinuous.prodMk, uniformContinuous_id, uniformContinuous_const, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.ZMod
Goal:
N : ℕ
⊢ DiscreteTopology (ZMod N)

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
inl : DiscreteTopology ↥(AddSubgroup.zmultiples 0)
inr : ∀ (ha : a ≠ 0), DiscreteTopology ↥(AddSubgroup.zmultiples a)
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
inl : DiscreteTopology ↥⊥
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)

Tactic:
rw [AddSubgroup.zmultiples_zero_eq_bot]

Premises used: AddSubgroup.zmultiples_zero_eq_bot
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology ↥⊥

Tactic:
Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))

Premises used: Set.Mem, Subsingleton.discreteTopology
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology ↥⊥

Tactic:
exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))

Premises used: Subsingleton.discreteTopology
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
inr :
  ∃ (t : Set ℝ),
    IsOpen t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' t) {0}
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]

Premises used: discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ (t : Set ℝ),
    IsOpen t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' t) {0}

Tactic:
⟨ball 0 |a|, isOpen_ball, ?_⟩

Premises used: abs, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
inr :
  Eq (α := Set ↥(AddSubgroup.zmultiples a))
    (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
    {0}
⊢ ∃ (t : Set ℝ),
    IsOpen t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' t) {0}

Tactic:
refine ⟨ball 0 |a|, isOpen_ball, ?_⟩
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
inr :
  ∀ (x : ℝ) (hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x),
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹'
          ball 0 |a|)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx) ↔
      Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx)
⊢ Eq (α := Set ↥(AddSubgroup.zmultiples a))
    (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
    {0}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
x : ℝ
hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x
inr :
  ∀ (k : ℤ) (hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) (k • a)),
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹'
          ball 0 |a|)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) (k • a) hx) ↔
      Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) (k • a) hx)
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx)

Tactic:
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx

Premises used: AddSubgroup.mem_zmultiples_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) (k • a)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : |k| < 1 ↔ |k| < 1
⊢ LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ |k| < 1

Tactic:
norm_cast
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
apply : IsDiscrete (↑(AddMonoidHom.range (castAddHom ℝ)) : Set ℝ)
⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)

Tactic:
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective

Premises used: AddMonoidHom.tendsto_coe_cofinite_of_discrete, Int.cast_injective
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
rw : DiscreteTopology ↥(AddSubgroup.zmultiples 1)
⊢ IsDiscrete (↑(AddMonoidHom.range (castAddHom ℝ)) : Set ℝ)

Tactic:
rw [range_castAddHom, SetLike.isDiscrete_iff_discreteTopology]

Premises used: Int.range_castAddHom, SetLike.isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
ha : a ≠ 0
apply : IsDiscrete (↑(AddMonoidHom.range (G := ℤ) ((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a)) : Set ℝ)
⊢ Tendsto (α := ℤ) (⇑((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a : ℤ →+ ℝ) : (a : ℤ) → ℝ) Filter.cofinite (cocompact ℝ)

Tactic:
apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha

Premises used: smul_left_injective, Int, AddMonoidHom.tendsto_coe_cofinite_of_discrete
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
ha : a ≠ 0
rw : DiscreteTopology ↥(AddSubgroup.zmultiples a)
⊢ IsDiscrete (↑(AddMonoidHom.range (G := ℤ) ((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a)) : Set ℝ)

Tactic:
rw [AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology]

Premises used: AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
⊢ Tendsto (α := ↥(zmultiples a)) (⇑(AddSubgroup.subtype (zmultiples a)) : (a : ↥(zmultiples a)) → ℝ) Filter.cofinite
    (cocompact ℝ)

Tactic:
(zmultiples a).tendsto_coe_cofinite_of_discrete ?_

Premises used: AddSubgroup.tendsto_coe_cofinite_of_discrete, AddSubgroup.zmultiples
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
refine : IsDiscrete (↑(zmultiples a) : Set ℝ)
⊢ Tendsto (α := ↥(zmultiples a)) (⇑(AddSubgroup.subtype (zmultiples a)) : (a : ↥(zmultiples a)) → ℝ) Filter.cofinite
    (cocompact ℝ)

Tactic:
refine (zmultiples a).tendsto_coe_cofinite_of_discrete ?_

Premises used: AddSubgroup.tendsto_coe_cofinite_of_discrete, AddSubgroup.zmultiples
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
rw : DiscreteTopology ↥(zmultiples a)
⊢ IsDiscrete (↑(zmultiples a) : Set ℝ)

Tactic:
rw [SetLike.isDiscrete_iff_discreteTopology]

Premises used: SetLike.isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.Instances.ZMultiples
Goal:
a : ℝ
⊢ DiscreteTopology ↥(zmultiples a)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
⊢ s.Nonempty

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
⊢ IsPreirreducible s

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsPreirreducible.{u_1} (X := X) ∅

Tactic:
fun _ _ _ _ _ ⟨_, h1, _⟩ =>
  h1.elim

Premises used: _private.0.isPreirreducible_empty.match_1, IsPreirreducible, False.elim, Inter.inter, Set.Nonempty, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Subsingleton
⊢ IsPreirreducible s

Tactic:
fun _u _v _ _ ⟨_x, hxs, hxu⟩ ⟨y, hys, hyv⟩ => ⟨y, hys, hs hxs hys ▸ hxu, hyv⟩

Premises used: IsPreirreducible, _private.0.Set.Subsingleton.isPreirreducible.match_1, Eq.rec, Inter.inter, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPreirreducible (X := X) {x}

Tactic:
subsingleton_singleton.isPreirreducible

Premises used: Set.subsingleton_singleton, Set.Subsingleton.isPreirreducible
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsIrreducible (X := X) {x}

Tactic:
⟨singleton_nonempty x, isPreirreducible_singleton⟩

Premises used: Set.singleton_nonempty, IsIrreducible, isPreirreducible_singleton, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
rw :
  (s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
rw₁ : IsOpen[inst] u
⊢ (closure[inst] s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
rw [closure_inter_open_nonempty_iff]

Premises used: closure_inter_open_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
rw :
  (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
rw₁ : IsOpen[inst] v
⊢ (s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
rw [closure_inter_open_nonempty_iff]

Premises used: closure_inter_open_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
rw : IsOpen[inst] (u ∩ v)
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
rw [closure_inter_open_nonempty_iff]

Premises used: closure_inter_open_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
iterate : IsOpen[inst] (u ∩ v)
iterate₁ : IsOpen[inst] v
iterate₂ : IsOpen[inst] u
⊢ (closure[inst] s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
iterate 3 rw [closure_inter_open_nonempty_iff]

Premises used: closure_inter_open_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ IsOpen[inst] (u ∩ v)

Tactic:
hu.inter hv

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ IsOpen[inst] v

Tactic:
hv
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ IsOpen[inst] u

Tactic:
hu
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ IsOpen[inst] (u ∩ v)

Tactic:
exacts [hu.inter hv, hv, hu]

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsIrreducible (closure[inst] s) ↔ IsIrreducible s

Tactic:
and_congr closure_nonempty_iff isPreirreducible_iff_closure

Premises used: closure_nonempty_iff, IsIrreducible, isPreirreducible_iff_closure, and_congr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : IsPreirreducible s
⊢ ∃ (t : Set X), IsPreirreducible t ∧ s ⊆ t ∧ ∀ (u : Set X), IsPreirreducible u → t ⊆ u → u = t

Tactic:
let ⟨m, hsm, hm⟩ :=
    zorn_subset_nonempty { t : Set X | IsPreirreducible t }
      (fun c hc hcc _ =>
        ⟨⋃₀ c, fun u v hu hv ⟨y, hy, hyu⟩ ⟨x, hx, hxv⟩ =>
          let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy
          let ⟨q, hqc, hxq⟩ := mem_sUnion.1 hx
          Or.casesOn (hcc.total hpc hqc)
            (fun hpq : p ⊆ q =>
              let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv ⟨y, hpq hyp, hyu⟩ ⟨x, hxq, hxv⟩
              ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
            fun hqp : q ⊆ p =>
            let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv ⟨y, hyp, hyu⟩ ⟨x, hqp hxq, hxv⟩
            ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩,
          fun _ hxc => subset_sUnion_of_mem hxc⟩)
      s H
  ⟨m, hm.prop, hsm, fun _u hu hmu => (hm.eq_of_subset hu hmu).symm⟩

Premises used: IsPreirreducible, setOf, Set.sUnion, Maximal.prop, Exists, _private.0.exists_preirreducible.match_4, HasSubset.Subset, Or.casesOn, Inter.inter, _private.0.exists_preirreducible.match_1, And, Set.Nonempty, Set.mem_sUnion_of_mem, zorn_subset_nonempty, Maximal.eq_of_subset, And.intro, Exists.intro, Iff.mp, Set.subset_sUnion_of_mem, _private.0.exists_preirreducible.match_2, Set.mem_sUnion, Eq.symm, IsChain.total, _private.0.exists_preirreducible.match_3
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
rw : s = closure[inst] s
⊢ IsClosed[inst] s

Tactic:
rw [← closure_eq_iff_isClosed, eq_comm]

Premises used: closure_eq_iff_isClosed, eq_comm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s = closure[inst] s

Tactic:
subset_closure.antisymm (H.2 H.1.closure subset_closure)

Premises used: subset_closure, IsIrreducible.closure, And.right, And.left, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s = closure[inst] s

Tactic:
exact subset_closure.antisymm (H.2 H.1.closure subset_closure)

Premises used: subset_closure, IsIrreducible.closure, And.right, And.left, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    s ∈ irreducibleComponents X ↔
      Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
⊢ irreducibleComponents X = {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s}

Tactic:
ext s
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
h :
  s ∈ irreducibleComponents X →
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
h₁ :
  Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s →
    s ∈ irreducibleComponents X
⊢ s ∈ irreducibleComponents X ↔
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s

Tactic:
constructor
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s

Tactic:
⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩

Premises used: isClosed_of_mem_irreducibleComponents, Set.Mem, setOf, And.right, And.left, And.intro, Maximal
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s

Tactic:
exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
⊢ s ∈ irreducibleComponents X

Tactic:
⟨H.1.2, fun x h e => ?_⟩

Premises used: irreducibleComponents, Set.Mem, setOf, And.right, And.left, And.intro, Maximal
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
h : ∀ (x : Set X) (h : IsIrreducible x) (e : s ≤ x), x ≤ s
⊢ s ∈ irreducibleComponents X

Tactic:
refine ⟨H.1.2, fun x h e => ?_⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
x : Set X
h : IsIrreducible x
e : s ≤ x
⊢ closure[inst] x ≤ s

Tactic:
have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
x : Set X
h : IsIrreducible x
e : s ≤ x
this : closure[inst] x ≤ s
⊢ x ≤ s

Tactic:
le_trans subset_closure this

Premises used: subset_closure, le_trans
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
x : Set X
h : IsIrreducible x
e : s ≤ x
this : closure[inst] x ≤ s
⊢ x ≤ s

Tactic:
exact le_trans subset_closure this

Premises used: subset_closure, le_trans
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
obtain :
  ∀ (u : Set X) (hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u),
    ∃ u ∈ irreducibleComponents X, s ⊆ u
⊢ ∃ u ∈ irreducibleComponents X, s ⊆ u

Tactic:
obtain ⟨u, hu⟩ := exists_preirreducible s hs.isPreirreducible

Premises used: IsIrreducible.isPreirreducible, exists_preirreducible
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
right : s ⊆ u
⊢ ∃ u ∈ irreducibleComponents X, s ⊆ u

Tactic:
use u, ⟨⟨hs.left.mono hu.right.left,hu.left⟩,fun _ h hl => (hu.right.right _ h.right hl).le⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
⊢ s ⊆ u

Tactic:
hu.right.left

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
⊢ s ⊆ u

Tactic:
exact hu.right.left

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPreirreducible (irreducibleComponent x) ∧
    {x} ⊆ irreducibleComponent x ∧
      ∀ (u : Set X), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x

Tactic:
Classical.choose_spec (exists_preirreducible {x} isPreirreducible_singleton)

Premises used: Classical.choose_spec, isPreirreducible_singleton, Singleton.singleton, exists_preirreducible, irreducibleComponent
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ∈ irreducibleComponent x

Tactic:
singleton_subset_iff.1 (irreducibleComponent_property x).2.1

Premises used: Set.singleton_subset_iff, And.right, And.left, Iff.mp, irreducibleComponent_property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsIrreducible (irreducibleComponent x)

Tactic:
⟨⟨x, mem_irreducibleComponent⟩, (irreducibleComponent_property x).1⟩

Premises used: IsIrreducible, And.left, And.intro, Exists.intro, mem_irreducibleComponent, irreducibleComponent_property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
x : X
⊢ IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x

Tactic:
(irreducibleComponent_property x).2.2 _

Premises used: And.right, irreducibleComponent_property
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ irreducibleComponent x ∈ irreducibleComponents X

Tactic:
⟨isIrreducible_irreducibleComponent, fun _ h₁ h₂ => (eq_irreducibleComponent h₁.2 h₂).le⟩

Premises used: irreducibleComponents, Set.Mem, setOf, Eq.le, eq_irreducibleComponent, And.right, And.intro, Maximal, isIrreducible_irreducibleComponent