awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
⊢ Eq.{u_1 + 1} (α := Set (Set α))
    {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen[scott α univ] u ∧ u \ (↑(upperClosure t) : Set α) = s}
    {c : Set α |
      ∃ (a : Set (WithLower α)),
        Membership.mem (γ := Set (Set (WithLower α)))
            {s : Set (WithLower α) | ∃ (t : Set (WithLower α)), t.Finite ∧ (↑(upperClosure t) : Set (WithLower α))ᶜ = s}
            a ∧
          ∃ (b : Set (WithScott α)),
            Membership.mem (γ := Set (Set (WithScott α))) {U : Set (WithScott α) | IsOpen[scott α univ] U} b ∧
              (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' a ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' b =
                c}
have simp_rw : Eq.{u_1 + 1} (α := Set (Set α))
  {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen[scott α univ] u ∧ (↑(upperClosure t) : Set α)ᶜ ∩ u = s}
  {c : Set α |
    ∃ (a : Set (WithLower α)),
      Membership.mem (γ := Set (Set (WithLower α)))
          {s : Set (WithLower α) | ∃ (t : Set (WithLower α)), t.Finite ∧ (↑(upperClosure t) : Set (WithLower α))ᶜ = s}
          a ∧
        ∃ (b : Set (WithScott α)),
          Membership.mem (γ := Set (Set (WithScott α))) {U : Set (WithScott α) | IsOpen[scott α univ] U} b ∧
            (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' a ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' b = c}
Tactic: simp_rw [diff_eq_compl_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
⊢ IsTopologicalBasis (lawsonBasis α)
have lawsonBasis_image2 : lawsonBasis α =
  image2
    (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
      (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
    (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
Tactic: have lawsonBasis_image2 : lawsonBasis α =
      (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1)
        (IsLower.lowerBasis (WithLower α)) {U | IsOpen[scott α univ] U}) := by
    rw [lawsonBasis, image2, IsLower.lowerBasis]
    simp_rw [diff_eq_compl_inter]
    aesop
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
⊢ IsTopologicalBasis (lawsonBasis α)
have rw : IsTopologicalBasis.{u_1} (α := α)
  (image2
    (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
      (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
    (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U})
Tactic: rw [lawsonBasis_image2]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
⊢ IsTopologicalBasis.{u_1} (α := α)
    (image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U})
have h : inst_1 =
  induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
    induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
Tactic: convert!
    IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis
      (isTopologicalBasis_opens (α := WithScott α)) WithLower.toLower WithScott.toScott
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
⊢ inst_1 =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
have h : lower α ⊓ scott α univ =
  induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
    induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
Tactic: rw [@topology_eq_lawson α _ _ _, lawson]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
⊢ lower α ⊓ scott α univ =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
have apply : lower α = induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace
Tactic: apply (congrArg₂ min _) _
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
apply : lower α = induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace
⊢ lower α ⊓ scott α univ =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
have apply₁ : scott α univ = induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
Tactic: apply (congrArg₂ min _) _
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
⊢ L ≤ S
have rw : lawson α ≤ scott α univ
Tactic: rw [@IsScott.topology_eq α univ _ S _, @IsLawson.topology_eq_lawson α _ L _]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L : TopologicalSpace α
inst_1 : IsLawson α
⊢ scottHausdorff α univ ≤ L
have rw : scottHausdorff α univ ≤ lawson α
Tactic: rw [@IsLawson.topology_eq_lawson α _ L _]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[L] s ↔ IsOpen[S] s
have rw : IsOpen[lawson α] s ↔ IsOpen[scott α univ] s
Tactic: rw [@IsLawson.topology_eq_lawson α _ L _, @IsScott.topology_eq α univ _ S _]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ IsClosed[S] s
have rw : IsOpen[L] sᶜ ↔ IsClosed[S] s
Tactic: rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
    (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
rw : IsOpen[L] sᶜ ↔ IsClosed[S] s
⊢ IsClosed[L] s ↔ IsClosed[S] s
have rw₁ : IsOpen[L] sᶜ ↔ IsOpen[S] sᶜ
Tactic: rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
    (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
rw : IsOpen[L] sᶜ ↔ IsClosed[S] s
rw₁ : IsOpen[L] sᶜ ↔ IsOpen[S] sᶜ
⊢ IsClosed[L] s ↔ IsClosed[S] s
have rw₂ : IsOpen[S] sᶜ ↔ IsOpen[S] sᶜ
Tactic: rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
    (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ DirSupClosed s
have rw : IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s
Tactic: rw [lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h,
    @IsScott.isClosed_iff_isLowerSet_and_dirSupClosed]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[inst_1] {a}
have simp : IsClosed[lawson α] {a}
Tactic: simp +instances only [IsLawson.topology_eq_lawson]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[lawson α] {a}
have rw : IsClosed[WithLawson.instTopologicalSpace]
  ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹' ((↑(upperClosure {a}) : Set α) ∩ (↑(lowerClosure {a}) : Set α)))
Tactic: rw [← (Set.OrdConnected.upperClosure_inter_lowerClosure ordConnected_singleton),
      ← WithLawson.isClosed_preimage_ofLawson]
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹'
      ((↑(upperClosure {a}) : Set α) ∩ (↑(lowerClosure {a}) : Set α)))
have apply : IsClosed[WithLawson.instTopologicalSpace] (↑(lowerClosure {a}) : Set α)
Tactic: apply IsClosed.inter
      (lawsonClosed_of_lowerClosed _ (IsLower.isClosed_upperClosure (finite_singleton a)))
-- Lean 4 proof step from Mathlib.Topology.Order.LawsonTopology (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] (↑(lowerClosure {a}) : Set α)
have rw : IsClosed[WithLawson.instTopologicalSpace]
  ((⇑WithLawson.ofLawson : (a : WithLawson (WithLawson α)) → WithLawson α) ⁻¹' Iic a)
Tactic: rw [lowerClosure_singleton, LowerSet.coe_Iic, ← WithLawson.isClosed_preimage_ofLawson]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ interior s = ∅
have refine : ∀ (x : α) (hx : x ∈ interior s), False
Tactic: refine eq_empty_of_forall_notMem fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
⊢ False
have this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
Tactic: have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
⊢ False
have rcases : ∀ (y : α) (hyx : y < x) (hys : y ∈ s), False
Tactic: rcases this.exists_lt with ⟨y, hyx, hys⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a
have rw : 𝓝[Iic a ∪ Ici a] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ici a] a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a
have rw₁ : 𝓝[univ] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ici a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a
have rw₂ : 𝓝 a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw : 𝓝[s ∩ Iic a ∪ s ∩ Ici a] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ici a] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₁ : 𝓝[s ∩ (Iic a ∪ Ici a)] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ici a)] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ici a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₃ : 𝓝[s] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a
have rw : 𝓝[Iio a ∪ Ici a] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iio a ∪ Ici a] a = 𝓝 a
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a
have rw₁ : 𝓝[univ] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iio a ∪ Ici a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a
have rw₂ : 𝓝 a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw : 𝓝[s ∩ Iio a ∪ s ∩ Ici a] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ici a] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₁ : 𝓝[s ∩ (Iio a ∪ Ici a)] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ici a)] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ici a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a
have rw₃ : 𝓝[s] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
have rw : 𝓝[Iic a ∪ Ioi a] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ioi a] a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
have rw₁ : 𝓝[univ] a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ioi a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
have rw₂ : 𝓝 a = 𝓝 a
Tactic: rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a
have rw : 𝓝[s ∩ Iic a ∪ s ∩ Ioi a] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ioi a] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a
have rw₁ : 𝓝[s ∩ (Iic a ∪ Ioi a)] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ioi a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ioi a)] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a
have rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ioi a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ioi a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a
have rw₃ : 𝓝[s] a = 𝓝[s] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
⊢ 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a
have rw : 𝓝[Iio a ∪ Ioi a] a = 𝓝[≠] a
Tactic: rw [← nhdsWithin_union, Iio_union_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iio a ∪ Ioi a] a = 𝓝[≠] a
⊢ 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a
have rw₁ : 𝓝[≠] a = 𝓝[≠] a
Tactic: rw [← nhdsWithin_union, Iio_union_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw₂ : 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
rw₂ : 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw₃ : 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
rw₂ : 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a
rw₃ : 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw₄ : 𝓝[univ ∩ (s \ {a})] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
rw₂ : 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a
rw₃ : 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a
rw₄ : 𝓝[univ ∩ (s \ {a})] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a
have rw₅ : 𝓝[s \ {a}] a = 𝓝[s \ {a}] a
Tactic: rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
have rw : ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a
Tactic: rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
rw : ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
have rw₁ : ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
Tactic: rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]