awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ PreconnectedSpace α

Tactic:
exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
rw : IsPreconnected (connectedComponent (Classical.choice hα))
⊢ IsPreconnected.{u} (α := α) univ

Tactic:
rw [← h (Classical.choice hα)]

Premises used: Classical.choice
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Tactic:
isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Tactic:
exact isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ PreconnectedSpace α

Tactic:
exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
h : PreconnectedSpace X
x : X
⊢ connectedComponent x = univ

Tactic:
preconnectedSpace_iff_connectedComponent.mp h x

Premises used: Iff.mp, preconnectedSpace_iff_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
inst_3 : PreconnectedSpace β
rw : IsPreconnected (SProd.sprod (α := Set α) (β := Set β) univ univ)
⊢ IsPreconnected (α := α × β) univ

Tactic:
rw [← univ_prod_univ]

Premises used: Set.univ_prod_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
inst_3 : PreconnectedSpace β
⊢ IsPreconnected (SProd.sprod (α := Set α) (β := Set β) univ univ)

Tactic:
isPreconnected_univ.prod isPreconnected_univ

Premises used: PreconnectedSpace.isPreconnected_univ, IsPreconnected.prod
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
inst_3 : PreconnectedSpace β
⊢ IsPreconnected (SProd.sprod (α := Set α) (β := Set β) univ univ)

Tactic:
exact isPreconnected_univ.prod isPreconnected_univ

Premises used: PreconnectedSpace.isPreconnected_univ, IsPreconnected.prod
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : ConnectedSpace α
inst_3 : ConnectedSpace β
⊢ ConnectedSpace (α × β)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, ConnectedSpace.mk
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), PreconnectedSpace.{u_2} (X i)
rw : IsPreconnected (α := (i : ι) → X i) (pi (α := X) univ fun (i : ι) ↦ univ)
⊢ IsPreconnected (α := (i : ι) → X i) univ

Tactic:
rw [← pi_univ univ]

Premises used: Set.univ, Set.pi_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), PreconnectedSpace.{u_2} (X i)
⊢ IsPreconnected (α := (i : ι) → X i) (pi (α := X) univ fun (i : ι) ↦ univ)

Tactic:
isPreconnected_univ_pi fun i => isPreconnected_univ

Premises used: PreconnectedSpace.isPreconnected_univ, isPreconnected_univ_pi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), PreconnectedSpace.{u_2} (X i)
⊢ IsPreconnected (α := (i : ι) → X i) (pi (α := X) univ fun (i : ι) ↦ univ)

Tactic:
exact isPreconnected_univ_pi fun i => isPreconnected_univ

Premises used: PreconnectedSpace.isPreconnected_univ, isPreconnected_univ_pi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), ConnectedSpace.{u_2} (X i)
⊢ ConnectedSpace ((i : ι) → X i)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, ConnectedSpace.mk
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u
inst_1 : TopologicalSpace α
inst_2 : PreirreducibleSpace α
⊢ PreconnectedSpace α

Tactic:
⟨isPreirreducible_univ.isPreconnected⟩

Premises used: PreirreducibleSpace.isPreirreducible_univ, PreconnectedSpace.mk, IsPreirreducible.isPreconnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
rwa : IsPreconnected.{u} (α := α) (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ)
rwa₁ : IsPreconnected.{u} (α := α) (range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
rwa₂ rwa₃ rwa₄ rwa₅ : IsPreconnected s
⊢ IsPreconnected.{u} (α := (↑s : Type u)) univ

Tactic:
rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]

Premises used: Topology.IsInducing.isPreconnected_image, Set.image_univ, Subtype.range_val, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : PreconnectedSpace.{u} (↑s : Type u)
⊢ IsPreconnected s

Tactic:
simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn

Premises used: Continuous.continuousOn, continuous_subtype_val, IsPreconnected.image, PreconnectedSpace.isPreconnected_univ, Subtype.val
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ IsConnected s ↔ ConnectedSpace.{u} (↑s : Type u)

Tactic:
⟨Subtype.connectedSpace, fun h =>
    ⟨nonempty_subtype.mp h.2, isPreconnected_iff_preconnectedSpace.mpr h.1⟩⟩

Premises used: Iff.mpr, isPreconnected_iff_preconnectedSpace, ConnectedSpace.toPreconnectedSpace, Subtype.connectedSpace, ConnectedSpace.toNonempty, nonempty_subtype, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
inl : ∀ (hy : Finite.{u_1 + 1} (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
inr : ∀ (hy : Infinite.{u_1 + 1} (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)

Premises used: finite_or_infinite, ConnectedComponents
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
inl : ∀ (val : Fintype (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
cases nonempty_fintype (ConnectedComponents X)

Premises used: nonempty_fintype, ConnectedComponents
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
inl : (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
simp only [ENat.card_eq_coe_fintype_card]

Premises used: ENat.card_eq_coe_fintype_card
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
i j : Fin (Fintype.card.{u_1} (ConnectedComponents X))
hij : i ≠ j
⊢ Disjoint (α := Set (ConnectedComponents X))
    (singleton (α := ConnectedComponents X)
      ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
            (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
          i :
        ConnectedComponents X))
    (singleton (α := ConnectedComponents X)
      ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
            (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
          j :
        ConnectedComponents X))

Tactic:
simp [hij]
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
inl :
  ∀ (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))),
    IsClopen.{u_1} (X := X)
      ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
          (Set.preimage (β := ConnectedComponents X) mk
              (singleton (α := ConnectedComponents X)
                ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                      (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                    i :
                  ConnectedComponents X)) :
            Set X))
        i)
inl₁ :
  ∀ (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))),
    Set.Nonempty.{u_1} (α := X)
      ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
          (Set.preimage (β := ConnectedComponents X) mk
              (singleton (α := ConnectedComponents X)
                ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                      (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                    i :
                  ConnectedComponents X)) :
            Set X))
        i)
