awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
specialize hs u v hu hv hsuv
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
inl : ∀ (hsu : s ∩ u = ∅), s ⊆ u ∨ s ⊆ v
inr : ∀ (hsu : (s ∩ u).Nonempty), s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty

Premises used: Inter.inter, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.subset_right_of_subset_union, Or.inr
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Disjoint.subset_right_of_subset_union, Or.inr
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ ∀ (h₂ : ¬(s ∩ (u ∩ v)).Nonempty), ¬(s ∩ v).Nonempty

Tactic:
replace hs := mt (hs hsu)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ∀ (h₂ : ¬(s ∩ (u ∩ v)).Nonempty), ¬(s ∩ v).Nonempty
⊢ ∀ (h₂ : Disjoint s ∅), Disjoint s v

Tactic:
simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
      disjoint_iff_inter_eq_empty.1 huv] at hs

Premises used: Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty, Iff.mp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ∀ (h₂ : Disjoint s ∅), Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

Premises used: Disjoint.subset_left_of_subset_union, Set.disjoint_empty, Or.inl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ∀ (h₂ : Disjoint s ∅), Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

Premises used: Disjoint.subset_left_of_subset_union, Set.disjoint_empty, Or.inl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ Disjoint (Ioi b) (Iio b)

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ f '' s ⊆ Ioi b ∪ Iio b

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ MapsTo f s (Ioi b) ∨ MapsTo f s (Iio b)

Tactic:
simpa [mapsTo_iff_image_subset] using
    (hs.image f hf).subset_or_subset isOpen_Ioi isOpen_Iio (by grind) (by grind)

Premises used: IsPreconnected.subset_or_subset, IsPreconnected.image, Set.mapsTo_iff_image_subset, isOpen_Iio, isOpen_Ioi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, b < f x
x : α
hx : x ∈ s
⊢ ∃ (x : α) (_ : x ∈ s), f x ∉ Iio b

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, f x < b
x : α
hx : x ∈ s
⊢ ∃ (x : α) (_ : x ∈ s), f x ∉ Ioi b

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
by_contra : ∀ (hsv : ¬Disjoint s v), False
⊢ Disjoint s v

Tactic:
by_contra hsv
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ (s ∩ v).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter] at hsv

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
obtain : ∀ x ∈ s, ∀ (hx : x ∈ u ∩ v), False
⊢ False

Tactic:
obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
x : α
left : x ∈ s
hx : x ∈ u ∩ v
⊢ False

Tactic:
Set.disjoint_iff.1 huv hx

Premises used: Set.Mem, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
x : α
left : x ∈ s
hx : x ∈ u ∩ v
⊢ False

Tactic:
exact Set.disjoint_iff.1 huv hx

Premises used: Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
hs : IsPreconnected s
⊢ s ⊆ v

Tactic:
hs.subset_left_of_subset_union hv hu huv.symm (union_comm u v ▸ hsuv) hsv

Premises used: Eq.rec, Set.union_comm, Disjoint.symm, IsPreconnected.subset_left_of_subset_union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
pos : ∀ (xu : x ∈ u), x ∈ u ∪ (closure[inst] u)ᶜ
neg : ∀ (xu : x ∉ u), x ∈ u ∪ (closure[inst] u)ᶜ
⊢ x ∈ u ∪ (closure[inst] u)ᶜ

Tactic:
by_cases xu : x ∈ u
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ (closure[inst] u)ᶜ

Tactic:
Or.inl xu

Premises used: Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ (closure[inst] u)ᶜ

Tactic:
exact Or.inl xu

Premises used: Or.inl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
neg : x ∈ (closure[inst] u)ᶜ
⊢ x ∈ u ∪ (closure[inst] u)ᶜ

Tactic:
right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
h'x : x ∈ closure[inst] u
⊢ False

Tactic:
xu (h (mem_inter h'x hx))

Premises used: Set.mem_inter
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
h'x : x ∈ closure[inst] u
⊢ False

Tactic:
exact xu (h (mem_inter h'x hx))

Premises used: Set.mem_inter
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
⊢ s ⊆ u ∪ (closure[inst] u)ᶜ

Tactic:
have A : s ⊆ u ∪ (closure u)ᶜ := by
    intro x hx
    by_cases xu : x ∈ u
    · exact Or.inl xu
    · right
      intro h'x
      exact xu (h (mem_inter h'x hx))
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst] u)ᶜ
apply : Disjoint u (closure[inst] u)ᶜ
⊢ s ⊆ u

Tactic:
apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u

Premises used: IsClosed.isOpen_compl, IsPreconnected.subset_left_of_subset_union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst] u)ᶜ
⊢ Disjoint u (closure[inst] u)ᶜ

Tactic:
disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)

Premises used: Iff.mpr, subset_closure, Set.compl_subset_compl, disjoint_compl_right, Disjoint.mono_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst] u
h'u : (s ∩ u).Nonempty
h : closure[inst] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst] u)ᶜ
⊢ Disjoint u (closure[inst] u)ᶜ

