awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
refine_1 :
  IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
⊢ IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
have refine_2 : ∀ (H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b) (a b : Set α)
  (ha : IsOpen[inst] a) (hb : IsOpen[inst] b) (hsab : s ⊆ a ∪ b) (hsa : (s ∩ a).Nonempty) (hsb : (s ∩ b).Nonempty),
  (s ∩ (a ∩ b)).Nonempty
Tactic: refine ⟨?_, fun H a b ha hb hsab hsa hsb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
have refine_1 : (∃ (a : Set α) (b : Set α), IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b) →
  ¬IsPreconnected s
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ (s ∩ (a ∩ b)).Nonempty
have refine_2 : s ∩ (a ∩ b) ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
⊢ u = ⋃ x ∈ u, connectedComponentIn v x
have this : image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u) =
  image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v))
    (⋃ (x : (↑v : Type u_3)), ⋃ (_ : Membership.mem (γ := Set (↑v : Type u_3)) (v ↓∩ u) x), connectedComponent x)
Tactic: have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v))
      (⋃ (x : (↑v : Type u_3)), ⋃ (_ : Membership.mem (γ := Set (↑v : Type u_3)) (v ↓∩ u) x), connectedComponent x)
⊢ u = ⋃ x ∈ u, connectedComponentIn v x
have this₁ : u =
  ⋃ (i : X),
    ⋃ (x : i ∈ v),
      ⋃ (_ : i ∈ u),
        Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i sorry)
Tactic: simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
    inter_eq_right.mpr huv₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
⊢ u = ⋃ x ∈ u, connectedComponentIn v x
have nth_rw : Eq.{u_3 + 1} (α := Set X)
  (⋃ (i : X),
    ⋃ (x : i ∈ v),
      ⋃ (_ : i ∈ u),
        Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i sorry))
  (⋃ x ∈ u, connectedComponentIn v x)
Tactic: nth_rw 1 [this]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
⊢ Eq.{u_3 + 1} (α := Set X)
    (⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯))
    (⋃ x ∈ u, connectedComponentIn v x)
have h : ∀ (x : X),
  Eq.{u_3 + 1} (α := Set X)
    (⋃ (x_1 : x ∈ v),
      ⋃ (_ : x ∈ u),
        Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) x sorry))
    (⋃ (_ : x ∈ u), connectedComponentIn v x)
Tactic: congr! 2 with x hx
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)
huv₁ : u ⊆ v
this :
  u =
    ⋃ (i : X),
      ⋃ (x : i ∈ v),
        ⋃ (_ : i ∈ u),
          Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) i ⋯)
x : X
⊢ Eq.{u_3 + 1} (α := Set X)
    (⋃ (x_1 : x ∈ v),
      ⋃ (_ : x ∈ u),
        Subtype.val (p := fun (x : X) ↦ x ∈ v) '' connectedComponent (Subtype.mk (p := fun (x : X) ↦ x ∈ v) x ⋯))
    (⋃ (_ : x ∈ u), connectedComponentIn v x)
have h : Eq.{u_3 + 1} (α := Set X) (⋃ (_ : x ∈ v), ⋃ (_ : x ∈ u), connectedComponentIn v x)
  (⋃ (_ : x ∈ u), connectedComponentIn v x)
Tactic: simp only [← connectedComponentIn_eq_image]
-- 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
⊢ IsConnected (f ⁻¹' t)
have hf : Surjective f
Tactic: have hf : Surjective f := Surjective.of_comp fun t : β => (connected_fibers t).1
-- 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
⊢ IsConnected (f ⁻¹' t)
have refine : IsPreconnected (f ⁻¹' t)
Tactic: refine ⟨Nonempty.preimage ht'.nonempty hf, ?_⟩
-- 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
⊢ IsPreconnected (f ⁻¹' t)
have hT : IsClosed[inst] (f ⁻¹' t)
Tactic: have hT : IsClosed (f ⁻¹' t) :=
    hcl.isClosed_preimage.mpr ht
-- 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)
⊢ IsPreconnected (f ⁻¹' t)
have rw : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Tactic: rw [isPreconnected_iff_subset_of_fully_disjoint_closed hT]
-- 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}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
have a : f ⁻¹' {t'} ⊆ u ∪ v
Tactic: apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu 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}
t' : β
ht' : t' ∈ t
a : f ⁻¹' {t'} ⊆ u ∪ v
⊢ f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
have a₁ : f ⁻¹' {t'} ∩ (u ∩ v) = ∅
Tactic: apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu 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}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ∩ (u ∩ v) = ∅
have a : f ⁻¹' {t'} ∩ ∅ = ∅
Tactic: rw [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'_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'} ∩ ∅ = ∅
⊢ f ⁻¹' {t'} ∩ (u ∩ v) = ∅
have a₁ : Eq.{u + 1} (α := Set α) ∅ ∅
Tactic: rw [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}
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have fiber_decomp : ∀ 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]
-- 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
⊢ f ⁻¹' T₁ = f ⁻¹' t ∩ u
have a : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u
Tactic: apply eq_of_subset_of_subset
-- 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
a : f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u
⊢ f ⁻¹' T₁ = f ⁻¹' t ∩ u
have a₁ : f ⁻¹' t ∩ u ⊆ f ⁻¹' T₁
Tactic: apply eq_of_subset_of_subset
-- 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
⊢ f ⁻¹' T₁ ⊆ f ⁻¹' t ∩ u
have a : ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u
Tactic: rw [← biUnion_preimage_singleton]
-- 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
⊢ ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u
have a : ∀ (t' : β) (ht' : t' ∈ T₁), f ⁻¹' {t'} ⊆ f ⁻¹' t
Tactic: refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
-- 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' : β
ht' : t' ∈ T₁
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t
have a : t' ∈ t
Tactic: rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
-- 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ a ∈ f ⁻¹' T₁
have a₁ : f a ∈ t
Tactic: constructor
-- 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
a₁ : f a ∈ t
⊢ a ∈ f ⁻¹' T₁
have a₂ : f ⁻¹' {f a} ⊆ u
Tactic: constructor
-- 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
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f ⁻¹' {f a} ⊆ u
have a₁ : ∀ (h : f ⁻¹' {f a} ⊆ v), False
Tactic: refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_right fun h => ?_
-- 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
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
have T₁_u : 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)
-- 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₂ = f ⁻¹' t ∩ v
have a : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v
Tactic: apply eq_of_subset_of_subset
-- 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
a : f ⁻¹' T₂ ⊆ f ⁻¹' t ∩ v
⊢ f ⁻¹' T₂ = f ⁻¹' t ∩ v
have a₁ : f ⁻¹' t ∩ v ⊆ f ⁻¹' T₂
Tactic: apply eq_of_subset_of_subset
-- 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₂ ⊆ f ⁻¹' t ∩ v
have a : ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v
Tactic: rw [← biUnion_preimage_singleton]
-- 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
⊢ ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v
have a : ∀ (t' : β) (ht' : t' ∈ T₂), f ⁻¹' {t'} ⊆ f ⁻¹' t
Tactic: refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
-- 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' : β
ht' : t' ∈ T₂
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t
have a : t' ∈ t
Tactic: rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ a ∈ f ⁻¹' T₂
have a₁ : f a ∈ t
Tactic: constructor
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
a₁ : f a ∈ t
⊢ a ∈ f ⁻¹' T₂
have a₂ : f ⁻¹' {f a} ⊆ v
Tactic: constructor
-- 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
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ f ⁻¹' {f a} ⊆ v
have a₁ : ∀ (h : f ⁻¹' {f a} ⊆ u), False
Tactic: refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_