awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have h : s ⊆ range inl
Tactic: have h : s ⊆ range Sum.inl :=
        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
-- 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
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1 : IsConnected (inl ⁻¹' s)
Tactic: refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩
-- 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
x : α
hx : inl x ∈ s
h : s ⊆ range inl
refine_1 : IsConnected (inl ⁻¹' s)
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1₁ : s = inl '' inl ⁻¹' s
Tactic: refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have h : s ⊆ range inr
Tactic: have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
-- 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
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1 : IsConnected (inr ⁻¹' s)
Tactic: refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
-- 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
x : β
hx : inr x ∈ s
h : s ⊆ range inr
refine_1 : IsConnected (inr ⁻¹' s)
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
have refine_1₁ : s = inr '' inr ⁻¹' s
Tactic: refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_1 : ∀ (hs : IsPreconnected s),
  (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected 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 : IsPreconnected s),
    (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
⊢ IsPreconnected s ↔ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_2 : ((∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t) → IsPreconnected 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 : IsPreconnected s
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_1 : ∀ (hs : IsPreconnected (α := α ⊕ β) ∅),
  (∃ (t : Set α), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inl '' t)) ∨
    ∃ (t : Set β), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inr '' 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
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
refine_1 :
  ∀ (hs : IsPreconnected (α := α ⊕ β) ∅),
    (∃ (t : Set α), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inl '' t)) ∨
      ∃ (t : Set β), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inr '' t)
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_1₁ : ∀ (h : s.Nonempty), (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_1 : ∀ (t : Set α) (ht : IsConnected t) (hs : IsPreconnected (α := α ⊕ β) (inl '' t))
  (h : Set.Nonempty (α := α ⊕ β) (inl '' t)),
  (∃ (t_1 : Set α), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inl '' t) (inl '' t_1)) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ inl '' t = inr '' t_1
Tactic: obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.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 (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
refine_1 :
  ∀ (t : Set α) (ht : IsConnected t) (hs : IsPreconnected (α := α ⊕ β) (inl '' t))
    (h : Set.Nonempty (α := α ⊕ β) (inl '' t)),
    (∃ (t_1 : Set α), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inl '' t) (inl '' t_1)) ∨
      ∃ (t_1 : Set β), IsPreconnected t_1 ∧ inl '' t = inr '' t_1
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
have refine_1₁ : ∀ (t : Set β) (ht : IsConnected t) (hs : IsPreconnected (α := α ⊕ β) (inr '' t))
  (h : Set.Nonempty (α := α ⊕ β) (inr '' t)),
  (∃ (t_1 : Set α), IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inr '' t) (inr '' t_1)
Tactic: obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
⊢ ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
have rcases : ∀ (i : ι) (s : Set (X i)) (hs : range f = Sigma.mk (β := fun (i : ι) ↦ X i) i '' s),
  ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
Tactic: rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
⊢ ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g
have obtain : ∀ (i : ι) (hi : range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
  ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g
Tactic: obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
    rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
    exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
i : ι
hi : range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g
have rcases : ∀ (g : α → X i) (hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g))
  (hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
  ∃ (i_1 : ι) (g_1 : α → X i_1),
    Continuous[inst, inst_2 i_1] g_1 ∧ Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g = Sigma.mk (β := X) i_1 ∘ g_1
Tactic: rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩
Cleared hypotheses: f, hf, hi
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g)
hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i_1 : ι) (g_1 : α → X i_1),
    Continuous[inst, inst_2 i_1] g_1 ∧ Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g = Sigma.mk (β := X) i_1 ∘ g_1
have refine : Continuous[inst, inst_2 i] g
Tactic: refine ⟨i, g, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g)
hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ Continuous[inst, inst_2 i] g
have rwa : ∀ (hf : Continuous[inst, inst_2 i] g)
  (hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
  Continuous[inst, inst_2 i] g
Tactic: rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf
Cleared hypotheses: hf, hi
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
have refine : IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)
Tactic: refine ⟨?_, isOpen_induced hu (f := Subtype.val)⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)
have refine : Eq (α := Set (↑v : Type u_3)) (v ↓∩ closure[inst] u) (v ↓∩ u)
Tactic: refine isClosed_induced_iff.mpr ⟨closure u, isClosed_closure, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ Eq (α := Set (↑v : Type u_3)) (v ↓∩ closure[inst] u) (v ↓∩ u)
have a : image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ closure[inst] u) =
  image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u)
