awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s
have inl : ∀
  (H :
    ∀ (x : α),
      Membership.mem (γ := Set α) ∅ x →
        ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t),
  IsPreconnected.{u} (α := α) ∅
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
inl :
  ∀
    (H :
      ∀ (x : α),
        Membership.mem (γ := Set α) ∅ x →
          ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t),
    IsPreconnected.{u} (α := α) ∅
⊢ IsPreconnected s
have inr : ∀ (x : α) (hx : x ∈ s), IsPreconnected s
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ IsPreconnected (⋃₀ c)
have apply : ∀ y ∈ ⋃₀ c, ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic: apply isPreconnected_of_forall x
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)
have rcases : ∀ (x : α) (hxs : x ∈ s) (hxt : x ∈ t), IsPreconnected (s ∪ t)
Tactic: rcases H with ⟨x, hxs, hxt⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)
have rcases : ∀ (x : α) (hx : x ∈ s ∩ t), IsConnected (s ∪ t)
Tactic: rcases H with ⟨x, hx⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)
have refine : IsPreconnected (s ∪ t)
Tactic: refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty
have obtain : ∀ (r : Set α) (hrS : r ∈ S) (hsr : s ⊆ r) (htr : t ⊆ r), (⋃₀ S ∩ (u ∩ v)).Nonempty
Tactic: obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty
have Hnuv : (r ∩ (u ∩ v)).Nonempty
Tactic: have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
    H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : (r ∩ (u ∩ v)).Nonempty
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty
have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)
Tactic: have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
have refl : IsPreconnected.{u} (α := α) (⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} j), s j)
Tactic: refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected.{u} (α := α) (⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} j), s j)
have refl : IsPreconnected (s i)
Tactic: rw [biUnion_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
have tail : ∀ (p : Set ι) (hpt : p ⊆ t) (hip : i ∈ p) (hjp : j ∈ p) (hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)),
  ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
Tactic: obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
have tail : IsPreconnected.{u} (α := α) (⋃ j ∈ insert k p, s j)
Tactic: refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ IsPreconnected.{u} (α := α) (⋃ j ∈ insert k p, s j)
have tail : IsPreconnected (s k ∪ ⋃ x ∈ p, s x)
Tactic: rw [biUnion_insert]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ IsPreconnected (s k ∪ ⋃ x ∈ p, s x)
have tail : s j ∩ s k ⊆ s k ∩ ⋃ x ∈ p, s x
Tactic: refine (H k hj).union' (hjk.1.mono ?_) hp
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ s j ∩ s k ⊆ s k ∩ ⋃ x ∈ p, s x
have tail : s k ∩ s j ⊆ s k ∩ ⋃ x ∈ p, s x
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
⊢ ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
have refl : ∀ (hj : i ∈ t), ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
Tactic: induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
Cleared hypotheses: hj, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
refl : ∀ (hj : i ∈ t), ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
have tail : ∀ {j k : ι},
  ReflTransGen R i j →
    ∀ (hjk : R j k) (ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j))
      (hj : k ∈ t), ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
Tactic: induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
Cleared hypotheses: hj, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)
have P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
Tactic: have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
      ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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)
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x →
    ∀ (y : α),
      Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y → ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Tactic: refine isPreconnected_of_forall_pair ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
have obtain : ∀ (i : ι) (hi : i ∈ t) (hxi : x ∈ s i), ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Tactic: obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
have obtain : ∀ (j : ι) (hj : j ∈ t) (hyj : y ∈ s j), ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Tactic: obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
have obtain : ∀ (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: obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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} (α := α) (⋃ (n : ι), s n)
have rw : IsPreconnected.{u} (α := α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), s x)
Tactic: rw [← biUnion_univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)
have h1 : ∀ {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)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)
have h2 : ∀ {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⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
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
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)
have h3 : ∀ {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)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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)
have refine : ∀ (i : β) (hi : i ∈ t) (j : β) (hj : j ∈ t), ReflTransGen (fun (i j : β) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
Tactic: refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
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 (succ k) ∩ s k).Nonempty
have rw : (s k ∩ s (succ k)).Nonempty
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
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (u' : Set α) (hu' : IsOpen[inst] u') (u'_eq : f ⁻¹' u ∩ s = u' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
-- 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
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
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (v' : Set α) (hv' : IsOpen[inst] v') (v'_eq : f ⁻¹' v ∩ s = v' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
-- 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
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'
have 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'
Tactic: rw [image_subset_iff, preimage_union] at huv
Cleared hypotheses: huv, x, xs, xu, y, ys, yv, u', hu', u'_eq, v', hv', v'_eq
-- 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
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'
have huv₁ : s ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s
Tactic: replace huv := subset_inter huv Subset.rfl
Cleared hypotheses: huv
-- 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 ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s
⊢ s ⊆ u' ∪ v'
have huv₁ : s ⊆ (u' ∪ v') ∩ s
Tactic: rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv
Cleared hypotheses: huv
-- 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
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
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have huv₁ : 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
Cleared hypotheses: huv