awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆ connectedComponentIn F x
have this₁ : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x sorry)
Tactic: have := this.subset_connectedComponent h2xs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆ connectedComponentIn F x
have rw : s ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x sorry)
Tactic: rw [connectedComponentIn_eq_image (hsF hxs)]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
have refine : s ⊆
  image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
Tactic: refine Subset.trans ?_ (image_mono this)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆
    image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
have rw : s ⊆ F ∩ s
Tactic: rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
rw : s ⊆ F ∩ s
⊢ s ⊆
    image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
have rw₁ : s ⊆ s
Tactic: rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x = connectedComponentIn F y
have hx : x ∈ F
Tactic: have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y
have simp_rw : ∀ (h : y ∈ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)),
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F y
Tactic: simp_rw [connectedComponentIn_eq_image hx] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
hx : x ∈ F
h : y ∈ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F y
have obtain : ∀ (y : α) (hy : y ∈ F)
  (h2y : Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy ∈ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)),
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy) : α)
Tactic: obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy ∈ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy) : α)
have simp_rw : Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
  connectedComponentIn F y
Tactic: simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy ∈ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)
simp_rw simp_rw₁ :
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F y
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy) : α)
have simp_rw₂ : Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy)
Tactic: simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
have pos : ∀ (hx : x ∈ F), connectedComponentIn F x ⊆ connectedComponentIn G x
Tactic: by_cases hx : x ∈ F
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
pos : ∀ (hx : x ∈ F), connectedComponentIn F x ⊆ connectedComponentIn G x
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
have neg : ∀ (hx : x ∉ F), connectedComponentIn F x ⊆ connectedComponentIn G x
Tactic: by_cases hx : x ∈ F
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
have pos : Subtype.val (p := fun (x : α) ↦ x ∈ G) ''
    inclusion (s := F) (t := G) h '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) ⊆
  Subtype.val (p := fun (x : α) ↦ x ∈ G) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ G) x sorry)
Tactic: rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
      show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
have neg : ∅ ⊆ connectedComponentIn G x
Tactic: rw [connectedComponentIn_eq_empty hx]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst, inst_2] f
⊢ ConnectedSpace β
have rw : IsConnected (range f)
Tactic: rw [connectedSpace_iff_univ, ← hf.range_eq]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ ConnectedSpace α ↔ ∃ (x : α), connectedComponent x = univ
have mp : ConnectedSpace α → ∃ (x : α), connectedComponent x = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
mp : ConnectedSpace α → ∃ (x : α), connectedComponent x = univ
⊢ ConnectedSpace α ↔ ∃ (x : α), connectedComponent x = univ
have mpr : (∃ (x : α), connectedComponent x = univ) → ConnectedSpace α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected.{u} (α := α) univ
have rw : IsPreconnected (connectedComponent x)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α
have this : PreconnectedSpace α
Tactic: haveI : PreconnectedSpace α :=
      ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = univ
have mp : PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
mp : PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = univ
have mpr : (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α
have mpr : ∀ (hα : IsEmpty α), PreconnectedSpace α
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
mpr : ∀ (hα : IsEmpty α), PreconnectedSpace α
⊢ PreconnectedSpace α
have mpr₁ : ∀ (hα : Nonempty α), PreconnectedSpace α
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected.{u} (α := α) univ
have rw : IsPreconnected.{u} (α := α) ∅
Tactic: rw [univ_eq_empty_iff.mpr hα]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected.{u} (α := α) univ
have rw : IsPreconnected (connectedComponent (Classical.choice hα))
Tactic: rw [← h (Classical.choice hα)]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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 (α := α × β) univ
have rw : IsPreconnected (SProd.sprod (α := Set α) (β := Set β) univ univ)
Tactic: rw [← univ_prod_univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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) univ
have rw : IsPreconnected (α := (i : ι) → X i) (pi (α := X) univ fun (i : ι) ↦ univ)
Tactic: rw [← pi_univ univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected.{u} (α := (↑s : Type u)) univ
have rwa : IsPreconnected.{u} (α := α) (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ)
Tactic: rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
rwa : IsPreconnected.{u} (α := α) (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ)
⊢ IsPreconnected.{u} (α := (↑s : Type u)) univ
have rwa₁ : IsPreconnected.{u} (α := α) (range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
Tactic: rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]
-- 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
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
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have inl : ∀ (hy : Finite.{u_1 + 1} (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
Tactic: obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)
-- 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
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
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have inr : ∀ (hy : Infinite.{u_1 + 1} (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
Tactic: obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)
-- 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
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)
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have inl : ∀ (val : Fintype (ConnectedComponents X)), ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
Tactic: cases nonempty_fintype (ConnectedComponents X)
-- 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
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)
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have inl : (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard
Tactic: simp only [ENat.card_eq_coe_fintype_card]
-- 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
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)
⊢ (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard
have 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)
Tactic: refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [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
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)
⊢ (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard
have 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)
Tactic: refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [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
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)
⊢ (↑(Fintype.card.{u_1} (ConnectedComponents X)) : ℕ∞) ≤ (f ⁻¹' {y}).encard
have 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
Tactic: refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [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
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)
⊢ ENat.card.{u_1} (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
have inr : ∀ (m : ℕ), (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard
Tactic: simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
-- 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
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 : ℕ
⊢ (↑m : ℕ∞) ≤ (f ⁻¹' {y}).encard
have 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
Tactic: obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)