awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
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
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
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 : (s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
apply H
-- Module: Mathlib.Topology.Connected.Clopen
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
mpr₁ : ∀ (h : s ⊆ v), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases h with h | h
-- Module: Mathlib.Topology.Connected.Clopen
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
mpr : ∀ (x : α) (hxs : x ∈ s) (hxv : x ∈ v), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsv with ⟨x, hxs, hxv⟩
-- Module: Mathlib.Topology.Connected.Clopen
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
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, ⟨h hxs, hxv⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
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
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
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
mpr : ∀ (x : α) (hxs : x ∈ s) (hxu : x ∈ u), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, ⟨hxu, h hxs⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
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

Tactic:
isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩

Premises used: isPreconnected_iff_subset_of_disjoint_closed, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Connected.Clopen
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
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
⊢ IsPreconnected s ↔ ∀ (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 ⟨?_, ?_⟩

Premises used: isPreconnected_iff_subset_of_disjoint_closed, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Connected.Clopen
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 ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H u v hu hv hss
-- Module: Mathlib.Topology.Connected.Clopen
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 ∩ ∅ = ∅
refine_1₁ refine_1₂ : Eq.{u + 1} (α := Set α) ∅ ∅
⊢ s ∩ (u ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

Premises used: Set.inter_empty, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.Clopen
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) = ∅
⊢ 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)
-- Module: Mathlib.Topology.Connected.Clopen
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
⊢ 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

Premises used: Set.subset_inter_iff
-- Module: Mathlib.Topology.Connected.Clopen
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
⊢ 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

Premises used: Set.Subset.refl, and_true
-- Module: Mathlib.Topology.Connected.Clopen
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
refine_2₁ : Disjoint (u ∩ s) (v ∩ s)
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H1 (hu.inter hs) (hv.inter hs)

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Connected.Clopen
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 ∪ v) ∩ s
⊢ s ⊆ u ∩ s ∪ v ∩ s

Tactic:
rw [← union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Topology.Connected.Clopen
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 ∪ v) ∩ s

Tactic:
subset_inter hss Subset.rfl

Premises used: Set.Subset.rfl, Set.subset_inter
-- Module: Mathlib.Topology.Connected.Clopen
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 ∪ v) ∩ s

Tactic:
exact subset_inter hss Subset.rfl

Premises used: Set.Subset.rfl, Set.subset_inter
-- Module: Mathlib.Topology.Connected.Clopen
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) = ∅
refine_2₁ : u ∩ v ∩ s = ∅
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : s ∩ (u ∩ v) = ∅
⊢ Disjoint (u ∩ s) (v ∩ s)

Tactic:
rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

Premises used: Set.inter_inter_distrib_right, Set.disjoint_iff_inter_eq_empty, Set.inter_comm
-- Module: Mathlib.Topology.Connected.Clopen
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

Tactic:
⟨?_, fun H a b ha hb hsab hsa hsb ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
refine_1 :
  IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
refine_2 :
  ∀ (H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b) (a b : Set α)
    (ha : IsOpen[inst] a) (hb : IsOpen[inst] b) (hsab : s ⊆ a ∪ b) (hsa : (s ∩ a).Nonempty) (hsb : (s ∩ b).Nonempty),
    (s ∩ (a ∩ b)).Nonempty
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
refine_1 :
  (∃ (a : Set α) (b : Set α), IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b) →
    ¬IsPreconnected s
⊢ IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b

Tactic:
contrapose!
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
rwa rwa₁ rwa₂ rwa₃ : a.Nonempty
⊢ ((a ∪ b) ∩ a).Nonempty

Tactic:
rwa [union_inter_cancel_left]

Premises used: Set.union_inter_cancel_left
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
rwa rwa₁ rwa₂ rwa₃ : b.Nonempty
⊢ ((a ∪ b) ∩ b).Nonempty

Tactic:
rwa [union_inter_cancel_right]

Premises used: Set.union_inter_cancel_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ (a ∪ b) ∩ (a ∩ b) = ∅

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ False

Tactic:
exact (H a b ha.isOpen hb.isOpen subset_rfl (by rwa [union_inter_cancel_left])
      (by rwa [union_inter_cancel_right])).ne_empty (by grind)

Premises used: Set.Nonempty.ne_empty, IsClopen.isOpen, subset_rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
refine_2 : s ∩ (a ∩ b) ≠ ∅
⊢ (s ∩ (a ∩ b)).Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ a ∩ b = ∅

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ⊆ b ∪ a

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ b ∩ a = ∅

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)

