awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
C : u.Nonempty
⊢ P x y
have D : u = univ
Tactic: have D : u = Set.univ := IsClopen.eq_univ ⟨A, B⟩ C
-- 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
B : IsOpen[inst] u
C : u.Nonempty
D : u = univ
⊢ P x y
have change : y ∈ u
Tactic: change y ∈ u
-- 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
h' : IsTrans α P
h'' : Symmetric P
x y : α
⊢ P x y
have refine : ∀ (z : α), ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z
Tactic: refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y
-- 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
h' : IsTrans α P
h'' : Symmetric P
x y z : α
⊢ ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z
have h₁ : ∀ (a : α) (ha : P z a), P z a ∧ P a z
Tactic: filter_upwards [h z] with a ha
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
⊢ P x y
have change : Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
Tactic: change Q ⟨x, hx⟩ ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
have have : ∀ (this : PreconnectedSpace.{u} (↑s : Type u)),
  Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
Tactic: have : PreconnectedSpace s := Subtype.preconnectedSpace hs
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
have h₁ : ∀ (x : { x : α // x ∈ s }), ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x
Tactic: apply PreconnectedSpace.induction₂'
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
h₁ : ∀ (x : { x : α // x ∈ s }), ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
have h'₁ : IsTrans { x : α // x ∈ s } Q
Tactic: apply PreconnectedSpace.induction₂'
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x_1 y : α
hx_1 : x_1 ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
x : α
hx : x ∈ s
⊢ ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
have Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
Tactic: have Z := h x hx
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x_1 y : α
hx_1 : x_1 ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
⊢ ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
have h₁ : ∀
  (Z :
    ∀ᶠ (y : α) in Filter.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)),
      P x y ∧ P y x),
  ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Tactic: rwa [nhdsWithin_eq_map_subtype_coe] at Z
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ P x y
have apply : ∀ (z : α) (hz : z ∈ s), ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z
Tactic: apply hs.induction₂' P (fun z hz ↦ ?_) h' hx hy
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
⊢ ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z
have h₁ : ∀ (a : α) (ha : P z a) (h'a : a ∈ s), P z a ∧ P a z
Tactic: filter_upwards [h z hz, self_mem_nhdsWithin] with a ha h'a
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
have mp : IsPreconnected s → ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
mp : IsPreconnected s → ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
have mpr : (∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) → IsPreconnected s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
have h₁ : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Tactic: specialize h u v hu hv hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
have mp : ∀ (huv : ¬s ⊆ u ∧ ¬s ⊆ v), (s ∩ (u ∩ v)).Nonempty
Tactic: contrapose! huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty
have huv₁ : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
Tactic: simp only [not_subset] at huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty
have mp : ∀ (x : α) (hxs : x ∈ s) (hxu : x ∉ u) (y : α) (hys : y ∈ s) (hyv : y ∉ v), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty
have hxv : x ∈ v
Tactic: have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
have hyu : y ∈ u
Tactic: have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
have mpr : ∀ (H : ¬(s ∩ (u ∩ v)).Nonempty), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False
have h₁ : s ⊆ u ∨ s ⊆ v
Tactic: specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ False
have mpr : (s ∩ (u ∩ v)).Nonempty
Tactic: apply H
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty
have mpr : ∀ (h : s ⊆ u), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
mpr : ∀ (h : s ⊆ u), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
have mpr₁ : ∀ (h : s ⊆ v), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
⊢ (s ∩ (u ∩ v)).Nonempty
have mpr : ∀ (x : α) (hxs : x ∈ s) (hxv : x ∈ v), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases hsv with ⟨x, hxs, hxv⟩
Cleared hypotheses: hsv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty
have mpr : ∀ (x : α) (hxs : x ∈ s) (hxu : x ∈ u), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases hsu with ⟨x, hxs, hxu⟩
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ IsConnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
have rw : (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
Tactic: rw [IsConnected, isPreconnected_iff_subset_of_disjoint]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
have refine_1 : (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
  ∀ (U : Finset (Set α)) (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v)
    (hUo : ∀ u ∈ U, IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))) (hne : s.Nonempty)
    (h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v), ∃ u ∈ U, s ⊆ u
Tactic: refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
refine_1 :
  (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (U : Finset (Set α)) (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v)
      (hUo : ∀ u ∈ U, IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))) (hne : s.Nonempty)
      (h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v),
      ∃ u ∈ U, s ⊆ u
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
have refine_2 : ∀
  (h :
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u),
  s.Nonempty
Tactic: refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
refine_1 :
  (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (U : Finset (Set α)) (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v)
      (hUo : ∀ u ∈ U, IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))) (hne : s.Nonempty)
      (h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v),
      ∃ u ∈ U, s ⊆ u
refine_2 :
  ∀
    (h :
      ∀ (U : Finset (Set α)),
        (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
          (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u),
    s.Nonempty
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
have refine_3 : ∀
  (h :
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u)
  (u v : Set α) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hs : s ⊆ u ∪ v) (hsuv : s ∩ (u ∩ v) = ∅), s ⊆ u ∨ s ⊆ v
Tactic: refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
U : Finset (Set α)
uU : u ∉ U
IH :
  ∀ (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU : ∀ (u_1 v : Set α), u_1 ∈ insert u U → v ∈ insert u U → (s ∩ (u_1 ∩ v)).Nonempty → u_1 = v
hUo : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1
hsU : s ⊆ ⋃₀ (↑(insert u U) : Set (Set α))
⊢ ∃ u_1 ∈ insert u U, s ⊆ u_1
have refine_1 : (s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b) →
  ∀ (h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b)
    (IH :
      ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
        (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u)
    (hU :
      (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
        ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1)
    (hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x) (hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))), s ⊆ u ∨ ∃ x ∈ U, s ⊆ x
Tactic: simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *
Cleared hypotheses: h_1, h, IH, hU, hUo, hsU
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ⊆ u ∨ ∃ x ∈ U, s ⊆ x
have refine_1 : s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅
Tactic: refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
refine_1 : s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅
⊢ s ⊆ u ∨ ∃ x ∈ U, s ⊆ x
have refine_1₁ : s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ x ∈ U, s ⊆ x
Tactic: refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅
have refine_1 : ∀ x ∈ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))),
  ∀ (hxs : x ∈ s) (hxu : x ∈ u) (v : Set α) (hvU : v ∈ (↑U : Set (Set α))) (hxv : x ∈ v),
    Membership.mem (γ := Set α) ∅ x
Tactic: refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
U : Finset (Set α)
hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ U, IsOpen[inst] u
hsU : s ⊆ ⋃₀ (↑U : Set (Set α))
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∃ u ∈ U, s ⊆ u
have refine_1 : ∀
  (hU :
    ∀ (u v : Set α),
      Membership.mem (γ := Finset (Set α)) ∅ u →
        Membership.mem (γ := Finset (Set α)) ∅ v → (s ∩ (u ∩ v)).Nonempty → u = v)
  (hUo : ∀ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u → IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑∅ : Set (Set α))),
  ∃ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u ∧ s ⊆ u
Tactic: induction U using Finset.induction_on with
    | empty => exact absurd (by simpa using hsU) hne.not_subset_empty
    | insert u U uU IH =>
      simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *
      refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
      · refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
        exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm
      · exact IH (fun u hu => (hU.2 u hu).2) hUo.2
Cleared hypotheses: U, hU, hUo, hsU