-- Mathlib/Topology/Connected/Basic.lean
theorem Topology.IsInducing.isPreconnected_image [TopologicalSpace β] {s : Set α} {f : α → β}
    (hf : IsInducing f) : IsPreconnected (f '' s) ↔ IsPreconnected s

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
v : Set α
hv' : IsOpen v
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
hyv : y ∈ v
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
huv : s ⊆ f ⁻¹' u ∪ v
hxu : x ∈ f ⁻¹' u
⊢ (s ∩ (f ⁻¹' u ∩ v)).Nonempty

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
⊢ IsPreconnected s

Tactic:
rintro u v hu' hv' huv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
u v : Set α
hu' : IsOpen u
hv' : IsOpen v
huv : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∈ u
y : α
hys : y ∈ s
hyv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ f '' s ⊆ u ∪ v

Tactic:
rwa [image_subset_iff]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
u v : Set α
hu' : IsOpen u
hv' : IsOpen v
huv : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∈ u
y : α
hys : y ∈ s
hyv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

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

Result:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
v : Set α
hv' : IsOpen v
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
hyv : y ∈ v
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
huv : s ⊆ f ⁻¹' u ∪ v
hxu : x ∈ f ⁻¹' u
⊢ (s ∩ (f ⁻¹' u ∩ v)).Nonempty

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
⊢ IsPreconnected (f '' s) ↔ IsPreconnected s

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

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
⊢ IsPreconnected s

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
⊢ (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⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (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

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen u
hu' : IsOpen (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen v
hv' : IsOpen (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⟩

Result:
no goals