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
refine : IsPreconnected (f ⁻¹' t)
⊢ IsConnected (f ⁻¹' t)

Tactic:
refine ⟨Nonempty.preimage ht'.nonempty hf, ?_⟩
-- 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
⊢ IsClosed[inst] (f ⁻¹' t)

Tactic:
have hT : IsClosed (f ⁻¹' t) :=
    hcl.isClosed_preimage.mpr ht
-- 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)
rw : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
⊢ IsPreconnected (f ⁻¹' t)

Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hT]

Premises used: 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'_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}
t' : β
ht' : t' ∈ t
a : f ⁻¹' {t'} ⊆ u ∪ v
a₁ : f ⁻¹' {t'} ∩ (u ∩ v) = ∅
⊢ f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v

Tactic:
apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv

Premises used: isPreconnected_iff_subset_of_disjoint_closed, And.right, Iff.mp
-- 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}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ u ∪ v

Tactic:
Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Subset.trans, 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'_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}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ u ∪ v

Tactic:
exact Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Subset.trans, 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'_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}
t' : β
ht' : t' ∈ t
a : f ⁻¹' {t'} ∩ ∅ = ∅
a₁ a₂ : Eq.{u + 1} (α := Set α) ∅ ∅
⊢ f ⁻¹' {t'} ∩ (u ∩ v) = ∅

Tactic:
rw [uv_disj.inter_eq, inter_empty]

Premises used: 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}
⊢ ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v

Tactic:
have fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v := by
    intro t' ht'
    apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv
    · exact Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv
    rw [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
a : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u
a₁ : f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
⊢ f ⁻¹' T₁ = f ⁻¹' t ∩ u

Tactic:
apply eq_of_subset_of_subset

Premises used: Set.eq_of_subset_of_subset
-- 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
a : ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u
⊢ f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u

Tactic:
rw [← biUnion_preimage_singleton]

Premises used: Set.biUnion_preimage_singleton
-- 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
⊢ ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u

Tactic:
iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Premises used: Set.iUnion₂_subset, Set.subset_inter, And.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
a : ∀ (t' : β) (ht' : t' ∈ T₁), f ⁻¹' {t'} ⊆ f ⁻¹' t
⊢ ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u

Tactic:
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Premises used: Set.iUnion₂_subset, Set.subset_inter
-- 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' : β
ht' : t' ∈ T₁
a : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t

Tactic:
rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Function.Surjective.preimage_subset_preimage_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'_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' : β
ht' : t' ∈ T₁
⊢ t' ∈ t

Tactic:
ht'.1

Premises used: And.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' : β
ht' : t' ∈ T₁
⊢ t' ∈ t

Tactic:
exact ht'.1

Premises used: And.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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
a₁ : f a ∈ t
a₂ : f ⁻¹' {f a} ⊆ u
⊢ a ∈ f ⁻¹' T₁

Tactic:
constructor
-- 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f a ∈ t

Tactic:
mem_preimage.1 hat

Premises used: 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f a ∈ t

Tactic:
exact mem_preimage.1 hat

Premises used: 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f ⁻¹' {f a} ⊆ u

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

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

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

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

Tactic:
uv_disj.subset_compl_right hau (h rfl)

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

Tactic:
exact uv_disj.subset_compl_right hau (h rfl)

Premises used: Disjoint.subset_compl_right, 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
⊢ f ⁻¹' T₁ = f ⁻¹' t ∩ u

Tactic:
have T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u := 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, hau⟩
    constructor
    · exact mem_preimage.1 hat
    refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_right fun h => ?_
    exact uv_disj.subset_compl_right hau (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
a : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v
a₁ : f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
⊢ f ⁻¹' T₂ = f ⁻¹' t ∩ v

Tactic:
apply eq_of_subset_of_subset

Premises used: Set.eq_of_subset_of_subset
-- 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 : ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v
⊢ f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v

Tactic:
rw [← biUnion_preimage_singleton]

Premises used: Set.biUnion_preimage_singleton
-- 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
⊢ ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v

Tactic:
iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Premises used: Set.iUnion₂_subset, Set.subset_inter, And.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
a : ∀ (t' : β) (ht' : t' ∈ T₂), f ⁻¹' {t'} ⊆ f ⁻¹' t
⊢ ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v

Tactic:
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Premises used: Set.iUnion₂_subset, Set.subset_inter
-- 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' : β
ht' : t' ∈ T₂
a : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t

Tactic:
rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Function.Surjective.preimage_subset_preimage_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'_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' : β
ht' : t' ∈ T₂
⊢ t' ∈ t

Tactic:
ht'.1

Premises used: And.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' : β
ht' : t' ∈ T₂
⊢ t' ∈ t

Tactic:
exact ht'.1

Premises used: And.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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
a₁ : f a ∈ t
a₂ : f ⁻¹' {f a} ⊆ v
⊢ a ∈ f ⁻¹' T₂

Tactic:
constructor
-- 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 a ∈ t

Tactic:
mem_preimage.1 hat

Premises used: 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
⊢ f a ∈ t

Tactic:
exact mem_preimage.1 hat

Premises used: Iff.mp, Set.mem_preimage