awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Opens α
rw :
  IsAtom (α := (Opens α)ᵒᵈ) ((toDual : (a : Opens α) → (Opens α)ᵒᵈ) s.compl.compl : (Opens α)ᵒᵈ) ↔
    ∃ (x : α), s.compl.compl = Closeds.compl {x}
⊢ IsCoatom s ↔ ∃ (x : α), s = Closeds.compl {x}

Tactic:
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]

Premises used: isAtom_dual_iff_isCoatom, TopologicalSpace.Opens.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Opens α
⊢ IsAtom (α := (Opens α)ᵒᵈ) ((Closeds.complOrderIso α : (a : Closeds α) → (Opens α)ᵒᵈ) s.compl : (Opens α)ᵒᵈ) ↔
    ∃ (x : α), s.compl.compl = Closeds.compl {x}

Tactic:
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff,
    Closeds.compl_bijective.injective.eq_iff]

Premises used: Function.Injective.eq_iff, OrderIso.isAtom_iff, Function.Bijective.injective, TopologicalSpace.Closeds.isAtom_iff, TopologicalSpace.Closeds.compl_bijective, TopologicalSpace.Closeds.complOrderIso
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Clopens α
h : Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) s) ((fun (s : Clopens α) ↦ s.carrier) t)
mk :
  ∀ (carrier : Set α) (isClopen' : IsClopen carrier)
    (h :
      Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
        ((fun (s : Clopens α) ↦ s.carrier) t)),
    { carrier := carrier, isClopen' := isClopen' : Clopens α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Clopens α
carrier : Set α
isClopen' : IsClopen carrier
h :
  Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
    ((fun (s : Clopens α) ↦ s.carrier) t)
mk :
  ∀ (carrier_1 : Set α) (isClopen'_1 : IsClopen carrier_1)
    (h :
      Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
        ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier_1, isClopen' := isClopen'_1 })),
    { carrier := carrier, isClopen' := isClopen' : Clopens α } = { carrier := carrier_1, isClopen' := isClopen'_1 }
⊢ { carrier := carrier, isClopen' := isClopen' : Clopens α } = t

Tactic:
cases t
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
carrier : Set α
isClopen' : IsClopen carrier
carrier_1 : Set α
isClopen'_1 : IsClopen carrier_1
h :
  Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
    ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier_1, isClopen' := isClopen'_1 })
