awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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 ⊆ v
have T₂_v : 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)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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 ⊆ u ∨ f ⁻¹' t ⊆ v
have hT₁ : IsClosed[inst_1] T₁
Tactic: have hT₁ : IsClosed T₁ := hcl.isClosed_preimage.mp (T₁_u.symm ▸ IsClosed.inter hT hu)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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₁
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have hT₂ : IsClosed[inst_1] T₂
Tactic: have hT₂ : IsClosed T₂ := hcl.isClosed_preimage.mp (T₂_v.symm ▸ IsClosed.inter hT hv)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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
⊢ t' ∈ T₁ ∨ t' ∈ T₂
have inl : ∀ (htu : f ⁻¹' {t'} ⊆ u), t' ∈ T₁ ∨ t' ∈ T₂
Tactic: rcases fiber_decomp t' ht' with htu | htv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₂
⊢ t' ∈ T₁ ∨ t' ∈ T₂
have inr : ∀ (htv : f ⁻¹' {t'} ⊆ v), t' ∈ T₁ ∨ t' ∈ T₂
Tactic: rcases fiber_decomp t' ht' with htu | htv
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₁ ∨ t' ∈ T₂
have inl : t' ∈ T₁
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₁ ∨ t' ∈ T₂
have inr : t' ∈ T₂
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have T_decomp : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₂
have refine : Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
Tactic: refine Disjoint.of_preimage hf ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw : Disjoint (f ⁻¹' t ∩ u) (f ⁻¹' T₂)
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₂)
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw₁ : Disjoint (f ⁻¹' t ∩ u) (f ⁻¹' t ∩ v)
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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)
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw₂ : f ⁻¹' t ∩ u ∩ (f ⁻¹' t ∩ v) = ∅
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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) = ∅
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw₃ : f ⁻¹' t ∩ (u ∩ v) = ∅
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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) = ∅
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw₄ : f ⁻¹' t ∩ ∅ = ∅
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 ∩ ∅ = ∅
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
have rw₅ : Eq.{u + 1} (α := Set α) ∅ ∅
Tactic: rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq,
      inter_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have T_disjoint : 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]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have inl : ∀ (h : t ⊆ T₁), 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
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have inr : ∀ (h : t ⊆ T₂), 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
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 ⊆ u ∨ f ⁻¹' t ⊆ v
have inl : f ⁻¹' t ⊆ u
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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 ⊆ u
have T₁_u₁ : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u ∧ f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
Tactic: rw [Subset.antisymm_iff] at T₁_u
Cleared hypotheses: T₁_u, T₂_v, hT₁, hT₂, T_decomp, T_disjoint, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 ⊆ u
have inl : f ⁻¹' t ⊆ f ⁻¹' T₁
Tactic: suffices f ⁻¹' t ⊆ f ⁻¹' T₁
      from (this.trans T₁_u.1).trans inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 ⊆ u ∨ f ⁻¹' t ⊆ v
have inr : f ⁻¹' t ⊆ v
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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 ⊆ v
have T₂_v₁ : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v ∧ f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
Tactic: rw [Subset.antisymm_iff] at T₂_v
Cleared hypotheses: T₂_v, hT₁, hT₂, T_decomp, T_disjoint, h
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 ⊆ v
have inr : f ⁻¹' t ⊆ f ⁻¹' T₂
Tactic: suffices f ⁻¹' t ⊆ f ⁻¹' T₂
      from (this.trans T₂_v.1).trans inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsConnected (f ⁻¹' connectedComponent t)
have ht : IsClosed[inst_1] (connectedComponent t)
Tactic: apply hcl.isConnected_preimage_of_isClosed
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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)
⊢ IsConnected (f ⁻¹' connectedComponent t)
have ht' : IsConnected (connectedComponent t)
Tactic: apply hcl.isConnected_preimage_of_isClosed
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f '' connectedComponent a = connectedComponent (f a)
have rw : f '' f ⁻¹' connectedComponent (f a) = connectedComponent (f a)
Tactic: rw [← hf.preimage_connectedComponent h_fibers,
    image_preimage_eq _ fun y ↦ (h_fibers y).nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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)
⊢ f '' connectedComponent a = connectedComponent (f a)
have rw₁ : connectedComponent (f a) = connectedComponent (f a)
Tactic: rw [← hf.preimage_connectedComponent h_fibers,
    image_preimage_eq _ fun y ↦ (h_fibers y).nonempty]