inl₂ :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))),
      (fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
          (Set.preimage (β := ConnectedComponents X) mk
              (singleton (α := ConnectedComponents X)
                ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                      (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                    i :
                  ConnectedComponents X)) :
            Set X))
        i)
    Set.univ
⊢ (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard

Tactic:
refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_

Premises used: ConnectedComponents.mk, Fintype.equivFin, Set.preimage, Equiv.symm, Singleton.singleton, ConnectedComponents, DFunLike.coe, Disjoint.preimage
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
i : Fin (Fintype.card.{u_1} (ConnectedComponents X))
⊢ IsClopen.{u_1} (X := X)
    ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
        (Set.preimage (β := ConnectedComponents X) mk
            (singleton (α := ConnectedComponents X)
              ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                    (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                  i :
                ConnectedComponents X)) :
          Set X))
      i)

Tactic:
(isClopen_discrete _).preimage continuous_coe

Premises used: isClopen_discrete, ConnectedComponents.continuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
i : Fin (Fintype.card.{u_1} (ConnectedComponents X))
⊢ IsClopen.{u_1} (X := X)
    ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
        (Set.preimage (β := ConnectedComponents X) mk
            (singleton (α := ConnectedComponents X)
              ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                    (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                  i :
                ConnectedComponents X)) :
          Set X))
      i)

Tactic:
exact (isClopen_discrete _).preimage continuous_coe

Premises used: isClopen_discrete, ConnectedComponents.continuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
i : Fin (Fintype.card.{u_1} (ConnectedComponents X))
⊢ Set.Nonempty.{u_1} (α := X)
    ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
        (Set.preimage (β := ConnectedComponents X) mk
            (singleton (α := ConnectedComponents X)
              ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                    (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                  i :
                ConnectedComponents X)) :
          Set X))
      i)

Tactic:
(Set.singleton_nonempty _).preimage surjective_coe

Premises used: Set.singleton_nonempty, ConnectedComponents.surjective_coe, Set.Nonempty.preimage
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
i : Fin (Fintype.card.{u_1} (ConnectedComponents X))
⊢ Set.Nonempty.{u_1} (α := X)
    ((fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
        (Set.preimage (β := ConnectedComponents X) mk
            (singleton (α := ConnectedComponents X)
              ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                    (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                  i :
                ConnectedComponents X)) :
          Set X))
      i)

Tactic:
exact (Set.singleton_nonempty _).preimage surjective_coe

Premises used: Set.singleton_nonempty, ConnectedComponents.surjective_coe, Set.Nonempty.preimage
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Finite.{u_1 + 1} (ConnectedComponents X)
val : Fintype (ConnectedComponents X)
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))),
      (fun (i : Fin (Fintype.card.{u_1} (ConnectedComponents X))) ↦
          (Set.preimage (β := ConnectedComponents X) mk
              (singleton (α := ConnectedComponents X)
                ((Equiv.symm (Fintype.equivFin (ConnectedComponents X)) :
                      (a : Fin (Fintype.card (ConnectedComponents X))) → ConnectedComponents X)
                    i :
                  ConnectedComponents X)) :
            Set X))
        i)
    Set.univ

Tactic:
simp [← Set.preimage_iUnion]

Premises used: Set.preimage_iUnion
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Infinite.{u_1 + 1} (ConnectedComponents X)
inr : ∀ (m : ℕ), (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]

Premises used: ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Infinite.{u_1 + 1} (ConnectedComponents X)
m : ℕ
⊢ 0 < m + 1

Tactic:
simp
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Infinite.{u_1 + 1} (ConnectedComponents X)
m : ℕ
inr :
  ∀ (U : Fin (m + 1) → Set X) (hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)) (hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty)
    (hU3 : Pairwise (Disjoint on U)) (hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin (m + 1)), U i) Set.univ),
    (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard
⊢ (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard

Tactic:
obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)

Premises used: HAdd.hAdd, ConnectedComponents.exists_fun_isClopen_of_infinite, OfNat.ofNat
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Infinite.{u_1 + 1} (ConnectedComponents X)
m : ℕ
U : Fin (m + 1) → Set X
hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)
hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin (m + 1)), U i) Set.univ
⊢ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑(m + 1) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ (i : Fin n), IsClopen (U i)) (hU₂ : ∀ (i : Fin n), (U i).Nonempty)
    (hU₃ : Pairwise (Disjoint on U)) (hU₄ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ),
    (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
hy : Infinite.{u_1 + 1} (ConnectedComponents X)
m : ℕ
U : Fin (m + 1) → Set X
hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)
hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin (m + 1)), U i) Set.univ
⊢ (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard

Tactic:
exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)

Premises used: le_trans