awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
s : Set ((i : ι) × X i)
h : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
have inl : Subset (α := Set ((i : ι) × X i)) ∅ univ →
  ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅), Set.Subsingleton (α := (i : ι) × X i) ∅
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
s : Set ((i : ι) × X i)
h : s ⊆ univ
hs : IsPreconnected s
inl :
  Subset (α := Set ((i : ι) × X i)) ∅ univ →
    ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅), Set.Subsingleton (α := (i : ι) × X i) ∅
⊢ s.Subsingleton
have inr : ∀ (h : s.Nonempty), s.Subsingleton
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
s : Set ((i : ι) × X i)
h_1 : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
⊢ s.Subsingleton
have inr : ∀ (a : ι) (t : Set (X a)) (ht : IsConnected t),
  Sigma.mk (β := fun (i : ι) ↦ X i) a '' t ⊆ univ →
    ∀ (hs : IsPreconnected (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t))
      (h : (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty), (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Subsingleton
Tactic: obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
Cleared hypotheses: s, h_1, hs, h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
have mp : TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
mp : TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
have mpr : (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ (connectedComponent x).Subsingleton
have mp : connectedComponent x ⊆ univ
Tactic: apply h.1
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
mp : connectedComponent x ⊆ univ
⊢ (connectedComponent x).Subsingleton
have mp₁ : IsPreconnected (connectedComponent x)
Tactic: apply h.1
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α
have mpr : IsTotallyDisconnected.{u} (α := α) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
have mpr : ∀ (s_sub : Subset.{u} (α := Set α) ∅ univ) (hs : IsPreconnected.{u} (α := α) ∅), Set.Subsingleton.{u} (α := α) ∅
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
Cleared hypotheses: s, s_sub, hs
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
mpr : ∀ (s_sub : Subset.{u} (α := Set α) ∅ univ) (hs : IsPreconnected.{u} (α := α) ∅), Set.Subsingleton.{u} (α := α) ∅
⊢ s.Subsingleton
have mpr₁ : ∀ (x : α) (x_in : x ∈ s), s.Subsingleton
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
have rw : (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}
Tactic: rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}
have refine : ∀ (x : α), (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}
Tactic: refine forall_congr' fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}
have rw : x ∈ connectedComponent x
Tactic: rw [subsingleton_iff_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s
have refine : ∀ (hs : IsTotallyDisconnected s) (u : Set β) (hus : u ⊆ f '' s) (hu : IsPreconnected u), u.Subsingleton
Tactic: refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ f '' (f ⁻¹' u ∩ s) = u
have rwa : u ∩ f '' s = u
Tactic: rwa [image_preimage_inter, inter_eq_left]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u.Subsingleton
have obtain : ∀ (v : Set α) (hvs : v ⊆ s) (hus : f '' v ⊆ f '' s) (hu : IsPreconnected (f '' v)), (f '' v).Subsingleton
Tactic: obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩
Cleared hypotheses: u, hus, hu
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected (f '' v)
⊢ (f '' v).Subsingleton
have hu₁ : IsPreconnected v
Tactic: rw [hf.isInducing.isPreconnected_image] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α
have rw : IsTotallyDisconnected (range f) ↔ IsTotallyDisconnected.{u} (α := α) univ
Tactic: rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
rw : IsTotallyDisconnected (range f) ↔ IsTotallyDisconnected.{u} (α := α) univ
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α
have rw₁ : IsTotallyDisconnected (f '' univ) ↔ IsTotallyDisconnected.{u} (α := α) univ
Tactic: rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
rw : IsTotallyDisconnected (range f) ↔ IsTotallyDisconnected.{u} (α := α) univ
rw₁ : IsTotallyDisconnected (f '' univ) ↔ IsTotallyDisconnected.{u} (α := α) univ
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α
have rw₂ : IsTotallyDisconnected.{u} (α := α) univ ↔ IsTotallyDisconnected.{u} (α := α) univ
Tactic: rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ TotallyDisconnectedSpace.{u} (↑s : Type u) ↔ IsTotallyDisconnected s
have rw : IsTotallyDisconnected.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔
  IsTotallyDisconnected s
Tactic: rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
rw :
  IsTotallyDisconnected.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔
    IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace.{u} (↑s : Type u) ↔ IsTotallyDisconnected s
have rw₁ : IsTotallyDisconnected s ↔ IsTotallyDisconnected s
Tactic: rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y
have by_contra : ∀ (h : ¬x = y), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
⊢ False
have Set : ∀ (u v : Set α) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hxu : x ∈ u) (hyv : y ∈ v) (hs : s ⊆ u ∪ v)
  (huv : Disjoint u v), False
Tactic: obtain
    ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
      huv⟩ :=
    H (hts x_in) (hts y_in) h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False
have refine : t ∩ (u ∩ v) = ∅
Tactic: refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅
have rw : t ∩ ∅ = ∅
Tactic: rw [huv.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
rw : t ∩ ∅ = ∅
⊢ t ∩ (u ∩ v) = ∅
have rw₁ : Eq.{u + 1} (α := Set α) ∅ ∅
Tactic: rw [huv.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ TotallySeparatedSpace α ↔ Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
have simp : (∀ ⦃x y : α⦄,
    x ≠ y → ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
  Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
Tactic: simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄,
      x ≠ y →
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
have refine_1 : ∀ (x y : α),
  x ≠ y →
    (∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) →
      ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (Ux : x ∈ U) (Vy : y ∈ V) (f : univ ⊆ U ∪ V)
        (disj : Disjoint U V), (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
Tactic: refine forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
refine_1 :
  ∀ (x y : α),
    x ≠ y →
      (∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) →
        ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (Ux : x ∈ U) (Vy : y ∈ V) (f : univ ⊆ U ∪ V)
          (disj : Disjoint U V), (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
⊢ (∀ ⦃x y : α⦄,
      x ≠ y →
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
have refine_2 : ∀ (x y : α),
  x ≠ y →
    (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y →
      ∀ (U : Set α) (hU : IsClopen U) (Ux : x ∈ U) (Ucy : y ∈ Uᶜ),
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: refine forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (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 : TotallyDisconnectedSpace β
f : α → β
⊢ TotallyDisconnectedSpace.{u} (ConnectedComponents α)
have rw : ∀ (x : ConnectedComponents α), connectedComponent x = {x}
Tactic: rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (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 : TotallyDisconnectedSpace β
f : α → β
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}
have refine : ∀ (x : α), Eq (α := Set (ConnectedComponents α)) (connectedComponent (mk x)) {mk x}
Tactic: refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (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 : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ Eq (α := Set (ConnectedComponents α)) (connectedComponent (mk x)) {mk x}
have h_fibers : ∀ (y : ConnectedComponents α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {y})
Tactic: rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ←
    connectedComponents_preimage_singleton, image_preimage_eq _ ConnectedComponents.surjective_coe]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (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 : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ ∀ (y : ConnectedComponents α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {y})
have h_fibers : ∀ (y : α), IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {mk y})
Tactic: refine ConnectedComponents.surjective_coe.forall.2 fun y => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (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 : TotallyDisconnectedSpace β
f : α → β
x y : α
⊢ IsConnected (α := α) (preimage (β := ConnectedComponents α) mk {mk y})
have h_fibers : IsConnected (connectedComponent y)
Tactic: rw [connectedComponents_preimage_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing ⋯.connectedComponentsMap
have rw : IsCoinducing (sorry.connectedComponentsMap ∘ ConnectedComponents.mk)
Tactic: rw [← ConnectedComponents.isQuotientMap_coe.isCoinducing.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
⊢ Bijective ⋯.connectedComponentsMap
have refine : ∀ (x y : ConnectedComponents α) (h : sorry.connectedComponentsMap x = sorry.connectedComponentsMap y), x = y
Tactic: refine ⟨fun x y h ↦ ?_, Continuous.connectedComponentsMap_surjective _ fun y ↦ (hf' y).nonempty⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
x y : ConnectedComponents α
h : ⋯.connectedComponentsMap x = ⋯.connectedComponentsMap y
⊢ x = y
have obtain : ∀ (x : α) (h : sorry.connectedComponentsMap (ConnectedComponents.mk x) = sorry.connectedComponentsMap y),
  ConnectedComponents.mk x = y
Tactic: obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
y : ConnectedComponents α
x : α
h : ⋯.connectedComponentsMap (ConnectedComponents.mk x) = ⋯.connectedComponentsMap y
⊢ ConnectedComponents.mk x = y
have obtain : ∀ (y : α)
  (h : sorry.connectedComponentsMap (ConnectedComponents.mk x) = sorry.connectedComponentsMap (ConnectedComponents.mk y)),
  Eq (α := ConnectedComponents α) (ConnectedComponents.mk x) (ConnectedComponents.mk y)
Tactic: obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
this : F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
⊢ f x = f y
have rwa : ∀
  (this :
    (↑(F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx)) : β) = (↑(F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)) : β)),
  f x = f y
Tactic: rwa [← Subtype.coe_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
⊢ f x = f y
have suffices : F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
Tactic: suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : (↑S : Type u) → (↑T : Type u_3) := MapsTo.restrict f S T hTm
⊢ F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
have rw : ∀ (hT : DiscreteTopology.{u_3} (↑T : Type u_3)) {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) {x y : α}
  (hx : x ∈ S) (hy : y ∈ S),
  let F := MapsTo.restrict f S T hTm;
  F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) x hx) = F (Subtype.mk (p := fun (x : α) ↦ x ∈ S) y hy)
Tactic: rw [isDiscrete_iff_discreteTopology] at hT
Cleared hypotheses: hT, f, hc, hTm, x, y, hx, hy, F
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
⊢ ∃ y ∈ T, EqOn f (const α y) S
have inl : ∀ (hS : IsPreconnected.{u} (α := α) ∅) (hc : ContinuousOn f ∅) (hTm : MapsTo f ∅ T), ∃ y ∈ T, EqOn f (const α y) ∅
Tactic: rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
Cleared hypotheses: S, hS, hc, hTm
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst_1 : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
inl : ∀ (hS : IsPreconnected.{u} (α := α) ∅) (hc : ContinuousOn f ∅) (hTm : MapsTo f ∅ T), ∃ y ∈ T, EqOn f (const α y) ∅
⊢ ∃ y ∈ T, EqOn f (const α y) S
have inr : ∀ (x : α) (hx : x ∈ S), ∃ y ∈ T, EqOn f (const α y) S
Tactic: rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)
have cons : IsRetrocompact (t i ⊔ s.sup t)
Tactic: rw [Finset.sup_cons]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)
have empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.sup ∅ t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.sup ∅ t)
⊢ IsRetrocompact (s.sup t)
have cons : ∀ (i : ι) (s : Finset ι) (ih : i ∉ s) (hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.sup t))
  (ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)), IsRetrocompact ((Finset.cons i s ih).sup t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup' hs t)
have rw : IsRetrocompact (s.sup t)
Tactic: rw [Finset.sup'_eq_sup]