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 α
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
H : Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t
⊢ ∃ t_1 ⊆ s ×ˢ t, (a₁, b₁) ∈ t_1 ∧ (a₂, b₂) ∈ t_1 ∧ IsPreconnected t_1
have H₁ : IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)
Tactic: refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (I : Finset ι) (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
Tactic: rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
hI : Finset.piecewise (π := X) ∅ f g ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have empty : g ∈ u
Tactic: refine ⟨g, hgs, ⟨?_, hgv⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : (insert i I).piecewise (π := X) f g ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have hI₁ : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
Tactic: rw [Finset.piecewise_insert] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
Tactic: have := I.piecewise_mem_set_pi hfs hgs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have h : I.piecewise (π := X) f g ∈ v
Tactic: refine (hsuv this).elim ihI fun h => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
⊢ S ⊆ pi (α := X) univ s
have refine : ∀ (z : X i) (hz : z ∈ s i), z ∈ update (β := X) (I.piecewise (π := X) f g) i ⁻¹' pi (α := X) univ s
Tactic: refine image_subset_iff.2 fun z hz => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
z : X i
hz : z ∈ s i
⊢ z ∈ update (β := X) (I.piecewise (π := X) f g) i ⁻¹' pi (α := X) univ s
have rwa : ∀ (j : ι), j ≠ i → I.piecewise (π := X) f g j ∈ s j
Tactic: rwa [update_preimage_univ_pi]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have hsub : S ⊆ pi (α := X) univ s
Tactic: have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
hsub : S ⊆ pi (α := X) univ s
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have hconn : IsPreconnected S
Tactic: have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
hsub : S ⊆ pi (α := X) univ s
hconn : IsPreconnected S
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have hSu : (S ∩ u).Nonempty
Tactic: have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
hsub : S ⊆ pi (α := X) univ s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have hSv : (S ∩ v).Nonempty
Tactic: have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
i : ι
I : Finset ι
h_1 : i ∉ I
ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
hI : update (β := X) (I.piecewise (π := X) f g) i (f i) ∈ u
this : I.piecewise (π := X) f g ∈ pi (α := X) univ s
h : I.piecewise (π := X) f g ∈ v
S : Set ((a : ι) → X a) := update (β := X) (I.piecewise (π := X) f g) i '' s i
hsub : S ⊆ pi (α := X) univ s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
hSv : (S ∩ v).Nonempty
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have insert : S ∩ (u ∩ v) ⊆ pi (α := X) univ s ∩ (u ∩ v)
Tactic: refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
I : Finset ι
hI : I.piecewise (π := X) f g ∈ u
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have empty : ∀ (hI : Finset.piecewise (π := X) ∅ f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
Tactic: induction I using Finset.induction_on with
  | empty =>
    refine ⟨g, hgs, ⟨?_, hgv⟩⟩
    simpa using hI
  | insert i I _ ihI =>
    rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
I : Finset ι
hI : I.piecewise (π := X) f g ∈ u
empty : ∀ (hI : Finset.piecewise (π := X) ∅ f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have insert : ∀ (i : ι) (I : Finset ι),
  i ∉ I →
    ∀ (ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty)
      (hI : (insert i I).piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
Tactic: induction I using Finset.induction_on with
  | empty =>
    refine ⟨g, hgs, ⟨?_, hgv⟩⟩
    simpa using hI
  | insert i I _ ihI =>
    rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : pi (α := X) univ s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ pi (α := X) univ s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ pi (α := X) univ s
hgv : g ∈ v
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (I : Finset ι) (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
Tactic: classical
  rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩
  induction I using Finset.induction_on with
  | empty =>
    refine ⟨g, hgs, ⟨?_, hgv⟩⟩
    simpa using hI
  | insert i I _ ihI =>
    rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ IsConnected (pi (α := X) univ s) ↔ ∀ (i : ι), IsConnected (s i)
have simp : (pi (α := X) univ s).Nonempty → (IsPreconnected (pi (α := X) univ s) ↔ ∀ (x : ι), IsPreconnected (s x))
Tactic: simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (pi (α := X) univ s).Nonempty → (IsPreconnected (pi (α := X) univ s) ↔ ∀ (x : ι), IsPreconnected (s x))
have refine : ∀ (hne : (pi (α := X) univ s).Nonempty) (hc : IsPreconnected (pi (α := X) univ s)) (i : ι), IsPreconnected (s i)
Tactic: refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hne : (pi (α := X) univ s).Nonempty
hc : IsPreconnected (pi (α := X) univ s)
i : ι
⊢ IsPreconnected (s i)
have rw : IsPreconnected.{u_2} (α := X i) ((fun (f : (i : ι) → X i) ↦ f i) '' pi (α := X) univ s)
Tactic: rw [← eval_image_univ_pi hne]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
⊢ Set.Nonempty.{u} (α := α)
      (if h : x ∈ F then
        Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
      else ∅) ↔
    x ∈ F
have pos : ∀ (h : x ∈ F),
  (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)).Nonempty ↔
    x ∈ F
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
pos :
  ∀ (h : x ∈ F),
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) ''
          connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)).Nonempty ↔
      x ∈ F
⊢ Set.Nonempty.{u} (α := α)
      (if h : x ∈ F then
        Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
      else ∅) ↔
    x ∈ F
have neg : x ∉ F → (Set.Nonempty.{u} (α := α) ∅ ↔ x ∈ F)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then
      Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
    else ∅) ⊆
    F
have pos : ∀ (h : x ∈ F),
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h) ⊆ F
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
pos :
  ∀ (h : x ∈ F),
    Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h) ⊆ F
⊢ (if h : x ∈ F then
      Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
    else ∅) ⊆
    F
have neg : x ∉ F → ∅ ⊆ F
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected.{u} (α := α)
    (if h : x ∈ F then
      Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
    else ∅)
have pos : ∀ (h : x ∈ F),
  IsPreconnected
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
pos :
  ∀ (h : x ∈ F),
    IsPreconnected
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h))
⊢ IsPreconnected.{u} (α := α)
    (if h : x ∈ F then
      Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)
    else ∅)
have neg : x ∉ F → IsPreconnected.{u} (α := α) ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F
have simp_rw : IsConnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
Tactic: simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
simp_rw : IsConnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F
have simp_rw₁ : (connectedComponentIn F x).Nonempty ∧ IsPreconnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
Tactic: simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
simp_rw : IsConnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
simp_rw₁ :
  (connectedComponentIn F x).Nonempty ∧ IsPreconnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F
have simp_rw₂ : (connectedComponentIn F x).Nonempty ∧ True ↔ (connectedComponentIn F x).Nonempty
Tactic: simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
have refine : IsPreconnected
  (image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s))
Tactic: refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected
    (image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s))
have rwa : IsPreconnected (F ∩ s)
Tactic: rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ s ⊆ connectedComponentIn F x
have this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
Tactic: have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
⊢ Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
have rw : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) x sorry) : α) ∈ s
Tactic: rw [mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
⊢ s ⊆ connectedComponentIn F x
have h2xs : Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
  (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x sorry)
Tactic: have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs