awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩

Premises used: Set.Nonempty, And.right, And.left, And.intro, Exists.intro, 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 ⊆ u' ∪ v'
z : α
hz : z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
H : IsConnected s
f : α → β
hf : ContinuousOn f s
⊢ IsConnected (f '' s)

Tactic:
⟨image_nonempty.mpr H.nonempty, H.isPreconnected.image f hf⟩

Premises used: Iff.mpr, Set.image_nonempty, IsConnected, IsPreconnected.image, IsConnected.nonempty, IsConnected.isPreconnected, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
rw : ¬s ⊆ tᶜ ∪ t'ᶜ
⊢ (s ∩ (t ∩ t')).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]

Premises used: Set.subset_compl_iff_disjoint_right, Set.compl_inter, Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
⊢ x ∉ t'

Tactic:
have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
⊢ y ∉ t

Tactic:
have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
⊢ (s ∩ (tᶜ ∩ t'ᶜ)).Nonempty

Tactic:
have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (tᶜ ∩ t'ᶜ)).Nonempty
⊢ (s ∩ (t ∪ t')ᶜ).Nonempty

Tactic:
rw [← compl_union] at this

Premises used: Set.compl_union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (t ∪ t')ᶜ).Nonempty
⊢ False

Tactic:
this.ne_empty htt'.disjoint_compl_right.inter_eq

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.disjoint_compl_right, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst] t
ht' : IsClosed[inst] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (t ∪ t')ᶜ).Nonempty
⊢ False

Tactic:
exact this.ne_empty htt'.disjoint_compl_right.inter_eq

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.disjoint_compl_right, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
rw : ¬s ⊆ uᶜ ∪ vᶜ
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]

Premises used: Set.subset_compl_iff_disjoint_right, Set.compl_inter, Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
⊢ x ∉ v

Tactic:
have xv : x ∉ v := (h' xs).elim (absurd xu) id
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
⊢ y ∉ u

Tactic:
have yu : y ∉ u := (h' ys).elim id (absurd yv)
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
⊢ (s ∩ (uᶜ ∩ vᶜ)).Nonempty

Tactic:
have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
this : (s ∩ (uᶜ ∩ vᶜ)).Nonempty
⊢ (s ∩ (u ∪ v)ᶜ).Nonempty

Tactic:
rw [← compl_union] at this

Premises used: Set.compl_union
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
this : (s ∩ (u ∪ v)ᶜ).Nonempty
⊢ False

Tactic:
this.ne_empty huv.disjoint_compl_right.inter_eq

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.disjoint_compl_right, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.Basic
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 : IsOpen[inst] u
hv : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
this : (s ∩ (u ∪ v)ᶜ).Nonempty
⊢ False

Tactic:
exact this.ne_empty huv.disjoint_compl_right.inter_eq

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.disjoint_compl_right, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
⊢ IsPreconnected (f '' s) ↔ IsPreconnected s

Tactic:
⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩

Premises used: Continuous.continuousOn, IsPreconnected.image, Iff.intro, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
refine : ∀ (h : IsPreconnected (f '' s)), IsPreconnected s
⊢ IsPreconnected (f '' s) ↔ IsPreconnected s

Tactic:
refine ⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
u v : Set α
hu' : IsOpen[inst] u
hv' : IsOpen[inst] v
huv : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∈ u
y : α
hys : y ∈ s
hyv : y ∈ v
rcases :
  ∀ (u : Set β) (hu : IsOpen[inst_1] u) (hu' : IsOpen[inst] (f ⁻¹' u)) (huv : s ⊆ f ⁻¹' u ∪ v) (hxu : x ∈ f ⁻¹' u),
    (s ∩ (f ⁻¹' u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hf.isOpen_iff.1 hu' with ⟨u, hu, rfl⟩

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
v : Set α
hv' : IsOpen[inst] v
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
hyv : y ∈ v
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
huv : s ⊆ f ⁻¹' u ∪ v
hxu : x ∈ f ⁻¹' u
rcases :
  ∀ (v : Set β) (hv : IsOpen[inst_1] v) (hv' : IsOpen[inst] (f ⁻¹' v)) (hyv : y ∈ f ⁻¹' v)
    (huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v), (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
⊢ (s ∩ (f ⁻¹' u ∩ v)).Nonempty

Tactic:
rcases hf.isOpen_iff.1 hv' with ⟨v, hv, rfl⟩

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst_1] v
hv' : IsOpen[inst] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
rwa rwa₁ rwa₂ rwa₃ : s ⊆ f ⁻¹' (u ∪ v)
⊢ f '' s ⊆ u ∪ v

Tactic:
rwa [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst_1] v
hv' : IsOpen[inst] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ f '' s ⊆ u ∪ v

Tactic:
replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst_1] v
hv' : IsOpen[inst] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
rcases : ∀ (z : α) (hzs : z ∈ s) (hzuv : f z ∈ u ∩ v), (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with
    ⟨_, ⟨z, hzs, rfl⟩, hzuv⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst_1] v
hv' : IsOpen[inst] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
z : α
hzs : z ∈ s
hzuv : f z ∈ u ∩ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
⟨z, hzs, hzuv⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst_1] u
hu' : IsOpen[inst] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst_1] v
hv' : IsOpen[inst] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
z : α
hzs : z ∈ s
hzuv : f z ∈ u ∩ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
exact ⟨z, hzs, hzuv⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
hsf : s ⊆ range f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
⊢ f '' f ⁻¹' s = s

Tactic:
replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty

Tactic:
hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_

Premises used: Set.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
refine_1 : s ⊆ f '' u ∪ f '' v
refine_2 : (s ∩ f '' u).Nonempty
refine_3 : (s ∩ f '' v).Nonempty
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty

Tactic:
refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_

Premises used: Set.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

Tactic:
simpa only [hsf, image_union] using image_mono (f := f) hsuv

Premises used: Set.image_mono, Set.image_union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsu.image f

Premises used: Set.image_preimage_inter, Set.Nonempty.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsv.image f

Premises used: Set.image_preimage_inter, Set.Nonempty.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
obtain : ∀ (a : α) (hau : a ∈ u) (has : f a ∈ s) (hav : f a ∈ f '' v), (f ⁻¹' s ∩ (u ∩ v)).Nonempty
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
    refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
    · simpa only [hsf, image_union] using image_mono (f := f) hsuv
    · simpa only [image_preimage_inter] using hsu.image f
    · simpa only [image_preimage_inter] using hsv.image f

Premises used: Inter.inter, Set.Nonempty, Set.image, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
⟨a, has, hau, hinj.mem_set_image.1 hav⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, Iff.mp, Function.Injective.mem_set_image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
hsf : s ⊆ range f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
⊢ f '' f ⁻¹' s = s

Tactic:
replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty

Tactic:
isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_

Premises used: Iff.mp, Set.image, isPreconnected_closed_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
refine_1 : s ⊆ f '' u ∪ f '' v
refine_2 : (s ∩ f '' u).Nonempty
refine_3 : (s ∩ f '' v).Nonempty
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty

Tactic:
refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_

Premises used: Iff.mp, Set.image, isPreconnected_closed_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

Tactic:
simpa only [hsf, image_union] using image_mono (f := f) hsuv

Premises used: Set.image_mono, Set.image_union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsu.image f

Premises used: Set.image_preimage_inter, Set.Nonempty.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
simpa only [image_preimage_inter] using hsv.image f

Premises used: Set.image_preimage_inter, Set.Nonempty.image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
obtain : ∀ (a : α) (hau : a ∈ u) (has : f a ∈ s) (hav : f a ∈ f '' v), (f ⁻¹' s ∩ (u ∩ v)).Nonempty
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
      refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
      · simpa only [hsf, image_union] using image_mono (f := f) hsuv
      · simpa only [image_preimage_inter] using hsu.image f
      · simpa only [image_preimage_inter] using hsv.image f

Premises used: Inter.inter, Set.Nonempty, Set.image, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
⟨a, has, hau, hinj.mem_set_image.1 hav⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, Iff.mp, Function.Injective.mem_set_image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsConnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
hsf : s ⊆ range f
⊢ IsConnected (f ⁻¹' s)

Tactic:
⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isOpenMap hinj hf hsf⟩

Premises used: IsConnected, Set.Nonempty.preimage', IsConnected.nonempty, IsConnected.isPreconnected, And.intro, IsPreconnected.preimage_of_isOpenMap
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set β
hs : IsConnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
hsf : s ⊆ range f
⊢ IsConnected (f ⁻¹' s)

Tactic:
⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isClosedMap hinj hf hsf⟩

Premises used: IsConnected, Set.Nonempty.preimage', IsConnected.nonempty, IsConnected.isPreconnected, And.intro, IsPreconnected.preimage_of_isClosedMap