awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
rw : ∀ (x : ConnectedComponents α), connectedComponent x = {x}
⊢ TotallyDisconnectedSpace.{u} (ConnectedComponents α)

Tactic:
rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]

Premises used: totallyDisconnectedSpace_iff_connectedComponent_singleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}

Tactic:
ConnectedComponents.surjective_coe.forall.2 fun x => ?_

Premises used: Iff.mpr, Function.Surjective.forall, ConnectedComponents.surjective_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
refine : ∀ (x : α), Eq (α := Set (ConnectedComponents α)) (connectedComponent (mk x)) {mk x}
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}

Tactic:
refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_

Premises used: Iff.mpr, Function.Surjective.forall, ConnectedComponents.surjective_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x : α
h_fibers : ∀ (y : ConnectedComponents α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {y})
⊢ Eq (α := Set (ConnectedComponents α)) (connectedComponent (mk x)) {mk x}

Tactic:
rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ←
    connectedComponents_preimage_singleton, image_preimage_eq _ ConnectedComponents.surjective_coe]

Premises used: Topology.IsCoinducing.image_connectedComponent, connectedComponents_preimage_singleton, ConnectedComponents.surjective_coe, Set.image_preimage_eq, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ ∀ (y : ConnectedComponents α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {y})

Tactic:
ConnectedComponents.surjective_coe.forall.2 fun y => ?_

Premises used: Iff.mpr, Function.Surjective.forall, ConnectedComponents.surjective_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x : α
h_fibers : ∀ (y : α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {mk y})
⊢ ∀ (y : ConnectedComponents α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {y})

Tactic:
refine ConnectedComponents.surjective_coe.forall.2 fun y => ?_

Premises used: Iff.mpr, Function.Surjective.forall, ConnectedComponents.surjective_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x y : α
h_fibers : IsConnected (connectedComponent y)
⊢ IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {mk y})

Tactic:
rw [connectedComponents_preimage_singleton]

Premises used: connectedComponents_preimage_singleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x y : α
⊢ IsConnected (connectedComponent y)

Tactic:
isConnected_connectedComponent

Premises used: isConnected_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
x y : α
⊢ IsConnected (connectedComponent y)

Tactic:
exact isConnected_connectedComponent

Premises used: isConnected_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
x : α
⊢ hf.connectedComponentsMap (ConnectedComponents.mk x) = ConnectedComponents.mk (f x)

Tactic:
rfl

Premises used: Quotient.liftOn', ConnectedComponents.mk, Continuous.connectedComponentsLift, Continuous.connectedComponentsMap, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
h : Continuous[inst, inst_1] f
⊢ Continuous h.connectedComponentsMap

Tactic:
Continuous.connectedComponentsLift_continuous (ConnectedComponents.continuous_coe.comp h)

Premises used: Continuous.comp, ConnectedComponents.continuous_coe, Continuous.connectedComponentsMap, Continuous.connectedComponentsLift_continuous
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
rw : IsCoinducing (⋯.connectedComponentsMap ∘ ConnectedComponents.mk)
⊢ IsCoinducing ⋯.connectedComponentsMap

Tactic:
rw [← ConnectedComponents.isQuotientMap_coe.isCoinducing.of_comp_iff]

Premises used: Topology.IsCoinducing.of_comp_iff, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing (⋯.connectedComponentsMap ∘ ConnectedComponents.mk)

Tactic:
ConnectedComponents.isQuotientMap_coe.isCoinducing.comp hf

Premises used: Quotient.liftOn', ConnectedComponents.mk, Topology.IsCoinducing.comp, Continuous.connectedComponentsLift, Continuous.connectedComponentsMap, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing (⋯.connectedComponentsMap ∘ ConnectedComponents.mk)

Tactic:
exact ConnectedComponents.isQuotientMap_coe.isCoinducing.comp hf

Premises used: Topology.IsCoinducing.comp, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
h : Surjective f
⊢ Surjective hf.connectedComponentsMap

Tactic:
Quotient.lift_surjective _ _ <| ConnectedComponents.surjective_coe.comp h

Premises used: Quotient.liftOn', ConnectedComponents.surjective_coe, Quotient.lift_surjective, Quotient, Continuous.connectedComponentsLift, Continuous.connectedComponentsMap, Function.Surjective.comp, ConnectedComponents
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
⊢ Bijective ⋯.connectedComponentsMap