⊢ { carrier := carrier, isClopen' := isClopen' : Clopens α } = { carrier := carrier_1, isClopen' := isClopen'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Clopens α
⊢ IsClopen (↑s : Set α)

Tactic:
s.isClopen'

Premises used: TopologicalSpace.Clopens.isClopen'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Clopens α
⊢ IsOpen[inst] (↑s : Set α)

Tactic:
s.isClopen.isOpen

Premises used: TopologicalSpace.Clopens.isClopen, IsClopen.isOpen
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Clopens α
⊢ IsClosed[inst] (↑s : Set α)

Tactic:
s.isClopen.isClosed

Premises used: TopologicalSpace.Clopens.isClopen, IsClopen.isClosed
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
h : IsClopen s
⊢ (↑{ carrier := s, isClopen' := h : Clopens α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
h : IsClopen s
⊢ x ∈ { carrier := s, isClopen' := h : Clopens α } ↔ x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
⊢ (↑(s \ t) : Set α) = (↑s : Set α) \ (↑t : Set α)

Tactic:
rfl

Premises used: Set.diff, setOf, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
⊢ (↑(s ⇨ t) : Set α) = (↑s : Set α) ⇨ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Clopens α
⊢ (↑sᶜ : Set α) = (↑s : Set α)ᶜ

Tactic:
rfl

Premises used: setOf, Not, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Clopens α
t : Clopens β
x : α × β
⊢ x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
U : ι → Clopens α
⊢ (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
U : ι → Clopens α
a : ι
s : Finset ι
h : a ∉ s
IH : (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)
⊢ (↑((insert a s).sup U) : Set α) = ⋃ i ∈ insert a s, (↑(U i) : Set α)

Tactic:
simp [IH]
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (IH : (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)),
        (↑((Insert.insert a s).sup U) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(U i) : Set α)
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]

Premises used: Insert.insert
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (IH : (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)),
        (↑((Insert.insert a s).sup U) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(U i) : Set α)
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]

Premises used: Insert.insert
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Clopens α
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
simp [disjoint_iff, ← SetLike.coe_set_eq]

Premises used: disjoint_iff, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : IrreducibleCloseds α
h : s.carrier = t.carrier
mk :
  ∀ (carrier : Set α) (isIrreducible' : IsIrreducible carrier) (isClosed' : IsClosed[inst] carrier)
    (h :
      { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
        t.carrier),
    { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : IrreducibleCloseds α
carrier : Set α
isIrreducible' : IsIrreducible carrier
isClosed' : IsClosed[inst] carrier
h :
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
    t.carrier
mk :
  ∀ (carrier_1 : Set α) (isIrreducible'_1 : IsIrreducible carrier_1) (isClosed'_1 : IsClosed[inst] carrier_1)
    (h :
      { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
        { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 :
            IrreducibleCloseds α }.carrier),
    { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } =
      { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 }
⊢ { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } = t

Tactic:
cases t
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
carrier : Set α
isIrreducible' : IsIrreducible carrier
isClosed' : IsClosed[inst] carrier
carrier_1 : Set α
isIrreducible'_1 : IsIrreducible carrier_1
isClosed'_1 : IsClosed[inst] carrier_1
h :
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
    { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 :
        IrreducibleCloseds α }.carrier
⊢ { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } =
    { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : IrreducibleCloseds α
⊢ IsIrreducible (↑s : Set α)

Tactic:
s.isIrreducible'

Premises used: TopologicalSpace.IrreducibleCloseds.isIrreducible'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : IrreducibleCloseds α
⊢ IsClosed[inst] (↑s : Set α)

Tactic:
s.isClosed'

Premises used: TopologicalSpace.IrreducibleCloseds.isClosed'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : IrreducibleCloseds α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
h : IsIrreducible s
h' : IsClosed[inst] s
⊢ (↑{ carrier := s, isIrreducible' := h, isClosed' := h' : IrreducibleCloseds α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
x : α
⊢ Eq (α := IrreducibleCloseds α) { carrier := {x}, isIrreducible' := ⋯, isClosed' := ⋯ } {x}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
a b : α
⊢ Membership.mem (γ := IrreducibleCloseds α) {b} a ↔ a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
⊢ Function.Injective (β := IrreducibleCloseds α) fun (x : α) ↦ {x}

Tactic:
.of_comp (f := SetLike.coe) Set.singleton_injective

Premises used: Set.singleton_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
x y : α
⊢ Eq (α := IrreducibleCloseds α) {x} {y} ↔ x = y

Tactic:
singleton_injective.eq_iff

Premises used: Function.Injective.eq_iff, TopologicalSpace.IrreducibleCloseds.singleton_injective
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : Continuous[inst_1, inst] f
s : IrreducibleCloseds β
⊢ (↑(map f hf s) : Set α) = closure[inst] (f '' (↑s : Set β))

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : Continuous[inst_1, inst] f
⊢ Monotone (map f hf)

Tactic:
fun _ _ h_le => closure_mono <| Set.image_mono h_le

Premises used: Set.Mem, Set.image_mono, Monotone, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
a : (↑A : Set β) = (↑B : Set β)
⊢ A = B

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
⊢ closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))

Tactic:
replace h_images_eq : closure (f '' A) = closure (f '' B) := congr($h_images_eq)
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
a₁ : f ⁻¹' closure[inst] (f '' (↑A : Set β)) = (↑B : Set β)
a₂ : f ⁻¹' closure[inst] (f '' (↑B : Set β)) = (↑B : Set β)
a₃ : closure[inst_1] (↑B : Set β) = (↑B : Set β)
a₄ a₅ : (↑B : Set β) = (↑B : Set β)
⊢ (↑A : Set β) = (↑B : Set β)

Tactic:
rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]

Premises used: IsClosed.closure_eq, TopologicalSpace.IrreducibleCloseds.isClosed, Topology.IsInducing.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
⊢ StrictMono (map f ⋯)

Tactic:
Monotone.strictMono_of_injective (map_mono hf.continuous) (map_injective_of_isInducing hf)

Premises used: Monotone.strictMono_of_injective, TopologicalSpace.IrreducibleCloseds.map_injective_of_isInducing, TopologicalSpace.IrreducibleCloseds.map_mono, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
h₁ :
  ∀ (x : β),
    x ∈
        (↑((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
                  IrreducibleCloseds β })
              ((fun (T : IrreducibleCloseds β) ↦
                  (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                      (map f ⋯ T) ⋯ :
                    { x : IrreducibleCloseds α //
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
                V)) :
          Set β) ↔
      x ∈ (↑V : Set β)
⊢ (fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
        { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
          IrreducibleCloseds β })
      ((fun (T : IrreducibleCloseds β) ↦
          (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
              Membership.mem (γ := Set (IrreducibleCloseds α))
                {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
              (map f ⋯ T) ⋯ :
            { x : IrreducibleCloseds α //
              Membership.mem (γ := Set (IrreducibleCloseds α))
                {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
        V) =
    V

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
x : β
⊢ x ∈
      (↑((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
              { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
                IrreducibleCloseds β })
            ((fun (T : IrreducibleCloseds β) ↦
                (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                    Membership.mem (γ := Set (IrreducibleCloseds α))
                      {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                    (map f ⋯ T) ⋯ :
                  { x : IrreducibleCloseds α //
                    Membership.mem (γ := Set (IrreducibleCloseds α))
                      {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
              V)) :
        Set β) ↔
    x ∈ (↑V : Set β)

Tactic:
simp [h.isOpenMap.preimage_closure_image h.injective h.continuous _ V.isClosed]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.continuous, IsOpenMap.preimage_closure_image, TopologicalSpace.IrreducibleCloseds.isClosed, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)
a :
  ∀ (x : α),
    x ∈
        (↑(↑((fun (T : IrreducibleCloseds β) ↦
                    (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                        Membership.mem (γ := Set (IrreducibleCloseds α))
                          {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                        (map f ⋯ T) ⋯ :
                      { x : IrreducibleCloseds α //
                        Membership.mem (γ := Set (IrreducibleCloseds α))
                          {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
                  ((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                      { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
                        IrreducibleCloseds β })
                    V)) :
              IrreducibleCloseds α) :
          Set α) ↔
      x ∈ (↑(↑V : IrreducibleCloseds α) : Set α)
⊢ (fun (T : IrreducibleCloseds β) ↦
        (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
            Membership.mem (γ := Set (IrreducibleCloseds α)) {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty}
              x)
            (map f ⋯ T) ⋯ :
          { x : IrreducibleCloseds α //
            Membership.mem (γ := Set (IrreducibleCloseds α)) {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty}
              x }))
      ((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
          { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
            IrreducibleCloseds β })
        V) =
    V

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)
x : α
⊢ x ∈
      (↑(↑((fun (T : IrreducibleCloseds β) ↦
                  (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                      (map f ⋯ T) ⋯ :
                    { x : IrreducibleCloseds α //
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
                ((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                    { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
                      IrreducibleCloseds β })
                  V)) :
            IrreducibleCloseds α) :
        Set α) ↔
    x ∈ (↑(↑V : IrreducibleCloseds α) : Set α)

Tactic:
simp [closure_image_preimage_of_isPreirreducible f h.isOpenMap V V.2 V.1.2.2 V.1.3]

Premises used: Topology.IsOpenEmbedding.isOpenMap, closure_image_preimage_of_isPreirreducible, TopologicalSpace.IrreducibleCloseds.isIrreducible', SetLike.coe, And.right, TopologicalSpace.IrreducibleCloseds.isClosed', Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
⊢ LE.le.{u_2} (α := (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f ⋯ T) ⋯,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          a :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f ⋯ T) ⋯,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          b :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↔
    a ≤ b

Tactic:
⟨fun hle ↦ ?_, fun hle ↦ map_mono h.continuous hle⟩

Premises used: Topology.IsOpenEmbedding.continuous, Iff.intro, TopologicalSpace.IrreducibleCloseds.map_mono