awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
have refine_1 : x ∈ s ∩ u'
Tactic: refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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'
⊢ (s ∩ (u' ∩ v')).Nonempty
have refine_2 : y ∈ s ∩ v'
Tactic: refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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 ∈ s ∩ u'
have refine_1 : x ∈ u' ∩ s
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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 ∈ s ∩ v'
have refine_2 : y ∈ v' ∩ s
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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'
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have obtain : ∀ (z : α) (hz : z ∈ s ∩ (u' ∩ v')), (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⟩]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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')
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have hz₁ : 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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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'
⊢ (s ∩ (t ∩ t')).Nonempty
have rw : ¬s ⊆ tᶜ ∪ t'ᶜ
Tactic: rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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'ᶜ
⊢ False
have xt' : x ∉ t'
Tactic: have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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'
⊢ False
have yt : y ∉ t
Tactic: have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ False
have this : (s ∩ (tᶜ ∩ t'ᶜ)).Nonempty
Tactic: have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
have this₁ : (s ∩ (t ∪ t')ᶜ).Nonempty
Tactic: rw [← compl_union] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (u ∩ v)).Nonempty
have rw : ¬s ⊆ uᶜ ∪ vᶜ
Tactic: rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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ᶜ
⊢ False
have xv : x ∉ v
Tactic: have xv : x ∉ v := (h' xs).elim (absurd xu) id
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ False
have yu : y ∉ u
Tactic: have yu : y ∉ u := (h' ys).elim id (absurd yv)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ False
have this : (s ∩ (uᶜ ∩ vᶜ)).Nonempty
Tactic: have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
have this₁ : (s ∩ (u ∪ v)ᶜ).Nonempty
Tactic: rw [← compl_union] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
⊢ IsPreconnected (f '' s) ↔ IsPreconnected s
have refine : ∀ (h : IsPreconnected (f '' s)), IsPreconnected s
Tactic: refine ⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (u ∩ v)).Nonempty
have 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
Tactic: rcases hf.isOpen_iff.1 hu' with ⟨u, hu, rfl⟩
Cleared hypotheses: u, hu', huv, hxu
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f ⁻¹' u ∩ v)).Nonempty
have 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
Tactic: rcases hf.isOpen_iff.1 hv' with ⟨v, hv, rfl⟩
Cleared hypotheses: v, hv', hyv, huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
have rwa : s ⊆ f ⁻¹' (u ∪ v)
Tactic: rwa [image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
have huv₁ : f '' s ⊆ u ∪ v
Tactic: replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
have rcases : ∀ (z : α) (hzs : z ∈ s) (hzuv : f z ∈ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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 ⁻¹' s ∩ (u ∩ v)).Nonempty
have hsf₁ : f '' f ⁻¹' s = s
Tactic: replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf
Cleared hypotheses: hsf
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
have refine_1 : s ⊆ f '' u ∪ f '' v
Tactic: refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty
have refine_2 : (s ∩ f '' u).Nonempty
Tactic: refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty
have refine_3 : (s ∩ f '' v).Nonempty
Tactic: refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty
have obtain : ∀ (a : α) (hau : a ∈ u) (has : f a ∈ s) (hav : f a ∈ f '' v), (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
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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 ⁻¹' s ∩ (u ∩ v)).Nonempty
have hsf₁ : f '' f ⁻¹' s = s
Tactic: replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf
Cleared hypotheses: hsf
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
have refine_1 : s ⊆ f '' u ∪ f '' v
Tactic: refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty
have refine_2 : (s ∩ f '' u).Nonempty
Tactic: refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (s ∩ (f '' u ∩ f '' v)).Nonempty
have refine_3 : (s ∩ f '' v).Nonempty
Tactic: refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty
have obtain : ∀ (a : α) (hau : a ∈ u) (has : f a ∈ s) (hav : f a ∈ f '' v), (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
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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 ∨ s ⊆ v
have hs₁ : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Tactic: specialize hs u v hu hv hsuv
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ s ⊆ u ∨ s ⊆ v
have inl : ∀ (hsu : s ∩ u = ∅), s ⊆ u ∨ s ⊆ v
Tactic: obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ s ⊆ u ∨ s ⊆ v
have inr : ∀ (hsu : (s ∩ u).Nonempty), s ⊆ u ∨ s ⊆ v
Tactic: obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ s ⊆ u ∨ s ⊆ v
have hs₁ : ∀ (h₂ : ¬(s ∩ (u ∩ v)).Nonempty), ¬(s ∩ v).Nonempty
Tactic: replace hs := mt (hs hsu)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ s ⊆ u ∨ s ⊆ v
have hs₁ : ∀ (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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ Disjoint s v
have by_contra : ∀ (hsv : ¬Disjoint s v), False
Tactic: by_contra hsv
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ False
have hsv₁ : (s ∩ v).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter] at hsv
Cleared hypotheses: hsv
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ False
have obtain : ∀ x ∈ s, ∀ (hx : x ∈ u ∩ v), False
Tactic: obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ x ∈ u ∪ (closure[inst] u)ᶜ
have pos : ∀ (xu : x ∈ u), x ∈ u ∪ (closure[inst] u)ᶜ
Tactic: by_cases xu : x ∈ u
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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)ᶜ
⊢ x ∈ u ∪ (closure[inst] u)ᶜ
have neg : ∀ (xu : x ∉ u), x ∈ u ∪ (closure[inst] u)ᶜ
Tactic: by_cases xu : x ∈ u
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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)ᶜ
have neg : x ∈ (closure[inst] u)ᶜ
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
have A : 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))
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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)ᶜ
⊢ s ⊆ u
have apply : Disjoint u (closure[inst] u)ᶜ
Tactic: apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ×ˢ t)
have H : ∀ x ∈ s ×ˢ t, ∀ y ∈ s ×ˢ t, ∃ t_1 ⊆ s ×ˢ t, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Tactic: apply isPreconnected_of_forall_pair
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
have H : Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t
Tactic: refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