-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isBasis_basicOpen (X : Scheme) [IsAffine X] :
    Opens.IsBasis (Set.range (X.basicOpen : Γ(X, ⊤) → X.Opens))

Proof state:
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ↑(X.basicOpen x) = ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x)

Tactic:
exact congr_arg Opens.carrier (Scheme.toSpecΓ_preimage_basicOpen _ _).symm

Result:
no goals

Proof state:
case h.e'_3.h.mp
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x ∈ Set.range X.basicOpen, ↑x = x✝) →
    ∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝

Tactic:
rintro ⟨_, ⟨x, rfl⟩, rfl⟩

Result:
case h.e'_3.h.mp.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ∃ x_1,
    (∃ x ∈ Set.range PrimeSpectrum.basicOpen, ↑x = x_1) ∧
      ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x_1 = ↑(X.basicOpen x)

Proof state:
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ∃ x_1 ∈ Set.range X.basicOpen,
    ↑x_1 = ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x)

Tactic:
refine ⟨_, ⟨x, rfl⟩, ?_⟩

Result:
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ↑(X.basicOpen x) = ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x)

Proof state:
case h.e'_3.h.mpr
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝) →
    ∃ x ∈ Set.range X.basicOpen, ↑x = x✝

Tactic:
rintro ⟨_, ⟨_, ⟨x, rfl⟩, rfl⟩, rfl⟩

Result:
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ∃ x_1 ∈ Set.range X.basicOpen,
    ↑x_1 = ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x)

Proof state:
X : Scheme
inst✝ : IsAffine X
⊢ IsTopologicalBasis (SetLike.coe '' Set.range X.basicOpen)

Tactic:
convert PrimeSpectrum.isBasis_basic_opens.isInducing
  (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing using 1

Result:
case h.e'_3
X : Scheme
inst✝ : IsAffine X
⊢ SetLike.coe '' Set.range X.basicOpen =
    Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ''
      (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)

Proof state:
case h.e'_3.h
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ x✝ ∈ SetLike.coe '' Set.range X.basicOpen ↔
    x✝ ∈
      Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ''
        (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)

Tactic:
simp only [Set.mem_image, exists_exists_eq_and]

Result:
case h.e'_3.h
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x ∈ Set.range X.basicOpen, ↑x = x✝) ↔
    ∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝

Proof state:
case h.e'_3.h.mp.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ∃ x_1,
    (∃ x ∈ Set.range PrimeSpectrum.basicOpen, ↑x = x_1) ∧
      ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x_1 = ↑(X.basicOpen x)

Tactic:
refine ⟨_, ⟨_, ⟨x, rfl⟩, rfl⟩, ?_⟩

Result:
case h.e'_3.h.mp.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x) = ↑(X.basicOpen x)

Proof state:
case h.e'_3
X : Scheme
inst✝ : IsAffine X
⊢ SetLike.coe '' Set.range X.basicOpen =
    Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ''
      (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)

Tactic:
ext

Result:
case h.e'_3.h
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ x✝ ∈ SetLike.coe '' Set.range X.basicOpen ↔
    x✝ ∈
      Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ''
        (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)

Proof state:
X : Scheme
inst✝ : IsAffine X
⊢ Opens.IsBasis (Set.range X.basicOpen)

Tactic:
delta Opens.IsBasis

Result:
X : Scheme
inst✝ : IsAffine X
⊢ IsTopologicalBasis (SetLike.coe '' Set.range X.basicOpen)

Proof state:
case h.e'_3.h
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x ∈ Set.range X.basicOpen, ↑x = x✝) ↔
    ∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝

Tactic:
constructor

Result:
case h.e'_3.h.mp
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x ∈ Set.range X.basicOpen, ↑x = x✝) →
    ∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝

case h.e'_3.h.mpr
X : Scheme
inst✝ : IsAffine X
x✝ : Set ↑↑X.toPresheafedSpace
⊢ (∃ x,
      (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧
        ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝) →
    ∃ x ∈ Set.range X.basicOpen, ↑x = x✝

Proof state:
case h.e'_3.h.mp.intro.intro.intro
X : Scheme
inst✝ : IsAffine X
x : ↑Γ(X, ⊤)
⊢ ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen x) = ↑(X.basicOpen x)

Tactic:
exact congr_arg Opens.carrier (Scheme.toSpecΓ_preimage_basicOpen _ _)

Result:
no goals