awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₁
T₁_u₁ : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
T₂_v₁ : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₃ : IsClosed[inst_1] T₁
hT₄ : IsClosed[inst_1] T₂
T_decomp₁ : t ⊆ T₁ ∪ T₂
T_disjoint₁ : Disjoint T₁ T₂
⊢ t ⊆ T₁

Tactic:
rw [Subset.antisymm_iff] at T₁_u

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₁
inl : f ⁻¹' t ⊆ f ⁻¹' T₁
⊢ f ⁻¹' t ⊆ u

Tactic:
suffices f ⁻¹' t ⊆ f ⁻¹' T₁
      from (this.trans T₁_u.1).trans inter_subset_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₁
⊢ f ⁻¹' t ⊆ f ⁻¹' T₁

Tactic:
preimage_mono h

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₁
⊢ f ⁻¹' t ⊆ f ⁻¹' T₁

Tactic:
exact preimage_mono h

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
inr : f ⁻¹' t ⊆ v
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
⊢ IsClosed[inst_1] T₁

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₃ : IsClosed[inst_1] T₁
⊢ IsClosed[inst_1] T₂

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₃ : IsClosed[inst_1] T₁
hT₄ : IsClosed[inst_1] T₂
⊢ t ⊆ T₁ ∪ T₂

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₃ : IsClosed[inst_1] T₁
hT₄ : IsClosed[inst_1] T₂
T_decomp₁ : t ⊆ T₁ ∪ T₂
⊢ Disjoint T₁ T₂

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₃ : IsClosed[inst_1] T₁
hT₄ : IsClosed[inst_1] T₂
T_decomp₁ : t ⊆ T₁ ∪ T₂
T_disjoint₁ : Disjoint T₁ T₂
⊢ t ⊆ T₂

Tactic:
rw [Subset.antisymm_iff] at T₂_v

Premises used: Set.Subset.antisymm_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
inr : f ⁻¹' t ⊆ f ⁻¹' T₂
⊢ f ⁻¹' t ⊆ v

Tactic:
suffices f ⁻¹' t ⊆ f ⁻¹' T₂
      from (this.trans T₂_v.1).trans inter_subset_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' t ⊆ f ⁻¹' T₂

Tactic:
preimage_mono h

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst_1] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' : β | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
hT₁ : IsClosed[inst_1] T₁
hT₂ : IsClosed[inst_1] T₂
T_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' t ⊆ f ⁻¹' T₂

