awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have 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
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)
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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}
have rw : ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
Tactic: rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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}
have conv_lhs : f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
Tactic: conv_lhs => rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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}
⊢ f ⁻¹' {y} = ⋃ (i : Fin n), U i ∩ f ⁻¹' {y}
have conv_lhs₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : Fin n), U i ∩ f ⁻¹' {y}) (⋃ (i : Fin n), U i ∩ f ⁻¹' {y})
Tactic: conv_lhs => rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (hypothesis)
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
⊢ (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
have heq : 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]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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}
⊢ (↑n : ℕ∞) ≤ (f ⁻¹' {y}).encard
have rw : LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)
Tactic: rw [heq, Set.encard_iUnion_of_finite fun i j hij ↦ .inter_left _ (.inter_right _ <| hU3 hij)]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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), (U i ∩ f ⁻¹' {y}).encard)
have trans : LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ i : Fin n, 1)
Tactic: trans ∑ i : Fin n, 1
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)
have trans₁ : LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard)
Tactic: trans ∑ i : Fin n, 1
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
have rw : LE.le (α := ℕ∞) (∑ i : Fin n, 1) (∑ i : Fin n, (U i ∩ f ⁻¹' {y}).encard)
Tactic: rw [finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
have refine : ∀ (i : Fin n), y ∈ f '' U i
Tactic: refine Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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
⊢ y ∈ f '' U i
have h : f '' U i = Set.univ
Tactic: convert! Set.mem_univ y
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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
⊢ Finite.{u_1 + 1} (ConnectedComponents X)
have rw : ENat.card.{u_1} (ConnectedComponents X) < ⊤
Tactic: rw [← ENat.card_lt_top]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
have refine_1 : ∀ (i : ConnectedComponents Y),
  IsClopen.{u_1} (X := X) ((fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)
Tactic: refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
⊢ Finite.{u_1 + 1} (ConnectedComponents X)
have 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})
Tactic: refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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})
⊢ Finite.{u_1 + 1} (ConnectedComponents X)
have 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
Tactic: refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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))
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (i : ConnectedComponents Y),
      (fun (y : ConnectedComponents Y) ↦ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) i)
    Set.univ
have refine_3 : ∀ (x : X), ∃ (i : ConnectedComponents Y), x ∈ f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {i}
Tactic: rw [Set.iUnion_eq_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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
⊢ Finite.{u_1 + 1} (ConnectedComponents X)
have suffices : ∀ (y : ConnectedComponents Y),
  Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
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⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {y}) : Type u_1))
have obtain : ∀ (y : Y),
  Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {mk y}) : Type u_1))
Tactic: obtain ⟨y, rfl⟩ := surjective_coe y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (hypothesis)
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
⊢ Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {mk y}) : Type u_1))
have this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
Tactic: have := isConnected_iff_connectedSpace.mp (isConnected_connectedComponent (x := y))
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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 ⁻¹' Set.preimage (β := ConnectedComponents Y) mk {mk y}) : Type u_1))
have rw : Finite.{u_1 + 1} (ConnectedComponents (↑(f ⁻¹' connectedComponent y) : Type u_1))
Tactic: rw [connectedComponents_preimage_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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))
have refine : ((connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y sorry}).Finite
Tactic: refine IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
    (hf₁.restrictPreimage (connectedComponent y)) (hf₂.restrictPreimage (connectedComponent y))
    (y := ⟨y, mem_connectedComponent⟩) ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
⊢ ((connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯}).Finite
have 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 sorry}).Finite
Tactic: rw [← Set.finite_image_iff Subtype.val_injective.injOn]
-- Lean 4 proof step from Mathlib.Topology.Connected.CardComponents (goal)
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)
⊢ (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
have h₁ : Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' connectedComponent y) ''
    (connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y sorry} =
  f ⁻¹' {y}
Tactic: convert! h y
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsConnected s ↔ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1 : ∀ (hs : IsConnected s), ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
refine_1 : ∀ (hs : IsConnected s), ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
⊢ IsConnected s ↔ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_2 : (∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t) → IsConnected s
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
⊢ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1 : ∀ (i : ι) (x : X i) (hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s),
  ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
Tactic: obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s
⊢ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have this : s ⊆ range (mk (β := fun (i : ι) ↦ X i) i)
Tactic: have : s ⊆ range (Sigma.mk i) :=
      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsPreconnected s ↔ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1 : ∀ (hs : IsPreconnected s), ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
refine_1 :
  ∀ (hs : IsPreconnected s), ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
⊢ IsPreconnected s ↔ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_2 : (∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t) → IsPreconnected s
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1 : ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅),
  ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ ∅ = mk (β := fun (i : ι) ↦ X i) i '' t
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
refine_1 :
  ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅),
    ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ ∅ = mk (β := fun (i : ι) ↦ X i) i '' t
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1₁ : ∀ (h : s.Nonempty), ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
have refine_1 : ∀ (a : ι) (t : Set (X a)) (ht : IsConnected t) (hs : IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t))
  (h : (mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty),
  ∃ (i : ι) (t_1 : Set (X i)),
    IsPreconnected t_1 ∧ mk (β := fun (i : ι) ↦ X i) a '' t = mk (β := fun (i : ι) ↦ X i) i '' t_1
Tactic: obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsConnected s ↔ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1 : ∀ (hs : IsConnected s), (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
refine_1 :
  ∀ (hs : IsConnected s), (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
⊢ IsConnected s ↔ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_2 : ((∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t) → IsConnected s
Tactic: refine ⟨fun hs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1 : ∀ (x : α) (hx : inl x ∈ s), (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
Tactic: obtain ⟨x | x, hx⟩ := hs.nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
refine_1 :
  ∀ (x : α) (hx : inl x ∈ s),
    (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1₁ : ∀ (x : β) (hx : inr x ∈ s), (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
Tactic: obtain ⟨x | x, hx⟩ := hs.nonempty