awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
suffices :
  ∀ {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
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
suffices h : ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ i, IsClopen (U i)) (hU₂ : ∀ i, (U i).Nonempty)
      (hU₃ : Pairwise (Disjoint on U)) (hU₄ : ⋃ i, U i = Set.univ),
      n ≤ (f ⁻¹' {y}).encard by
    obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)
    · cases nonempty_fintype (ConnectedComponents X)
      simp only [ENat.card_eq_coe_fintype_card]
      refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_
      · exact (isClopen_discrete _).preimage continuous_coe
      · exact (Set.singleton_nonempty _).preimage surjective_coe
      · simp [← Set.preimage_iUnion]
    · simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
      intro m
      obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)
      exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
rw : ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
| f ⁻¹' {y}

Tactic:
rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]

Premises used: Set.univ_inter, Set.iUnion_inter, Set.preimage, Singleton.singleton
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
conv_lhs : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
conv_lhs₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i ∩ f ⁻¹' {y}) (⋃ (i : Fin n), U i ∩ f ⁻¹' {y})
⊢ f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}

Tactic:
conv_lhs => rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]

Premises used: Set.univ_inter, Set.iUnion_inter, Set.preimage, Singleton.singleton
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
⊢ f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}

Tactic:
have heq : f ⁻¹' {y} = ⋃ i, (U i ∩ f ⁻¹' {y}) := by
    conv_lhs => rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
rw : LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)
⊢ (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard

Tactic:
rw [heq, Set.encard_iUnion_of_finite fun i j hij ↦ .inter_left _ (.inter_right _ <| hU3 hij)]

Premises used: Disjoint.inter_right, Set.encard_iUnion_of_finite, Disjoint.inter_left
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
trans : LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ i : Fin n, 1)
trans₁ : LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)

Tactic:
trans ∑ i : Fin n, 1

Premises used: Fin
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ i : Fin n, 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
rw : LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ i : Fin n, (U i ∩ f ⁻¹' {y}).encard)
⊢ LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)

Tactic:
rw [finsum_eq_sum_of_fintype]

Premises used: finsum_eq_sum_of_fintype
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
⊢ LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ i : Fin n, (U i ∩ f ⁻¹' {y}).encard)

Tactic:
Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)

Premises used: Iff.mpr, Fintype.sum_mono, Set.one_le_encard_iff_nonempty
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
refine : ∀ (i : Fin n), y ∈ f '' U i
⊢ LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ i : Fin n, (U i ∩ f ⁻¹' {y}).encard)

Tactic:
refine Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)

Premises used: Iff.mpr, Fintype.sum_mono, Set.one_le_encard_iff_nonempty
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
i : Fin n
⊢ Membership.mem (γ := Set Y) Set.univ y

Tactic:
Set.mem_univ y

Premises used: Set.mem_univ
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
i : Fin n
h : f '' U i = Set.univ
⊢ y ∈ f '' U i

Tactic:
convert! Set.mem_univ y

Premises used: Set.mem_univ
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
i : Fin n
⊢ f '' U i = Set.univ

Tactic:
IsClopen.eq_univ ⟨hf₂ _ (hU1 i).1, hf₁ _ (hU1 i).2⟩ ((hU2 i).image f)

Premises used: IsClopen.eq_univ, And.right, And.left, Set.Nonempty.image, And.intro
-- 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
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i) Set.univ
heq : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
i : Fin n
⊢ f '' U i = Set.univ

Tactic:
exact IsClopen.eq_univ ⟨hf₂ _ (hU1 i).1, hf₁ _ (hU1 i).2⟩ ((hU2 i).image f)