Tactic:
exact preimage_mono h

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
ht : IsClosed[inst_1] (connectedComponent t)
ht' : IsConnected (connectedComponent t)
connected_fibers₁ : ∀ (t : β), IsConnected (f ⁻¹' {t})
⊢ IsConnected (f ⁻¹' connectedComponent t)

Tactic:
apply hcl.isConnected_preimage_of_isClosed

Premises used: Topology.IsCoinducing.isConnected_preimage_of_isClosed
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsClosed[inst_1] (connectedComponent t)

Tactic:
isClosed_connectedComponent

Premises used: isClosed_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsClosed[inst_1] (connectedComponent t)

Tactic:
exact isClosed_connectedComponent

Premises used: isClosed_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsConnected (connectedComponent t)

Tactic:
isConnected_connectedComponent

Premises used: isConnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsConnected (connectedComponent t)

Tactic:
exact isConnected_connectedComponent

Premises used: isConnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ ∀ (t : β), IsConnected (f ⁻¹' {t})

Tactic:
connected_fibers
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ ∀ (t : β), IsConnected (f ⁻¹' {t})

Tactic:
exact connected_fibers
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f ⁻¹' connectedComponent (f a) = connectedComponent a

Tactic:
((hf.isConnected_preimage_of_isClosed h_fibers isClosed_connectedComponent
    isConnected_connectedComponent).subset_connectedComponent mem_connectedComponent).antisymm
    (hf.continuous.mapsTo_connectedComponent a)

Premises used: Topology.IsCoinducing.isConnected_preimage_of_isClosed, isConnected_connectedComponent, mem_connectedComponent, Continuous.mapsTo_connectedComponent, HasSubset.Subset.antisymm, Topology.IsCoinducing.continuous, isClosed_connectedComponent, IsConnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
rw : f '' f ⁻¹' connectedComponent (f a) = connectedComponent (f a)
rw₁ rw₂ : connectedComponent (f a) = connectedComponent (f a)
⊢ f '' connectedComponent a = connectedComponent (f a)

Tactic:
rw [← hf.preimage_connectedComponent h_fibers,
    image_preimage_eq _ fun y ↦ (h_fibers y).nonempty]

Premises used: Set.image_preimage_eq, Topology.IsCoinducing.preimage_connectedComponent, IsConnected.nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u_3
inst_1 : TopologicalSpace α
x : α
⊢ connectedComponent x = connectedComponent x

Tactic:
trivial
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
⊢ Eq (α := ConnectedComponents α) (mk x) (mk y) ↔ connectedComponent x = connectedComponent y

Tactic:
Quotient.eq''

Premises used: ConnectedComponents.mk, Quotient.eq'', ConnectedComponents
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
⊢ Ne (α := ConnectedComponents α) (mk x) (mk y) ↔ connectedComponent x ≠ connectedComponent y

Tactic:
coe_eq_coe.not

Premises used: Iff.not, ConnectedComponents.coe_eq_coe
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
⊢ Eq (α := ConnectedComponents α) (mk x) (mk y) ↔ x ∈ connectedComponent y

Tactic:
coe_eq_coe.trans connectedComponent_eq_iff_mem

Premises used: connectedComponent_eq_iff_mem, ConnectedComponents.coe_eq_coe, Iff.trans
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Surjective.{u + 1, u + 1} (α := α) (β := ConnectedComponents α) mk

Tactic:
Quot.mk_surjective

Premises used: ConnectedComponents.mk, Quotient, Quot.mk_surjective, ConnectedComponents
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ IsQuotientMap.{u, u} (X := α) (Y := ConnectedComponents α) mk

Tactic:
isQuotientMap_quot_mk

Premises used: ConnectedComponents.mk, Quotient, Quotient.mk', ConnectedComponents, isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Continuous[inst, _] mk

Tactic:
isQuotientMap_coe.continuous

Premises used: Topology.IsQuotientMap.continuous, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Eq.{u + 1} (α := Set (ConnectedComponents α)) (range mk) univ

Tactic:
surjective_coe.range_eq

Premises used: ConnectedComponents.surjective_coe, Function.Surjective.range_eq
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Nonempty.{u + 1} (ConnectedComponents α) ↔ Nonempty α

Tactic:
⟨fun _ ↦ ConnectedComponents.surjective_coe.nonempty, fun h ↦ h.map ConnectedComponents.mk⟩

Premises used: ConnectedComponents.mk, ConnectedComponents.surjective_coe, Iff.intro, Nonempty.map, Function.Surjective.nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 rwa rwa₁ rwa₂ rwa₃ : Nonempty α
⊢ Nonempty.{u + 1} (ConnectedComponents α)

Tactic:
rwa [ConnectedComponents.nonempty_iff_nonempty]

Premises used: ConnectedComponents.nonempty_iff_nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
rw : ¬IsEmpty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
rw₁ : Nonempty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
rw₂ : Nonempty.{u + 1} (ConnectedComponents α) ↔ Nonempty α
rw₃ rw₄ : Nonempty α ↔ Nonempty α
⊢ IsEmpty.{u + 1} (ConnectedComponents α) ↔ IsEmpty α

Tactic:
rw [← not_iff_not, not_isEmpty_iff, not_isEmpty_iff, nonempty_iff_nonempty]

Premises used: not_iff_not, ConnectedComponents.nonempty_iff_nonempty, not_isEmpty_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
⊢ Subsingleton.{u + 1} (ConnectedComponents α)

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
refine : ∀ (x y : ConnectedComponents α), x = y
⊢ Subsingleton.{u + 1} (ConnectedComponents α)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
x y : ConnectedComponents α
obtain : ∀ (x : α), mk x = y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := surjective_coe x

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
y : ConnectedComponents α
x : α
obtain : ∀ (y : α), Eq (α := ConnectedComponents α) (mk x) (mk y)
⊢ mk x = y

Tactic:
obtain ⟨y, rfl⟩ := surjective_coe y

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
x y : α
simp_rw : connectedComponent x = connectedComponent y
⊢ Eq (α := ConnectedComponents α) (mk x) (mk y)

Tactic:
simp_rw [coe_eq_coe, PreconnectedSpace.connectedComponent_eq_univ, ]

Premises used: ConnectedComponents.coe_eq_coe, PreconnectedSpace.connectedComponent_eq_univ
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
rw : connectedComponentIn (U i) x = connectedComponent x
rw₁ rw₂ : connectedComponent x = connectedComponent x
⊢ Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
    connectedComponent x

Tactic:
rw [← connectedComponentIn_eq_image hx, (hclopen i).connectedComponentIn_eq hx]

Premises used: connectedComponentIn_eq_image, IsClopen.connectedComponentIn_eq
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
hconn : ∀ (i : ι), IsPreconnected (U i)
⊢ ∀ {x : α} {i : ι} (hx : x ∈ U i),
    Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
      connectedComponent x

Tactic:
haveI heq {x : α} {i} (hx : x ∈ U i) :
      Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x := by
    rw [← connectedComponentIn_eq_image hx, (hclopen i).connectedComponentIn_eq hx]
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq :
  ∀ {x : α} {i : ι} (hx : x ∈ U i),
    Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
      connectedComponent x
x_1 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i : ι
x_2 : ConnectedComponents (↑(U i) : Type u)
x y : { x : α // x ∈ U i }
hxy : connectedComponent x = connectedComponent y
⊢ Eq (α := ConnectedComponents α) ((mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) x)
    ((mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) y)

Tactic:
simp [← heq x.2, ← heq y.2, hxy]

Premises used: Subtype.property