Tactic:
⟨fun x y h ↦ ?_, Continuous.connectedComponentsMap_surjective _ fun y ↦ (hf' y).nonempty⟩

Premises used: Continuous.connectedComponentsMap_surjective, IsConnected.nonempty, And.intro, Function.Bijective
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
refine : ∀ (x y : ConnectedComponents α) (h : ⋯.connectedComponentsMap x = ⋯.connectedComponentsMap y), x = y
⊢ Bijective ⋯.connectedComponentsMap

Tactic:
refine ⟨fun x y h ↦ ?_, Continuous.connectedComponentsMap_surjective _ fun y ↦ (hf' y).nonempty⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
x y : ConnectedComponents α
h : ⋯.connectedComponentsMap x = ⋯.connectedComponentsMap y
obtain :
  ∀ (x : α) (h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap y),
    ConnectedComponents.mk x = y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
y : ConnectedComponents α
x : α
h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap y
obtain :
  ∀ (y : α)
    (h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap (ConnectedComponents.mk y)),
    Eq (α := ConnectedComponents α) (ConnectedComponents.mk x) (ConnectedComponents.mk y)
⊢ ConnectedComponents.mk x = y

Tactic:
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
x y : α
h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap (ConnectedComponents.mk y)
⊢ Eq (α := ConnectedComponents α) (ConnectedComponents.mk x) (ConnectedComponents.mk y)

Tactic:
simp_all [← hf.preimage_connectedComponent hf']

Premises used: Topology.IsCoinducing.preimage_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology Y
s : Set α
hs : IsPreconnected s
f : α → Y
hf : ContinuousOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
(hs.image f hf).subsingleton (mem_image_of_mem f hx) (mem_image_of_mem f hy)

Premises used: IsPreconnected.image, IsPreconnected.subsingleton, Set.mem_image_of_mem
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology Y
hp : PreconnectedSpace α
f : α → Y
hf : Continuous[inst, inst_1] f
x y : α
⊢ f x = f y

Tactic:
IsPreconnected.constant hp.isPreconnected_univ (Continuous.continuousOn hf) trivial trivial

Premises used: Continuous.continuousOn, trivial, IsPreconnected.constant, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
this : F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      (↑(F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx)) : β) =
        (↑(F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)) : β)),
    f x = f y
⊢ f x = f y

Tactic:
rwa [← Subtype.coe_inj] at this

Premises used: Subtype.coe_inj
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
suffices : F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
⊢ f x = f y

Tactic:
suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
rw :
  ∀ (hT : DiscreteTopology.{u_3} (↑T : Type u_3)) {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) {x y : α}
    (hx : x ∈ S) (hy : y ∈ S),
    let F := MapsTo.restrict f S T hTm;
    F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
⊢ F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)

Tactic:
rw [isDiscrete_iff_discreteTopology] at hT

Premises used: isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : DiscreteTopology.{u_3} (↑T : Type u_3)
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
⊢ F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)

Tactic:
(isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.mapsToRestrict _)

Premises used: isPreconnected_iff_preconnectedSpace, Iff.mp, ContinuousOn.mapsToRestrict, PreconnectedSpace.constant
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : DiscreteTopology.{u_3} (↑T : Type u_3)
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
⊢ F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)

Tactic:
exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.mapsToRestrict _)

Premises used: isPreconnected_iff_preconnectedSpace, Iff.mp, ContinuousOn.mapsToRestrict, PreconnectedSpace.constant
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
inl : ∀ (hS : IsPreconnected.{u} (α := α) ∅) (hc : ContinuousOn f ∅) (hTm : MapsTo f ∅ T), ∃ y ∈ T, EqOn f (const α y) ∅
inr : ∀ (x : α) (hx : x ∈ S), ∃ y ∈ T, EqOn f (const α y) S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hne : T.Nonempty
hS : IsPreconnected.{u} (α := α) ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

Tactic:
hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩

Premises used: Exists.imp, And.intro, Function.const, Set.eqOn_empty
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hne : T.Nonempty
hS : IsPreconnected.{u} (α := α) ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

Tactic:
exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩

Premises used: Exists.imp
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hT hc hTm hx' hx⟩

Premises used: IsPreconnected.constant_of_mapsTo, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hT hc hTm hx' hx⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsRetrocompact.{u_2} (X := X) ∅

