-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)}
    (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s)

Proof state:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
a✝¹ : ι
s✝ : Finset ι
a✝ : a✝¹ ∉ s✝
ihI : s✝.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : (insert a✝¹ s✝).piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
rename_i i I _

Result:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : (insert i I).piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩

Result:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

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

Result:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
set S := update (I.piecewise f g) i '' s i

Result:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have := I.piecewise_mem_set_pi hfs hgs

Result:
case intro.intro.intro.intro.intro.insert
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
I : Finset ι
hI : I.piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
induction I using Finset.induction_on with
| empty =>
  refine ⟨g, hgs, ⟨?_, hgv⟩⟩
  simpa using hI
| insert _ ihI =>
  rename_i i I _
  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

Result:
no goals