awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₁ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₂ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X) ⊓ 𝓟 t)) ⊥
rw₃ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓
        comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓟 t))
      ⊥
rw₄ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw₅ : Eq (α := Filter (↑s : Type u)) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (s ↓∩ t)) ⊥ ↔
  Eq (α := Filter { x : X // x ∈ s })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
have rw : 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {(↑x : X)}ᶜ] x = ⊥
Tactic: rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {(↑x : X)}ᶜ] x = ⊥
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
have rw₁ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {(↑x : X)})ᶜ] x = ⊥
Tactic: rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {(↑x : X)}ᶜ] x = ⊥
rw₁ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {(↑x : X)})ᶜ] x = ⊥
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
have rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ ↑{x})ᶜ] x = ⊥
Tactic: rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {(↑x : X)}ᶜ] x = ⊥
rw₁ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {(↑x : X)})ᶜ] x = ⊥
rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ ↑{x})ᶜ] x = ⊥
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
have rw₃ : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] x = ⊥
Tactic: rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
have rw : 𝓝[≠] x ≠ ⊥ ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
Tactic: rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x ≠ ⊥ ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
have rw₁ : 𝓝[≠] x ≠ ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S ≠ ⊥
Tactic: rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x ≠ ⊥ ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
rw₁ : 𝓝[≠] x ≠ ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S ≠ ⊥
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
have rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
Tactic: rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x ≠ ⊥ ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
rw₁ : 𝓝[≠] x ≠ ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S ≠ ⊥
rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
have rw₃ : 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
Tactic: rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
⊢ (s ∩ t)ᶜ.Finite
have rw : (sᶜ ∪ tᶜ).Finite
Tactic: rw [compl_inter]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋃₀ s)ᶜ.Finite
have rw : (⋂₀ (compl '' s)).Finite
Tactic: rw [compl_sUnion]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw : IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw₁ : IsOpen[TopologicalSpace.cofinite]
    (WithTopology.toTopology
        { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := sorry, isOpen_inter := sorry, isOpen_sUnion := sorry :
          TopologicalSpace X } ⁻¹'
      s) ↔
  s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
simp_rw₁ :
  IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
            isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw₂ : (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := sorry, isOpen_inter := sorry,
            isOpen_sUnion := sorry : TopologicalSpace X } ⁻¹'
        s).Nonempty →
    (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := sorry, isOpen_inter := sorry,
              isOpen_sUnion := sorry : TopologicalSpace X } ⁻¹'
          s)ᶜ.Finite ↔
  s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
simp_rw₁ :
  IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
            isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite
simp_rw₂ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw₃ : (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := sorry, isOpen_inter := sorry,
            isOpen_sUnion := sorry : TopologicalSpace X } ⁻¹'
        s).Nonempty →
    (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := sorry, isOpen_inter := sorry,
            isOpen_sUnion := sorry : TopologicalSpace X } ⁻¹'
        sᶜ).Finite ↔
  s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
simp_rw₁ :
  IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
            isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite
simp_rw₂ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite
simp_rw₃ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          sᶜ).Finite ↔
    s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw₄ : (WithTopology.ofTopology '' s).Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
simp_rw₁ :
  IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
            isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite
simp_rw₂ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite
simp_rw₃ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          sᶜ).Finite ↔
    s.Nonempty → sᶜ.Finite
simp_rw₄ : (WithTopology.ofTopology '' s).Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite
have simp_rw₅ : s.Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
Tactic: simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
x : CofiniteTopology X
⊢ 𝓝 x = pure x ⊔ cofinite
have h : ∀ (U : Set (CofiniteTopology X)), U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
have h : (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
Tactic: simp_rw [mem_nhds_iff, isOpen_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
have h : (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) → U ∈ pure x ⊔ cofinite
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
h : (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) → U ∈ pure x ⊔ cofinite
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
have h₁ : U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Constructions (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : MapClusterPt x la f
hg : MapClusterPt y lb g
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
have hf₁ : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
Tactic: rw [mapClusterPt_iff_frequently] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Constructions (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : MapClusterPt x la f
hg : MapClusterPt y lb g
hf₁ : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
have hg₁ : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
Tactic: rw [mapClusterPt_iff_frequently] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
have rw : ∀ (i : Prod.{u, v} (Set X) (Set Y)),
  i.1 ∈ 𝓝 x ∧ i.2 ∈ 𝓝 y → ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id i.1 ×ˢ id i.2
Tactic: rw [((𝓝 x).basis_sets.prod_nhds (𝓝 y).basis_sets).mapClusterPt_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id (s, t).1 ×ˢ id (s, t).2
have rw : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2
Tactic: rw [frequently_curry_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₃ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst] (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₃ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst] (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₄ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst] (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₃ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst] (f ⁻¹' {b})
rw₄ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst] (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₅ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₃ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst] (f ⁻¹' {b})
rw₄ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₅ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})
have rw₆ : IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b}) ↔ IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b})
Tactic: rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst_1] u
⊢ IsOpen[instTopologicalSpaceSubtype] ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u)
have h : Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) sorry) '' u) (Subtype.val (p := p) ⁻¹' f '' u)
Tactic: convert! (hf u hu).preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst_1] u
⊢ IsClosed[instTopologicalSpaceSubtype] ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u)
have h : Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) sorry) '' u) (Subtype.val (p := p) ⁻¹' f '' u)
Tactic: convert! (hf u hu).preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
⊢ Dense t ↔ s ⊆ closure[inst] ↑t
have rw : (∀ (x : X) (h : x ∈ s),
    (↑(mk (p := fun (x : X) ↦ x ∈ s) x h) : X) ∈ closure[inst] (val (p := fun (x : X) ↦ x ∈ s) '' t)) ↔
  s ⊆ closure[inst] ↑t
Tactic: rw [IsInducing.subtypeVal.dense_iff, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s
have rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
Tactic: rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s
have rw₁ : t ⊆ closure[inst] ↑(range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
Tactic: rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₁ : t ⊆ closure[inst] ↑(range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s
have rw₂ : t ⊆ closure[inst] (range (Subtype.val (p := fun (x : X) ↦ x ∈ t) ∘ inclusion (s := s) (t := t) hst)) ↔
  t ⊆ closure[inst] s
Tactic: rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]