Tactic:
exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)

Premises used: Iff.mpr, subset_closure, Set.compl_subset_compl, disjoint_compl_right, Disjoint.mono_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
H : ∀ x ∈ s ×ˢ t, ∀ y ∈ s ×ˢ t, ∃ t_1 ⊆ s ×ˢ t, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
⊢ IsPreconnected (s ×ˢ t)

Tactic:
apply isPreconnected_of_forall_pair

Premises used: isPreconnected_of_forall_pair
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ ∃ t_1 ⊆ s ×ˢ t, (a₁, b₁) ∈ t_1 ∧ (a₂, b₂) ∈ t_1 ∧ IsPreconnected t_1

Tactic:
⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩

Premises used: flip, Prod.mk, And.intro, Exists.intro, Set.image, Or.inl, Union.union, Or.inr, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
H : Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t
H₁ : IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)
⊢ ∃ t_1 ⊆ s ×ˢ t, (a₁, b₁) ∈ t_1 ∧ (a₂, b₂) ∈ t_1 ∧ IsPreconnected t_1

Tactic:
refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
y : β
hy : y ∈ t
⊢ (a₁, y) ∈ s ×ˢ t

Tactic:
⟨ha₁, hy⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
x : α
hx : x ∈ s
⊢ flip Prod.mk b₂ x ∈ s ×ˢ t

Tactic:
⟨hx, hb₂⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
y : β
hy : y ∈ t
⊢ (a₁, y) ∈ s ×ˢ t

Tactic:
exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ ContinuousOn (Prod.mk a₁) t

Tactic:
fun_prop
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)

Tactic:
exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
      ⟨a₁, ha₁, rfl⟩ (hs.image _ (Continuous.prodMk_left _).continuousOn)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsConnected s
ht : IsConnected t
⊢ IsConnected (s ×ˢ t)

Tactic:
⟨hs.1.prod ht.1, hs.2.prod ht.2⟩

Premises used: IsConnected, Set.Nonempty.prod, And.right, And.left, And.intro, IsPreconnected.prod
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
rcases : ∀ (I : Finset ι) (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty

Tactic:
rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩

Premises used: IsOpen.mem_nhds, exists_finset_piecewise_mem_of_mem_nhds
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
hI : Finset.piecewise (π := X) ∅ f g ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty

Tactic:
⟨g, hgs, ⟨?_, hgv⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
hI : Finset.piecewise (π := X) ∅ f g ∈ u
empty : g ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty

Tactic:
refine ⟨g, hgs, ⟨?_, hgv⟩⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
hI : Finset.piecewise (π := X) ∅ f g ∈ u
⊢ g ∈ u

Tactic:
simpa using hI
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : (insert i I).piecewise (π := X) f g ∈ u
⊢ update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u

Tactic:
rw [Finset.piecewise_insert] at hI

Premises used: Finset.piecewise_insert
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
⊢ I.piecewise (π := X) f g ∈ pi (α := X) univ s

Tactic:
have := I.piecewise_mem_set_pi hfs hgs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty

Tactic:
(hsuv this).elim ihI fun h => ?_

Premises used: Or.elim
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
⊢ I.piecewise (π := X) f g ∈ v

Tactic:
refine (hsuv this).elim ihI fun h => ?_

Premises used: Or.elim
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
⊢ S ⊆ pi (α := X) univ s

Tactic:
image_subset_iff.2 fun z hz => ?_

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
refine : ∀ (z : X i) (hz : z ∈ s i), z ∈ update (β := X) (I.piecewise (π := X) f g) i ⁻¹' pi (α := X) univ s
⊢ S ⊆ pi (α := X) univ s

Tactic:
refine image_subset_iff.2 fun z hz => ?_

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
z : X i
hz : z ∈ s i
rwa : ∀ (j : ι), j ≠ i → I.piecewise (π := X) f g j ∈ s j
⊢ z ∈ update (β := X) (I.piecewise (π := X) f g) i ⁻¹' pi (α := X) univ s

Tactic:
rwa [update_preimage_univ_pi]

Premises used: Set.update_preimage_univ_pi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
z : X i
hz : z ∈ s i
⊢ ∀ (j : ι), j ≠ i → I.piecewise (π := X) f g j ∈ s j

Tactic:
fun j _ => this j trivial

Premises used: trivial