awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ ∀ (j : ι), j ≠ i → I.piecewise (π := X) f g j ∈ s j

Tactic:
exact fun j _ => this j trivial

Premises used: trivial
-- Module: Mathlib.Topology.Connected.Basic
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

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
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ IsPreconnected S

Tactic:
have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ (S ∩ u).Nonempty

Tactic:
have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ (S ∩ v).Nonempty

Tactic:
have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
-- Module: Mathlib.Topology.Connected.Basic
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

Tactic:
(hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_

Premises used: HasSubset.Subset.trans, Set.Nonempty.mono
-- Module: Mathlib.Topology.Connected.Basic
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
insert : S ∩ (u ∩ v) ⊆ pi (α := X) univ s ∩ (u ∩ v)
⊢ (pi (α := X) univ s ∩ (u ∩ v)).Nonempty

Tactic:
refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_

Premises used: HasSubset.Subset.trans, Set.Nonempty.mono
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ S ∩ (u ∩ v) ⊆ pi (α := X) univ s ∩ (u ∩ v)

Tactic:
inter_subset_inter_left _ hsub

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.Topology.Connected.Basic
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
⊢ S ∩ (u ∩ v) ⊆ pi (α := X) univ s ∩ (u ∩ v)

Tactic:
exact inter_subset_inter_left _ hsub

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.Topology.Connected.Basic
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
insert :
  ∀ (i : ι) (I : Finset ι),
    i ∉ I →
      ∀ (ihI : ∀ (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty)
        (hI : (Insert.insert i I).piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
⊢ (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

Premises used: Finset.piecewise_insert, Insert.insert
-- Module: Mathlib.Topology.Connected.Basic
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
rcases : ∀ (I : Finset ι) (hI : I.piecewise (π := X) f g ∈ u), (pi (α := X) univ s ∩ (u ∩ v)).Nonempty
⊢ (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

Premises used: Finset.piecewise_insert, Insert.insert
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
simp : (pi (α := X) univ s).Nonempty → (IsPreconnected (pi (α := X) univ s) ↔ ∀ (x : ι), IsPreconnected (s x))
⊢ IsConnected (pi (α := X) univ s) ↔ ∀ (i : ι), IsConnected (s i)

Tactic:
simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]

Premises used: IsConnected, Set.univ_pi_nonempty_iff, and_congr_right_iff, forall_and
-- Module: Mathlib.Topology.Connected.Basic
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))

Tactic:
fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩

Premises used: Iff.intro, isPreconnected_univ_pi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
refine :
  ∀ (hne : (pi (α := X) univ s).Nonempty) (hc : IsPreconnected (pi (α := X) univ s)) (i : ι), IsPreconnected (s i)
⊢ (pi (α := X) univ s).Nonempty → (IsPreconnected (pi (α := X) univ s) ↔ ∀ (x : ι), IsPreconnected (s x))

Tactic:
refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩
-- Module: Mathlib.Topology.Connected.Basic
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 : ι
rw : IsPreconnected.{u_2} (α := X i) ((fun (f : (i : ι) → X i) ↦ f i) '' pi (α := X) univ s)
⊢ IsPreconnected (s i)

Tactic:
rw [← eval_image_univ_pi hne]

Premises used: Set.eval_image_univ_pi
-- Module: Mathlib.Topology.Connected.Basic
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.{u_2} (α := X i) ((fun (f : (i : ι) → X i) ↦ f i) '' pi (α := X) univ s)

Tactic:
hc.image _ (continuous_apply _).continuousOn

Premises used: Continuous.continuousOn, IsPreconnected.image, continuous_apply
-- Module: Mathlib.Topology.Connected.Basic
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.{u_2} (α := X i) ((fun (f : (i : ι) → X i) ↦ f i) '' pi (α := X) univ s)

Tactic:
exact hc.image _ (continuous_apply _).continuousOn

Premises used: Continuous.continuousOn, IsPreconnected.image, continuous_apply
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
h : x ∈ F
⊢ connectedComponentIn F x =
    Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)

Tactic:
dif_pos h

Premises used: dif_pos, connectedComponentIn
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
h : x ∉ F
⊢ connectedComponentIn F x = ∅

Tactic:
dif_neg h

Premises used: dif_neg, connectedComponentIn
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Tactic:
mem_sUnion_of_mem (mem_singleton x) ⟨isPreconnected_singleton, mem_singleton x⟩

Premises used: Set.mem_singleton, Set.Mem, connectedComponent, isPreconnected_singleton, Set.mem_sUnion_of_mem, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
⊢ x ∈ connectedComponentIn F x

Tactic:
simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]

Premises used: mem_connectedComponent, connectedComponentIn_eq_image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ (connectedComponent x).Nonempty

Tactic:
⟨x, mem_connectedComponent⟩

Premises used: mem_connectedComponent, Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
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
neg : x ∉ F → (Set.Nonempty.{u} (α := α) ∅ ↔ 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

Tactic:
split_ifs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∈ F
⊢ (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h)).Nonempty ↔
    x ∈ F

Tactic:
simp [connectedComponent_nonempty, *]

Premises used: connectedComponent_nonempty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∉ F
⊢ Set.Nonempty.{u} (α := α) ∅ ↔ x ∈ F

Tactic:
simp [connectedComponent_nonempty, *]

Premises used: connectedComponent_nonempty
-- Module: Mathlib.Topology.Connected.Basic
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
neg : x ∉ F → ∅ ⊆ 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

Tactic:
split_ifs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
h : x ∈ F
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h) ⊆ F

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
F : Set α
x : α
h : x ∉ F
⊢ ∅ ⊆ F

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
isPreconnected_sUnion x _ (fun _ => And.right) fun _ => And.left

Premises used: isPreconnected_sUnion, connectedComponent, And.right, And.left
-- Module: Mathlib.Topology.Connected.Basic
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))
neg : x ∉ F → IsPreconnected.{u} (α := α) ∅
⊢ 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 ∅)

Tactic:
split_ifs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∈ F
⊢ IsPreconnected
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h))

Tactic:
IsInducing.subtypeVal.isPreconnected_image.mpr isPreconnected_connectedComponent

Premises used: Iff.mpr, Topology.IsInducing.isPreconnected_image, isPreconnected_connectedComponent, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∈ F
⊢ IsPreconnected
    (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x h))

Tactic:
exact IsInducing.subtypeVal.isPreconnected_image.mpr isPreconnected_connectedComponent

Premises used: Iff.mpr, Topology.IsInducing.isPreconnected_image, isPreconnected_connectedComponent, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∉ F
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : x ∉ F
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
exact isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsConnected (connectedComponent x)

Tactic:
⟨⟨x, mem_connectedComponent⟩, isPreconnected_connectedComponent⟩

Premises used: IsConnected, mem_connectedComponent, isPreconnected_connectedComponent, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Basic
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
simp_rw₂ : (connectedComponentIn F x).Nonempty ∧ True ↔ (connectedComponentIn F x).Nonempty
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F

Tactic:
simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]

Premises used: and_true, IsConnected, isPreconnected_connectedComponentIn, connectedComponentIn_nonempty_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
s : Set α
H1 : IsPreconnected s
H2 : x ∈ s
⊢ s ⊆ connectedComponent x

Tactic:
fun _z hz => mem_sUnion_of_mem hz ⟨H1, H2⟩

Premises used: Set.Mem, connectedComponent, Set.Subset, Set.mem_sUnion_of_mem, And.intro
-- Module: Mathlib.Topology.Connected.Basic
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)

Tactic:
IsInducing.subtypeVal.isPreconnected_image.mp ?_

Premises used: Topology.IsInducing.isPreconnected_image, Iff.mp, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
refine :
  IsPreconnected
    (image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s))
⊢ IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)

Tactic:
refine IsInducing.subtypeVal.isPreconnected_image.mp ?_

Premises used: Topology.IsInducing.isPreconnected_image, Iff.mp, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
rwa : IsPreconnected (F ∩ s)
rwa₁ rwa₂ rwa₃ rwa₄ : IsPreconnected s
⊢ IsPreconnected
    (image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s))

Tactic:
rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

Premises used: Iff.mpr, Subtype.image_preimage_coe, Set.inter_eq_right
-- Module: Mathlib.Topology.Connected.Basic
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)

Tactic:
have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
-- Module: Mathlib.Topology.Connected.Basic
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)
rw : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯) : α) ∈ s
⊢ Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)

Tactic:
rw [mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Connected.Basic
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)
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯) : α) ∈ s

Tactic:
hxs

Premises used: Set.Mem