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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ f ⁻¹' {f a} ⊆ v

Tactic:
(fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_

Premises used: Or.resolve_left, Iff.mp, Set.mem_preimage
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
a₁ : ∀ (h : f ⁻¹' {f a} ⊆ u), False
⊢ f ⁻¹' {f a} ⊆ v

Tactic:
refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_

Premises used: Or.resolve_left, Iff.mp, Set.mem_preimage
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
h : f ⁻¹' {f a} ⊆ u
⊢ False

Tactic:
uv_disj.subset_compl_left hav (h rfl)

Premises used: Disjoint.subset_compl_left, rfl
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
h : f ⁻¹' {f a} ⊆ u
⊢ False

Tactic:
exact uv_disj.subset_compl_left hav (h rfl)

Premises used: Disjoint.subset_compl_left, rfl
-- 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₂ = f ⁻¹' t ∩ v

Tactic:
have T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v := by
    apply eq_of_subset_of_subset
    · rw [← biUnion_preimage_singleton]
      refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
      rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
      exact ht'.1
    rintro a ⟨hat, hav⟩
    constructor
    · exact mem_preimage.1 hat
    · refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_
      exact uv_disj.subset_compl_left hav (h rfl)
-- 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
⊢ IsClosed[inst_1] T₁

Tactic:
have hT₁ : IsClosed T₁ := hcl.isClosed_preimage.mp (T₁_u.symm ▸ IsClosed.inter hT hu)
-- 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₁
⊢ IsClosed[inst_1] T₂

Tactic:
have hT₂ : IsClosed T₂ := hcl.isClosed_preimage.mp (T₂_v.symm ▸ IsClosed.inter hT hv)
-- 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'_1 : 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' : β
ht' : t' ∈ t
inl : ∀ (htu : f ⁻¹' {t'} ⊆ u), t' ∈ T₁ ∨ t' ∈ T₂
inr : ∀ (htv : f ⁻¹' {t'} ⊆ v), t' ∈ T₁ ∨ t' ∈ T₂
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
rcases fiber_decomp t' ht' with htu | htv
-- 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'_1 : 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' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
inl : t' ∈ T₁
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
left
-- 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'_1 : 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' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁

Tactic:
⟨ht', htu⟩

Premises used: Set.Mem, setOf, And.intro
-- 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'_1 : 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' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁

Tactic:
exact ⟨ht', htu⟩
-- 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'_1 : 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' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
inr : t' ∈ T₂
⊢ t' ∈ T₁ ∨ t' ∈ T₂

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'_1 : 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' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₂

Tactic:
⟨ht', htv⟩

Premises used: Set.Mem, setOf, And.intro
-- 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'_1 : 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' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₂

Tactic:
exact ⟨ht', htv⟩
-- 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 ⊆ T₁ ∪ T₂

Tactic:
have T_decomp : t ⊆ T₁ ∪ T₂ := fun t' ht' => by
    rw [mem_union t' T₁ T₂]
    rcases fiber_decomp t' ht' with htu | htv
    · left; exact ⟨ht', htu⟩
    · right; exact ⟨ht', htv⟩
-- 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₂
⊢ Disjoint T₁ T₂

Tactic:
Disjoint.of_preimage hf ?_

Premises used: Disjoint.of_preimage
-- 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₂
refine : Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
⊢ Disjoint T₁ T₂

Tactic:
refine Disjoint.of_preimage hf ?_

Premises used: Disjoint.of_preimage
-- 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₂
rw : Disjoint (f ⁻¹' t ∩ u) (f ⁻¹' T₂)
rw₁ : Disjoint (f ⁻¹' t ∩ u) (f ⁻¹' t ∩ v)
rw₂ : f ⁻¹' t ∩ u ∩ (f ⁻¹' t ∩ v) = ∅
rw₃ : f ⁻¹' t ∩ (u ∩ v) = ∅
rw₄ : f ⁻¹' t ∩ ∅ = ∅
rw₅ rw₆ : Eq.{u + 1} (α := Set α) ∅ ∅
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)

Tactic:
rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]

Premises used: Set.disjoint_iff_inter_eq_empty, Set.inter_inter_distrib_left, Set.inter_empty, Disjoint.inter_eq
-- 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₂
⊢ Disjoint T₁ T₂

Tactic:
have T_disjoint : Disjoint T₁ T₂ := by
    refine Disjoint.of_preimage hf ?_
    rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- 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₂
inl : ∀ (h : t ⊆ T₁), f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
inr : ∀ (h : t ⊆ T₂), f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
rcases (isPreconnected_iff_subset_of_fully_disjoint_closed ht).1
    ht'.isPreconnected T₁ T₂ hT₁ hT₂ T_decomp T_disjoint with h | h

Premises used: IsConnected.isPreconnected, Iff.mp, isPreconnected_iff_subset_of_fully_disjoint_closed
-- 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₁
inl : f ⁻¹' t ⊆ u
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
left
-- 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 ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' 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
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₁
⊢ f ⁻¹' T₂ = f ⁻¹' t ∩ v

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
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
⊢ IsClosed[inst_1] 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
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₁
⊢ IsClosed[inst_1] 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
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 ⊆ 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
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₂
⊢ Disjoint T₁ T₂

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

Premises used: Set.Subset.antisymm_iff