Tactic:
grind [Set.disjoint_iff_inter_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s = s ∩ a ∪ s ∩ b

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ False

Tactic:
exact H (s ∩ a) (s ∩ b)
      (isClopen_inter_of_disjoint_cover_clopen' hs hsab ha hb (by grind))
      (isClopen_inter_of_disjoint_cover_clopen' hs (by grind) hb ha (by grind))
      hsa hsb (by grind [Set.disjoint_iff_inter_eq_empty]) (by grind)

Premises used: Inter.inter, isClopen_inter_of_disjoint_cover_clopen'
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ ¬IsPreconnected s ↔
    ∃ (a : Set α) (b : Set α), IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b

Tactic:
simp [hs.isPreconnected_iff]

Premises used: IsClopen.isPreconnected_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
hs : IsClopen s
hx : x ∈ s
⊢ connectedComponent x ⊆ s

Tactic:
isPreconnected_connectedComponent.subset_isClopen hs ⟨x, mem_connectedComponent, hx⟩

Premises used: mem_connectedComponent, IsPreconnected.subset_isClopen, isPreconnected_connectedComponent, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ connectedComponent x ⊆ ⋂ (Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }), (↑Z : Set α)

Tactic:
subset_iInter fun Z => Z.2.1.connectedComponent_subset Z.2.2

Premises used: Set.subset_iInter, IsClopen.connectedComponent_subset, And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
Z : Set α
h : IsClopen Z
⊢ ⋃ x ∈ Z, connectedComponent x = Z

Tactic:
Subset.antisymm (iUnion₂_subset fun _ => h.connectedComponent_subset) fun _ h =>
    mem_iUnion₂_of_mem h mem_connectedComponent

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, mem_connectedComponent, Set.mem_iUnion₂_of_mem, IsClopen.connectedComponent_subset
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
⊢ image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v))
      (⋃ (x : (↑v : Type u_3)), ⋃ (_ : Membership.mem (γ := Set (↑v : Type u_3)) (v ↓∩ u) x), connectedComponent x)

Tactic:
have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v))
      (⋃ (x : (↑v : Type u_3)), ⋃ (_ : Membership.mem (γ := Set (↑v : Type u_3)) (v ↓∩ u) x), connectedComponent x)
⊢ u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)

Tactic:
simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
    inter_eq_right.mpr huv₁] at this

Premises used: Iff.mpr, Set.image_val_iUnion, Subtype.image_preimage_coe, Set.iUnion_coe_set, Set.inter_eq_right, Set.mem_preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
nth_rw :
  Eq.{u_3 + 1} (α := Set X)
    (⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯))
    (⋃ x ∈ u, connectedComponentIn v x)
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
nth_rw 1 [this]
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
h :
  ∀ (x : X),
    Eq.{u_3 + 1} (α := Set X)
      (⋃ (x_1 : x ∈ v),
        ⋃ (_ : x ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) x ⋯))
      (⋃ (_ : x ∈ u), connectedComponentIn v x)
⊢ Eq.{u_3 + 1} (α := Set X)
    (⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯))
    (⋃ x ∈ u, connectedComponentIn v x)

Tactic:
congr! 2 with x hx
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
x : X
h :
  Eq.{u_3 + 1} (α := Set X) (⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x)
    (⋃ (_ : x ∈ u), connectedComponentIn v x)
⊢ Eq.{u_3 + 1} (α := Set X)
    (⋃ (x_1 : x ∈ v),
      ⋃ (_ : x ∈ u),
        Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) x ⋯))
    (⋃ (_ : x ∈ u), connectedComponentIn v x)

Tactic:
simp only [← connectedComponentIn_eq_image]

Premises used: connectedComponentIn_eq_image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
x : X
⊢ Eq.{u_3 + 1} (α := Set X) (⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x)
    (⋃ (_ : x ∈ u), connectedComponentIn v x)

Tactic:
le_antisymm (iUnion_subset fun _ ↦ le_rfl) <|
    iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl

Premises used: le_rfl, Set.iUnion_subset, Set.subset_iUnion₂_of_subset, le_antisymm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
x : X
⊢ Eq.{u_3 + 1} (α := Set X) (⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x)
    (⋃ (_ : x ∈ u), connectedComponentIn v x)

Tactic:
exact le_antisymm (iUnion_subset fun _ ↦ le_rfl) <|
    iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl

Premises used: le_rfl, Set.iUnion_subset, Set.subset_iUnion₂_of_subset, le_antisymm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
U : Set α
hU : IsClopen U
x : α
hx : x ∈ U
⊢ connectedComponentIn U x = connectedComponent x

Tactic:
subset_antisymm ((isPreconnected_connectedComponentIn).subset_connectedComponent
    (mem_connectedComponentIn hx)) <|
    (isPreconnected_connectedComponent).subset_connectedComponentIn (mem_connectedComponent)
    (hU.connectedComponent_subset hx)

Premises used: mem_connectedComponent, mem_connectedComponentIn, isPreconnected_connectedComponentIn, IsClopen.connectedComponent_subset, subset_antisymm, isPreconnected_connectedComponent, IsPreconnected.subset_connectedComponentIn, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
⊢ Surjective f

Tactic:
have hf : Surjective f := Surjective.of_comp fun t : β => (connected_fibers t).1
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
⊢ IsConnected (f ⁻¹' t)

Tactic:
⟨Nonempty.preimage ht'.nonempty hf, ?_⟩

Premises used: IsConnected, IsConnected.nonempty, And.intro, Set.Nonempty.preimage