Tactic:
simp [IsRetrocompact]

Premises used: IsRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsRetrocompact.{u_2} (X := X) Set.univ

Tactic:
simp +contextual [IsRetrocompact]

Premises used: IsRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
a : X
⊢ IsRetrocompact (X := X) {a}

Tactic:
fun _ _ _ ↦ Subsingleton.singleton_inter.isCompact

Premises used: Set.Subsingleton.singleton_inter, IsRetrocompact, Set.Subsingleton.isCompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsRetrocompact s
ht : IsRetrocompact t
⊢ IsRetrocompact (s ∪ t)

Tactic:
fun _U hUcomp hUopen ↦ union_inter_distrib_right .. ▸ (hs hUcomp hUopen).union (ht hUcomp hUopen)

Premises used: IsRetrocompact, Eq.rec, IsCompact.union, Eq.symm, Set.union_inter_distrib_right
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ SupClosed.{u_2} (α := Set X) {s : Set X | IsRetrocompact s}

Tactic:
fun _s hs _t ht ↦ hs.union ht

Premises used: Set.Mem, IsRetrocompact, setOf, SupClosed, IsRetrocompact.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)
⊢ IsRetrocompact (Finset.sup ∅ t)

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
cons : IsRetrocompact (t i ⊔ s.sup t)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)

Tactic:
rw [Finset.sup_cons]

Premises used: Finset.sup_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊔ s.sup t)

Tactic:
exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Premises used: Finset.forall_of_forall_cons, IsRetrocompact.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.sup ∅ t)
cons :
  ∀ (i : ι) (s : Finset ι) (ih : i ∉ s) (hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t))
    (ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)), IsRetrocompact ((Finset.cons i s ih).sup t)
⊢ IsRetrocompact (s.sup t)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Premises used: IsRetrocompact.empty, Finset.forall_of_forall_cons, IsRetrocompact.union, Finset.sup_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
rw : IsRetrocompact (s.sup t)
⊢ IsRetrocompact (s.sup' hs t)

Tactic:
rw [Finset.sup'_eq_sup]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
.finsetSup ht

Premises used: IsRetrocompact.finsetSup
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
exact .finsetSup ht
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsRetrocompact (f i)
⊢ IsRetrocompact.{u_2} (X := X) (⋃ (i : ι), f i)

Tactic:
supClosed_isRetrocompact.iSup_mem .empty hf

Premises used: Set.Mem, IsRetrocompact, SupClosed.iSup_mem, setOf, IsRetrocompact.empty, _private.0.supClosed_isRetrocompact, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsRetrocompact s
⊢ IsRetrocompact (⋃₀ S)

Tactic:
supClosed_isRetrocompact.sSup_mem hS .empty hS'

Premises used: Set.Mem, IsRetrocompact, setOf, Set.sUnion, IsRetrocompact.empty, _private.0.supClosed_isRetrocompact, SupClosed.sSup_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
f : ι → Set X
t : Set ι
ht : t.Finite
hf : ∀ i ∈ t, IsRetrocompact (f i)
⊢ IsRetrocompact.{u_2} (X := X) (⋃ i ∈ t, f i)

Tactic:
supClosed_isRetrocompact.biSup_mem ht .empty hf

Premises used: Set.Mem, IsRetrocompact, setOf, IsRetrocompact.empty, SupClosed.biSup_mem, _private.0.supClosed_isRetrocompact, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : T2Space X
hs : IsRetrocompact s
ht : IsRetrocompact t
⊢ IsRetrocompact (s ∩ t)

Tactic:
fun _U hUcomp hUopen ↦ inter_inter_distrib_right .. ▸ (hs hUcomp hUopen).inter (ht hUcomp hUopen)

Premises used: IsCompact.inter, Set.inter_inter_distrib_right, IsRetrocompact, Eq.rec, Eq.symm
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ InfClosed.{u_2} (α := Set X) {s : Set X | IsRetrocompact s}

Tactic:
fun _s hs _t ht ↦ hs.inter ht

Premises used: Set.Mem, IsRetrocompact, setOf, IsRetrocompact.inter, InfClosed
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
t : ι → Set X
ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)
⊢ IsRetrocompact (Finset.inf ∅ t)

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
cons : IsRetrocompact (t i ⊓ s.inf t)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]

Premises used: Finset.inf_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp