awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
h₁ :
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' connectedComponent y) ''
      (connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯} =
    f ⁻¹' {y}
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' connectedComponent y) ''
      (connectedComponent y).restrictPreimage f ⁻¹'
        {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯}).Finite

Tactic:
convert! h y
-- Module: Mathlib.Topology.Connected.CardComponents
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst_2 : Finite.{u_2 + 1} (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace.{u_2} (↑(connectedComponent y) : Type u_2)
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' connectedComponent y) ''
      (connectedComponent y).restrictPreimage f ⁻¹' {Subtype.mk (p := fun (x : Y) ↦ x ∈ connectedComponent y) y ⋯} =
    f ⁻¹' {y}

Tactic:
aesop (add safe mem_connectedComponent)

Premises used: mem_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsClopen t
hne : (s ∩ t).Nonempty
⊢ s ⊆ t ∪ tᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsConnected s ↔ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
⟨fun hs => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
refine_1 : ∀ (hs : IsConnected s), ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
refine_2 : (∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t) → IsConnected s
⊢ IsConnected s ↔ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
refine_1 :
  ∀ (i : ι) (x : X i) (hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s),
    ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
⊢ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty

Premises used: IsConnected.nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s
⊢ s ⊆ range (mk (β := fun (i : ι) ↦ X i) i)

Tactic:
have : s ⊆ range (Sigma.mk i) :=
      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s
this : s ⊆ range (mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
      (Set.image_preimage_eq_of_subset this).symm⟩

Premises used: Set.preimage, Set.image_preimage_eq_of_subset, And.intro, isOpenMap_sigmaMk, Exists.intro, IsConnected.preimage_of_isOpenMap, Sigma.mk, Eq.symm, sigma_mk_injective
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : mk (β := fun (i : ι) ↦ X i) i x ∈ s
this : s ⊆ range (mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
      (Set.image_preimage_eq_of_subset this).symm⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
t : Set (X i)
ht : IsConnected t
⊢ IsConnected (mk (β := fun (i : ι) ↦ X i) i '' t)

Tactic:
ht.image _ continuous_sigmaMk.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, continuous_sigmaMk
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
t : Set (X i)
ht : IsConnected t
⊢ IsConnected (mk (β := fun (i : ι) ↦ X i) i '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, continuous_sigmaMk
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsPreconnected s ↔ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
⟨fun hs => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
refine_1 :
  ∀ (hs : IsPreconnected s), ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
refine_2 : (∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t) → IsPreconnected s
⊢ IsPreconnected s ↔ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
refine_1 :
  ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅),
    ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ ∅ = mk (β := fun (i : ι) ↦ X i) i '' t
refine_1₁ : ∀ (h : s.Nonempty), ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
hs : IsPreconnected (α := (i : ι) × X i) ∅
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ ∅ = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Premises used: Classical.choice, And.intro, Exists.intro, isPreconnected_empty, EmptyCollection.emptyCollection, Eq.symm, Set.image_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
hs : IsPreconnected (α := (i : ι) × X i) ∅
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ ∅ = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
h : s.Nonempty
refine_1 :
  ∀ (a : ι) (t : Set (X a)) (ht : IsConnected t) (hs : IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t))
    (h : (mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty),
    ∃ (i : ι) (t_1 : Set (X i)),
      IsPreconnected t_1 ∧ mk (β := fun (i : ι) ↦ X i) a '' t = mk (β := fun (i : ι) ↦ X i) i '' t_1
⊢ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk (β := fun (i : ι) ↦ X i) i '' t

Tactic:
obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩

Premises used: And.intro, Iff.mp, Sigma.isConnected_iff, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
a : ι
t : Set (X a)
ht : IsConnected t
hs : IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t)
h : (mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty
⊢ ∃ (i : ι) (t_1 : Set (X i)),
    IsPreconnected t_1 ∧ mk (β := fun (i : ι) ↦ X i) a '' t = mk (β := fun (i : ι) ↦ X i) i '' t_1

Tactic:
⟨a, t, ht.isPreconnected, rfl⟩

Premises used: IsConnected.isPreconnected, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
a : ι
t : Set (X a)
ht : IsConnected t
hs : IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t)
h : (mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty
⊢ ∃ (i : ι) (t_1 : Set (X i)),
    IsPreconnected t_1 ∧ mk (β := fun (i : ι) ↦ X i) a '' t = mk (β := fun (i : ι) ↦ X i) i '' t_1

Tactic:
exact ⟨a, t, ht.isPreconnected, rfl⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
a : ι
t : Set (X a)
ht : IsPreconnected t
⊢ IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t)

Tactic:
ht.image _ continuous_sigmaMk.continuousOn

Premises used: Continuous.continuousOn, continuous_sigmaMk, IsPreconnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst : (i : ι) → TopologicalSpace (X i)
a : ι
t : Set (X a)
ht : IsPreconnected t
⊢ IsPreconnected (mk (β := fun (i : ι) ↦ X i) a '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

Premises used: Continuous.continuousOn, continuous_sigmaMk, IsPreconnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsConnected s ↔ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
⟨fun hs => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
refine_1 :
  ∀ (hs : IsConnected s), (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
refine_2 : ((∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t) → IsConnected s
⊢ IsConnected s ↔ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
refine_1 :
  ∀ (x : α) (hx : inl x ∈ s),
    (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
refine_1₁ :
  ∀ (x : β) (hx : inr x ∈ s),
    (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
obtain ⟨x | x, hx⟩ := hs.nonempty

Premises used: IsConnected.nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ s ⊆ range inl

Tactic:
have h : s ⊆ range Sum.inl :=
        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩

Premises used: Sum.inl, Set.preimage, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
refine_1 : IsConnected (inl ⁻¹' s)
refine_1₁ : s = inl '' inl ⁻¹' s
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)

Tactic:
hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h

Premises used: Sum.inl_injective, isOpenMap_inl, IsConnected.preimage_of_isOpenMap
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)

Tactic:
exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h

Premises used: Sum.inl_injective, isOpenMap_inl, IsConnected.preimage_of_isOpenMap
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s

Tactic:
(image_preimage_eq_of_subset h).symm

Premises used: Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s

Tactic:
exact (image_preimage_eq_of_subset h).symm

Premises used: Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ s ⊆ range inr

Tactic:
have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩

Premises used: Set.preimage, Sum.inr, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
refine_1 : IsConnected (inr ⁻¹' s)
refine_1₁ : s = inr '' inr ⁻¹' s
⊢ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

Tactic:
refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ IsConnected (inr ⁻¹' s)

Tactic:
hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h

Premises used: Sum.inr_injective, IsConnected.preimage_of_isOpenMap, isOpenMap_inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ IsConnected (inr ⁻¹' s)

Tactic:
exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h

Premises used: Sum.inr_injective, IsConnected.preimage_of_isOpenMap, isOpenMap_inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s

Tactic:
(image_preimage_eq_of_subset h).symm

Premises used: Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s

Tactic:
exact (image_preimage_eq_of_subset h).symm

Premises used: Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (α := α ⊕ β) (inl '' t)

Tactic:
ht.image _ continuous_inl.continuousOn

Premises used: Continuous.continuousOn, continuous_inl, IsConnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (α := α ⊕ β) (inl '' t)

Tactic:
exact ht.image _ continuous_inl.continuousOn

Premises used: Continuous.continuousOn, continuous_inl, IsConnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (α := α ⊕ β) (inr '' t)

Tactic:
ht.image _ continuous_inr.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, continuous_inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (α := α ⊕ β) (inr '' t)

Tactic:
exact ht.image _ continuous_inr.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, continuous_inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t

Tactic:
⟨fun hs => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
refine_1 :
  ∀ (hs : IsPreconnected s),
    (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
refine_2 :
  ((∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t) → IsPreconnected s
⊢ IsPreconnected s ↔ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
refine_1 :
  ∀ (hs : IsPreconnected (α := α ⊕ β) ∅),
    (∃ (t : Set α), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inl '' t)) ∨
      ∃ (t : Set β), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inr '' t)
refine_1₁ :
  ∀ (h : s.Nonempty), (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
hs : IsPreconnected (α := α ⊕ β) ∅
⊢ (∃ (t : Set α), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inl '' t)) ∨
    ∃ (t : Set β), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inr '' t)

Tactic:
Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Premises used: And.intro, Exists.intro, isPreconnected_empty, Or.inl, EmptyCollection.emptyCollection, Eq.symm, Set.image_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
hs : IsPreconnected (α := α ⊕ β) ∅
⊢ (∃ (t : Set α), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inl '' t)) ∨
    ∃ (t : Set β), IsPreconnected t ∧ Eq (α := Set (α ⊕ β)) ∅ (inr '' t)

Tactic:
exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
refine_1 :
  ∀ (t : Set α) (ht : IsConnected t) (hs : IsPreconnected (α := α ⊕ β) (inl '' t))
    (h : Set.Nonempty (α := α ⊕ β) (inl '' t)),
    (∃ (t_1 : Set α), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inl '' t) (inl '' t_1)) ∨
      ∃ (t_1 : Set β), IsPreconnected t_1 ∧ inl '' t = inr '' t_1
refine_1₁ :
  ∀ (t : Set β) (ht : IsConnected t) (hs : IsPreconnected (α := α ⊕ β) (inr '' t))
    (h : Set.Nonempty (α := α ⊕ β) (inr '' t)),
    (∃ (t_1 : Set α), IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨
      ∃ (t_1 : Set β), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inr '' t) (inr '' t_1)
⊢ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t

Tactic:
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩

Premises used: And.intro, Iff.mp, Sum.isConnected_iff, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (α := α ⊕ β) (inl '' t)
h : Set.Nonempty (α := α ⊕ β) (inl '' t)
⊢ (∃ (t_1 : Set α), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inl '' t) (inl '' t_1)) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ inl '' t = inr '' t_1

Tactic:
Or.inl ⟨t, ht.isPreconnected, rfl⟩

Premises used: IsConnected.isPreconnected, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (α := α ⊕ β) (inl '' t)
h : Set.Nonempty (α := α ⊕ β) (inl '' t)
⊢ (∃ (t_1 : Set α), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inl '' t) (inl '' t_1)) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ inl '' t = inr '' t_1

Tactic:
exact Or.inl ⟨t, ht.isPreconnected, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (α := α ⊕ β) (inr '' t)
h : Set.Nonempty (α := α ⊕ β) (inr '' t)
⊢ (∃ (t_1 : Set α), IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inr '' t) (inr '' t_1)

Tactic:
Or.inr ⟨t, ht.isPreconnected, rfl⟩

Premises used: IsConnected.isPreconnected, And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (α := α ⊕ β) (inr '' t)
h : Set.Nonempty (α := α ⊕ β) (inr '' t)
⊢ (∃ (t_1 : Set α), IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨
    ∃ (t_1 : Set β), IsPreconnected t_1 ∧ Eq (α := Set (α ⊕ β)) (inr '' t) (inr '' t_1)

Tactic:
exact Or.inr ⟨t, ht.isPreconnected, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (α := α ⊕ β) (inl '' t)

Tactic:
ht.image _ continuous_inl.continuousOn

Premises used: Continuous.continuousOn, continuous_inl, IsPreconnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (α := α ⊕ β) (inl '' t)

Tactic:
exact ht.image _ continuous_inl.continuousOn

Premises used: Continuous.continuousOn, continuous_inl, IsPreconnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (α := α ⊕ β) (inr '' t)

Tactic:
ht.image _ continuous_inr.continuousOn

Premises used: Continuous.continuousOn, continuous_inr, IsPreconnected.image