awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ u ∈ U, s ⊆ u
have refine_1₁ : ∀ (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
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
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
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
have hsuv₁ : ¬(s ∩ (u ∩ v)).Nonempty
Tactic: rw [← not_nonempty_iff_eq_empty] at hsuv
Cleared hypotheses: hsuv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
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 this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
have this₁ : ¬(s ∩ (v ∩ u)).Nonempty
Tactic: rw [inter_comm u] at this
Cleared hypotheses: this
-- 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: classical
  refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
  · 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
  · simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅
  · rw [← not_nonempty_iff_eq_empty] at hsuv
    have := hsuv; rw [inter_comm u] at this
    simpa [*, or_imp, forall_and] using h {u, v}
-- 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: classical
  refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
  · 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
  · simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅
  · rw [← not_nonempty_iff_eq_empty] at hsuv
    have := hsuv; rw [inter_comm u] at this
    simpa [*, or_imp, forall_and] using h {u, v}
-- 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: classical
  refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
  · 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
  · simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅
  · rw [← not_nonempty_iff_eq_empty] at hsuv
    have := hsuv; rw [inter_comm u] at this
    simpa [*, or_imp, forall_and] using h {u, v}
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
have mp : IsPreconnected s → ∀ (u v : Set α), IsClosed[inst] u → IsClosed[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 α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
have mpr : (∀ (u v : Set α), IsClosed[inst] u → IsClosed[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 (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
have mp : ∀
  (h :
    ∀ (t t' : Set α),
      IsClosed[inst] t →
        IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty)
  (u v : Set α) (hu : IsClosed[inst] u) (hv : IsClosed[inst] v) (hs : s ⊆ u ∪ v) (huv : s ∩ (u ∩ v) = ∅), s ⊆ u ∨ s ⊆ v
Tactic: rw [isPreconnected_closed_iff] at h
Cleared hypotheses: h, u, v, hu, hv, hs, huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
have mpr : ∀ (t t' : Set α),
  IsClosed[inst] t → IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
Tactic: rw [isPreconnected_closed_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[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 α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 : IsClosed[inst] u
hv : IsClosed[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 α
hs : IsClosed[inst] s
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
have refine_1 : (∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
  ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic: refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
refine_1 :
  (∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
have refine_2 : (∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
  ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Tactic: refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v
have refine_1 : s ∩ (u ∩ v) = ∅
Tactic: apply H u v hu hv hss
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ∩ (u ∩ v) = ∅
have refine_1 : s ∩ ∅ = ∅
Tactic: rw [huv.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
refine_1 : s ∩ ∅ = ∅
⊢ s ∩ (u ∩ v) = ∅
have refine_1₁ : Eq.{u + 1} (α := Set α) ∅ ∅
Tactic: rw [huv.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
have H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
Tactic: have H1 := H (u ∩ s) (v ∩ s)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v
have H1₁ : IsClosed[inst] (u ∩ s) →
  IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s
Tactic: rw [subset_inter_iff, subset_inter_iff] at H1
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst] (u ∩ s) →
    IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s
⊢ s ⊆ u ∨ s ⊆ v
have H1₁ : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
Tactic: simp only [Subset.refl, and_true] at H1
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v
have refine_2 : s ⊆ u ∩ s ∪ v ∩ s
Tactic: apply H1 (hu.inter hs) (hv.inter hs)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
refine_2 : s ⊆ u ∩ s ∪ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v
have refine_2₁ : Disjoint (u ∩ s) (v ∩ s)
Tactic: apply H1 (hu.inter hs) (hv.inter hs)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∩ s ∪ v ∩ s
have refine_2 : s ⊆ (u ∪ v) ∩ s
Tactic: rw [← union_inter_distrib_right]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)
have refine_2 : u ∩ s ∩ (v ∩ s) = ∅
Tactic: rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
H : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst] (u ∩ s) → IsClosed[inst] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
refine_2 : u ∩ s ∩ (v ∩ s) = ∅
⊢ Disjoint (u ∩ s) (v ∩ s)
have refine_2₁ : u ∩ v ∩ s = ∅
Tactic: rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
have refine_1 : IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
Tactic: refine ⟨?_, fun H a b ha hb hsab hsa hsb ↦ ?_⟩