Premises used: IsClopen.eq_univ, And.right, And.left, Set.Nonempty.image, And.intro
-- 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
hy : (f ⁻¹' {y}).Finite
rw : ENat.card.{u_1} (ConnectedComponents X) < ⊤
⊢ Finite.{u_1 + 1} (ConnectedComponents X)

Tactic:
rw [← ENat.card_lt_top]

Premises used: ENat.card_lt_top
-- 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
hy : (f ⁻¹' {y}).Finite
⊢ ENat.card.{u_1} (ConnectedComponents X) < ⊤

Tactic:
lt_of_le_of_lt (hf₁.enatCard_connectedComponents_le_encard_preimage_singleton hf₂ y)
    hy.encard_lt_top

Premises used: lt_of_le_of_lt, Set.Finite.encard_lt_top, IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton
-- 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
hy : (f ⁻¹' {y}).Finite
⊢ ENat.card.{u_1} (ConnectedComponents X) < ⊤

Tactic:
exact lt_of_le_of_lt (hf₁.enatCard_connectedComponents_le_encard_preimage_singleton hf₂ y)
    hy.encard_lt_top

Premises used: lt_of_le_of_lt, Set.Finite.encard_lt_top, IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ Finite.{u_1 + 1} (ConnectedComponents X)

Tactic:
.of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm

Premises used: Finite.of_equiv, ConnectedComponents.equivOfIsClopen, Equiv.symm
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
refine_1 :
  ∀ (i : ConnectedComponents Y),
    IsClopen.{u_1} (X := X)
      ((fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)
refine_2 :
  Pairwise.{u_2} (α := ConnectedComponents Y)
    (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set X) Disjoint fun (y : ConnectedComponents Y) ↦
      f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y})
refine_3 :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (i : ConnectedComponents Y),
      (fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)
    Set.univ
⊢ Finite.{u_1 + 1} (ConnectedComponents X)

Tactic:
refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ ∀ (i : ConnectedComponents Y),
    IsClopen.{u_1} (X := X)
      ((fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)

Tactic:
fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)

Premises used: Set.Mem, ConnectedComponents.mk, Continuous.comp, isClopen_discrete, setOf, ConnectedComponents.continuous_coe, Set.preimage, Set.singleton, Singleton.singleton, 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ ∀ (i : ConnectedComponents Y),
    IsClopen.{u_1} (X := X)
      ((fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)

Tactic:
exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)

Premises used: Continuous.comp, isClopen_discrete, ConnectedComponents.continuous_coe, Singleton.singleton, 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
i j : ConnectedComponents Y
hij : i ≠ j
⊢ Disjoint (α := Set (ConnectedComponents Y)) {i} {j}

Tactic:
simpa
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ Pairwise.{u_2} (α := ConnectedComponents Y)
    (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set X) Disjoint fun (y : ConnectedComponents Y) ↦
      f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y})

Tactic:
exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f

Premises used: ConnectedComponents.mk, 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
refine_3 : ∀ (x : X), ∃ (i : ConnectedComponents Y), x ∈ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {i}
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (i : ConnectedComponents Y),
      (fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)
    Set.univ

Tactic:
rw [Set.iUnion_eq_univ_iff]

Premises used: Set.iUnion_eq_univ_iff
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ ∀ (x : X), ∃ (i : ConnectedComponents Y), x ∈ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {i}

Tactic:
fun x ↦ ⟨mk (f x), rfl⟩

Premises used: ConnectedComponents.mk, Exists.intro, rfl
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h_1 : ∀ (y : Y), (f ⁻¹' {y}).Finite
h :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ ∀ (x : X), ∃ (i : ConnectedComponents Y), x ∈ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {i}

Tactic:
exact fun x ↦ ⟨mk (f x), rfl⟩
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
suffices :
  ∀ (y : ConnectedComponents Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
⊢ Finite.{u_1 + 1} (ConnectedComponents X)

Tactic:
suffices h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents (f ⁻¹' mk ⁻¹' {y})) by
    refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
    · exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)
    · exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f
    · rw [Set.iUnion_eq_univ_iff]
      exact fun x ↦ ⟨mk (f x), rfl⟩
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : ConnectedComponents Y
obtain :
  ∀ (y : Y),
    Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {mk y}) : Type u_1))
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))

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

Premises used: ConnectedComponents.surjective_coe, rfl
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
⊢ ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)

Tactic:
have := isConnected_iff_connectedSpace.mp (isConnected_connectedComponent (x := y))
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
rw : Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' connectedComponent y) : Type u_1))
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {mk y}) : Type u_1))

Tactic:
rw [connectedComponents_preimage_singleton]

Premises used: connectedComponents_preimage_singleton
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' connectedComponent y) : Type u_1))

Tactic:
IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
    (hf₁.restrictPreimage (connectedComponent y)) (hf₂.restrictPreimage (connectedComponent y))
    (y := ⟨y, mem_connectedComponent⟩) ?_

Premises used: IsOpenMap.restrictPreimage, IsClosedMap.restrictPreimage, IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace, connectedComponent
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
refine :
  ((connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯}).Finite
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' connectedComponent y) : Type u_1))

Tactic:
refine IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
    (hf₁.restrictPreimage (connectedComponent y)) (hf₂.restrictPreimage (connectedComponent y))
    (y := ⟨y, mem_connectedComponent⟩) ?_

Premises used: IsOpenMap.restrictPreimage, IsClosedMap.restrictPreimage, IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace, connectedComponent
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
rw :
  (Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' connectedComponent y) ''
      (connectedComponent y).restrictPreimage f ⁻¹'
        {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯}).Finite
⊢ ((connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯}).Finite

Tactic:
rw [← Set.finite_image_iff Subtype.val_injective.injOn]

Premises used: Subtype.val_injective, Function.Injective.injOn, Set.finite_image_iff
-- 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 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
⊢ (f ⁻¹' {y}).Finite

Tactic:
h y