-- Mathlib/Topology/Order/LawsonTopology.lean
theorem isTopologicalBasis : TopologicalSpace.IsTopologicalBasis (lawsonBasis α)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
x✝ : TopologicalSpace α := scott α univ
⊢ scott α univ = induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Tactic:
exact (@IsScott.withScottHomeomorph α _ (scott α univ) ⟨rfl⟩).isInducing.eq_induced

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
x✝ : TopologicalSpace α := lower α
⊢ lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpace

Tactic:
exact (@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen u ∧ u \ ↑(upperClosure t) = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}

Tactic:
simp_rw [diff_eq_compl_inter]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen u ∧ (↑(upperClosure t))ᶜ ∩ u = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen u ∧ (↑(upperClosure t))ᶜ ∩ u = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpace

Tactic:
letI _ := lower α

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
x✝ : TopologicalSpace α := lower α
⊢ lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpace

Proof state:
case h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ inst✝¹ =
    induced (⇑WithLower.toLower) WithLower.instTopologicalSpace ⊓
      induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Tactic:
rw [@topology_eq_lawson α _ _ _, lawson]

Result:
case h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ lower α ⊓ scott α univ =
    induced (⇑WithLower.toLower) WithLower.instTopologicalSpace ⊓
      induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}

Tactic:
rw [lawsonBasis, image2, IsLower.lowerBasis]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen u ∧ u \ ↑(upperClosure t) = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ IsTopologicalBasis (lawsonBasis α)

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

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ IsTopologicalBasis (lawsonBasis α)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ IsTopologicalBasis
    (image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U})

Tactic:
convert IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis
  (isTopologicalBasis_opens (α := WithScott α))
  WithLower.toLower WithScott.toScott

Result:
case h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ inst✝¹ =
    induced (⇑WithLower.toLower) WithLower.instTopologicalSpace ⊓
      induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ scott α univ = induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Tactic:
letI _ := scott α univ

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
x✝ : TopologicalSpace α := scott α univ
⊢ scott α univ = induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ IsTopologicalBasis (lawsonBasis α)

Tactic:
rw [lawsonBasis_image2]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ IsTopologicalBasis
    (image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U})