awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
x : α
hx : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x
y : α
hy : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
    mem_biUnion hjp hyj, hp⟩

Premises used: Set.mem_biUnion, And.intro, Exists.intro, Set.biUnion_subset_biUnion_left, Set.iUnion
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
x : α
hx : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x
y : α
hy : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
    mem_biUnion hjp hyj, hp⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
ht : t.Nonempty
H : ∀ i ∈ t, IsConnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsConnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
⟨nonempty_biUnion.2 <| ⟨ht.some, ht.some_mem, (H _ ht.some_mem).nonempty⟩,
    IsPreconnected.biUnion_of_reflTransGen (fun i hi => (H i hi).isPreconnected) K⟩

Premises used: Iff.mpr, IsConnected, Set.nonempty_biUnion, Set.Nonempty.some_mem, IsPreconnected.biUnion_of_reflTransGen, IsConnected.nonempty, IsConnected.isPreconnected, And.intro, Exists.intro, Set.Nonempty.some
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty) i j
rw : IsPreconnected.{u} (α := α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), s x)
⊢ IsPreconnected.{u} (α := α) (⋃ (n : ι), s n)

Tactic:
rw [← biUnion_univ]

Premises used: Set.biUnion_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty) i j
i : ι
h : Membership.mem (γ := Set ι) univ i
j : ι
h_1 : Membership.mem (γ := Set ι) univ j
⊢ ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ Membership.mem (γ := Set ι) univ i) i j

Tactic:
simpa [mem_univ] using K i j

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected.{u} (α := α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), s x)

Tactic:
exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
    simpa [mem_univ] using K i j

Premises used: IsPreconnected.biUnion_of_reflTransGen
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
inst_1 : Nonempty ι
s : ι → Set α
H : ∀ (i : ι), IsConnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty) i j
⊢ IsConnected.{u} (α := α) (⋃ (n : ι), s n)

Tactic:
⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩,
    IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩

Premises used: Iff.mpr, Set.nonempty_iUnion, IsConnected, Nonempty.elim, IsPreconnected.iUnion_of_reflTransGen, IsConnected.nonempty, IsConnected.isPreconnected, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x x_1 : β
⊢ ∀ i ∈ Ico x_1 x, (s (succ i) ∩ s i).Nonempty

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
inst_4 : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x x_1 : β
⊢ ∀ i ∈ Ico x_1 x, (s (succ i) ∩ s i).Nonempty

Tactic:
grind
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
⊢ ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t

Tactic:
have h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t := fun hi hj hk =>
    ht.out hi hj (Ico_subset_Icc_self hk)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
⊢ ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t

Tactic:
have h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t := fun hi hj hk =>
    ht.out hi hj ⟨hk.1.trans <| le_succ _, succ_le_of_lt hk.2⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
⊢ ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty

Tactic:
have h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty :=
    fun hi hj hk => K _ (h1 hi hj hk) (h2 hi hj hk)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_