Tactic: apply image_val_injective
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ closure[inst] u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u)
have a : v ∩ closure[inst] u = v ∩ u
Tactic: simp only [Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ v ∩ closure[inst] u = v ∩ u
have a : v ∩ (u ∪ frontier u) = v ∩ u
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ (u ∪ frontier u) = v ∩ u
⊢ v ∩ closure[inst] u = v ∩ u
have a₁ : v ∩ u ∪ v ∩ frontier u = v ∩ u
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ (u ∪ frontier u) = v ∩ u
a₁ : v ∩ u ∪ v ∩ frontier u = v ∩ u
⊢ v ∩ closure[inst] u = v ∩ u
have a₂ : v ∩ u ∪ frontier u ∩ v = v ∩ u
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ (u ∪ frontier u) = v ∩ u
a₁ : v ∩ u ∪ v ∩ frontier u = v ∩ u
a₂ : v ∩ u ∪ frontier u ∩ v = v ∩ u
⊢ v ∩ closure[inst] u = v ∩ u
have a₃ : v ∩ u ∪ ∅ = v ∩ u
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ (u ∪ frontier u) = v ∩ u
a₁ : v ∩ u ∪ v ∩ frontier u = v ∩ u
a₂ : v ∩ u ∪ frontier u ∩ v = v ∩ u
a₃ : v ∩ u ∪ ∅ = v ∩ u
⊢ v ∩ closure[inst] u = v ∩ u
have a₄ : v ∩ u = v ∩ u
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ Subsingleton ι
have rw : ¬Nontrivial ι
Tactic: rw [← not_nontrivial_iff_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ ¬Nontrivial ι
have by_contra : ∀ (i j : ι) (h_ne : i ≠ j), False
Tactic: by_contra ⟨i, j, h_ne⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : i ≠ j
⊢ False
have h_ne₁ : s i ∩ s j = ∅
Tactic: replace h_ne : s i ∩ s j = ∅ := by
    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne
Cleared hypotheses: h_ne
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
⊢ False
have inl : ∀ (hi : s i = ∅), False
Tactic: rcases isClopen_iff.mp (h_clopen i) with hi | hi
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
inl : ∀ (hi : s i = ∅), False
⊢ False
have inr : ∀ (hi : s i = univ), False
Tactic: rcases isClopen_iff.mp (h_clopen i) with hi | hi
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ False
have h_ne₁ : s j = ∅
Tactic: rw [hi, univ_inter] at h_ne
Cleared hypotheses: h_ne, hi
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ Subsingleton ι
have refine : ∀ (i : ι), IsClosed[inst] (s i)
Tactic: refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨?_, h_open i⟩)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsClosed[inst] (s i)
have rw : IsOpen[inst] (⋃ (i_1 : ι), s i_1 \ s i)
Tactic: rw [← isOpen_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsOpen[inst] (⋃ (i_1 : ι), s i_1 \ s i)
have refine : ∀ (j : ι), IsOpen[inst] (s j \ s i)
Tactic: refine isOpen_iUnion (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
⊢ IsOpen[inst] (s j \ s i)
have inl : IsOpen[inst] (s i \ s i)
Tactic: rcases eq_or_ne i j with rfl | h_ne
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
inl : IsOpen[inst] (s i \ s i)
⊢ IsOpen[inst] (s j \ s i)
have inr : ∀ (h_ne : i ≠ j), IsOpen[inst] (s j \ s i)
Tactic: rcases eq_or_ne i j with rfl | h_ne
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ Subsingleton ι
have refine : ∀ (i : ι), IsOpen[inst] (s i)
Tactic: refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsOpen[inst] (s i)
have rw : IsClosed[inst] (⋃ (i_1 : ι), s i_1 \ s i)
Tactic: rw [← isClosed_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsClosed[inst] (⋃ (i_1 : ι), s i_1 \ s i)
have refine : ∀ (j : ι), IsClosed[inst] (s j \ s i)
Tactic: refine isClosed_iUnion_of_finite (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
⊢ IsClosed[inst] (s j \ s i)
have inl : IsClosed[inst] (s i \ s i)
Tactic: rcases eq_or_ne i j with rfl | h_ne
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
inl : IsClosed[inst] (s i \ s i)
⊢ IsClosed[inst] (s j \ s i)
have inr : ∀ (h_ne : i ≠ j), IsClosed[inst] (s j \ s i)
Tactic: rcases eq_or_ne i j with rfl | h_ne
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
⊢ IsClosed[inst] u
have apply : ∀ (z : α) (hz : ∀ U ∈ 𝓝 z, (U ∩ u).Nonempty), z ∈ u
Tactic: apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
z : α
hz : ∀ U ∈ 𝓝 z, (U ∩ u).Nonempty
⊢ z ∈ u
have rcases : ∀ (t : α) (ht : Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ P z y ∧ P y z) x} t) (h't : t ∈ u), z ∈ u
Tactic: rcases hz _ (h z) with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
⊢ P x y
have A : IsClosed[inst] u
Tactic: have A : IsClosed u := by
    apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
    rcases hz _ (h z) with ⟨t, ht, h't⟩
    exact h'.trans x t z h't ht.2
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
A : IsClosed[inst] u
⊢ IsOpen[inst] u
have apply : ∀ (z : α) (hz : z ∈ u), u ∈ 𝓝 z
Tactic: apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
A : IsClosed[inst] u
z : α
hz : z ∈ u
⊢ u ∈ 𝓝 z
have h₁ : ∀ (t : α) (ht : P z t ∧ P t z), t ∈ u
Tactic: filter_upwards [h z] with t ht
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
A : IsClosed[inst] u
⊢ P x y
have B : IsOpen[inst] u
Tactic: have B : IsOpen u := by
    apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
    filter_upwards [h z] with t ht
    exact h'.trans x z t hz ht.1
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
A : IsClosed[inst] u
B : IsOpen[inst] u
⊢ P x y
have C : u.Nonempty
Tactic: have C : u.Nonempty := ⟨x, (mem_of_mem_nhds (h x)).1⟩