Premises used: IsPreconnected.biUnion_of_reflTransGen
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
refine : ∀ (i : β) (hi : i ∈ t) (j : β) (hj : j ∈ t), ReflTransGen (fun (i j : β) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_

Premises used: IsPreconnected.biUnion_of_reflTransGen
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
rw : (s k ∩ s (succ k)).Nonempty
⊢ (s (succ k) ∩ s k).Nonempty

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty

Tactic:
h3 hj hi hk
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty

Tactic:
exact h3 hj hi hk
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
⊢ ReflTransGen (fun (i j : β) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j

Tactic:
exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
      ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩

Premises used: reflTransGen_of_succ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
inst_2 : SuccOrder β
inst_3 : IsSuccArchimedean β
s : β → Set α
t : Set β
hnt : t.Nonempty
ht : t.OrdConnected
H : ∀ n ∈ t, IsConnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
⊢ IsConnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
⟨nonempty_biUnion.2 <| ⟨hnt.some, hnt.some_mem, (H _ hnt.some_mem).nonempty⟩,
    IsPreconnected.biUnion_of_chain ht (fun i hi => (H i hi).isPreconnected) K⟩

Premises used: Iff.mpr, IsPreconnected.biUnion_of_chain, IsConnected, Set.nonempty_biUnion, Set.Nonempty.some_mem, IsConnected.nonempty, IsConnected.isPreconnected, And.intro, Exists.intro, Set.Nonempty.some
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : IsPreconnected s
Kst : s ⊆ t
Ktcs : t ⊆ closure[inst] s
⊢ IsPreconnected t

Tactic:
fun u v hu hv htuv ⟨_y, hyt, hyu⟩ ⟨_z, hzt, hzv⟩ =>
  let ⟨p, hpu, hps⟩ := mem_closure_iff.1 (Ktcs hyt) u hu hyu
  let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (Ktcs hzt) v hv hzv
  let ⟨r, hrs, hruv⟩ := H u v hu hv (Subset.trans Kst htuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩
  ⟨r, Kst hrs, hruv⟩

Premises used: mem_closure_iff, Set.Subset.trans, _private.0.IsPreconnected.subset_closure.match_2, Inter.inter, Set.Nonempty, And.intro, _private.0.IsPreconnected.subset_closure.match_1, Exists.intro, Iff.mp, IsPreconnected, _private.0.IsPreconnected.subset_closure.match_3
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : IsConnected s
Kst : s ⊆ t
Ktcs : t ⊆ closure[inst] s
⊢ IsConnected t

Tactic:
⟨Nonempty.mono Kst H.left, IsPreconnected.subset_closure H.right Kst Ktcs⟩

Premises used: IsConnected, Set.Nonempty.mono, And.right, And.left, And.intro, IsPreconnected.subset_closure
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsPreconnected s
⊢ IsPreconnected (closure[inst] s)

Tactic:
IsPreconnected.subset_closure H subset_closure Subset.rfl

Premises used: subset_closure, Set.Subset.rfl, IsPreconnected.subset_closure
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsConnected s
⊢ IsConnected (closure[inst] s)

Tactic:
IsConnected.subset_closure H subset_closure <| Subset.rfl

Premises used: subset_closure, IsConnected.subset_closure, Set.Subset.rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
rcases : ∀ (u' : Set α) (hu' : IsOpen[inst] u') (u'_eq : f ⁻¹' u ∩ s = u' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
rcases : ∀ (v' : Set α) (hv' : IsOpen[inst] v') (v'_eq : f ⁻¹' v ∩ s = v' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
rw :
  ∀ (huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v) (x : α) (xs : x ∈ s) (xu : f x ∈ u) (y : α) (ys : y ∈ s) (yv : f y ∈ v) (u' : Set α)
    (hu' : IsOpen[inst] u') (u'_eq : f ⁻¹' u ∩ s = u' ∩ s) (v' : Set α) (hv' : IsOpen[inst] v')
    (v'_eq : f ⁻¹' v ∩ s = v' ∩ s), s ⊆ u' ∪ v'
⊢ s ⊆ u' ∪ v'

Tactic:
rw [image_subset_iff, preimage_union] at huv

Premises used: Set.preimage_union, Set.image_subset_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s

Tactic:
replace huv := subset_inter huv Subset.rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s
⊢ s ⊆ (u' ∪ v') ∩ s

Tactic:
rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
(subset_inter_iff.1 huv).1

Premises used: Set.subset_inter_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
exact (subset_inter_iff.1 huv).1

Premises used: Set.subset_inter_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
replace huv : s ⊆ u' ∪ v' := by
    rw [image_subset_iff, preimage_union] at huv
    replace huv := subset_inter huv Subset.rfl
    rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv
    exact (subset_inter_iff.1 huv).1
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ (s ∩ (u' ∩ v')).Nonempty

Tactic:
H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
refine_1 : x ∈ s ∩ u'
refine_2 : y ∈ s ∩ v'
⊢ (s ∩ (u' ∩ v')).Nonempty

Tactic:
refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
refine_1 : x ∈ u' ∩ s
⊢ x ∈ s ∩ u'

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
refine_2 : y ∈ v' ∩ s
⊢ y ∈ s ∩ v'

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s

Tactic:
u'_eq ▸ ⟨xu, xs⟩

Premises used: Eq.rec, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ y ∈ v' ∩ s

Tactic:
v'_eq ▸ ⟨yv, ys⟩

Premises used: Eq.rec, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s

Tactic:
exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩]
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
obtain : ∀ (z : α) (hz : z ∈ s ∩ (u' ∩ v')), (f '' s ∩ (u ∩ v)).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).Nonempty := by
    refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩ <;> rw [inter_comm]
    exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩]

Premises used: Inter.inter, Set.Nonempty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ s ∩ (u' ∩ v')
⊢ z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)

Tactic:
rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc, inter_comm s, inter_comm s,
    ← u'_eq, ← v'_eq] at hz

Premises used: Set.inter_self, Set.inter_left_comm, Set.inter_comm, Set.inter_assoc