awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
this :
  ∀ {X : Scheme.{u}} {x : ↥X} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
h : QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x
h₁ :
  IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1)
            ((X.affineCover.f i) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1 })) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥(X.affineCover.X i)) ↦
          Membership.mem (γ := Set ↥(X.affineCover.X i))
            (Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) x_1)
          x ⋯}
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1)
            ((X.affineCover.f i) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1 }))

Tactic:
convert! this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩ using 1

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
this :
  ∀ {X : Scheme.{u}} {x : ↥X} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x

Tactic:
quasiFiniteAt_comp_iff_of_isOpenImmersion.symm

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
this :
  ∀ {X : Scheme.{u}} {x : ↥X} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x

Tactic:
exact quasiFiniteAt_comp_iff_of_isOpenImmersion.symm

Premises used: AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
this :
  ∀ {X : Scheme.{u}} {x : ↥X} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1)
            ((X.affineCover.f i) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1 })) ↔
    IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f (ι x) : ↥(Spec R)))) : Type u))
      {Set.restrictPreimage (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f (ι x) : ↥(Spec R)))) (⇑ι)
          (Subtype.mk (p := fun (x_1 : ↥(X.affineCover.X i)) ↦
            Membership.mem (γ := Set ↥(X.affineCover.X i))
              (Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) x_1)
            x ⋯)}

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) {x : ↥(Spec S)} {f : Spec S ⟶ Spec R} [LocallyOfFiniteType f],
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥(Spec S)) ↦
            Membership.mem (γ := Set ↥(Spec S))
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
          x ⋯}

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
f : Spec S ⟶ Spec R
inst : LocallyOfFiniteType f
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)],
    QuasiFiniteAt (Spec.map φ) x ↔
      IsOpen (X :=
        (↑(Set.preimage (β := ↥(Spec R)) (⇑(Spec.map φ)) (singleton (α := ↥(Spec R)) ((Spec.map φ) x : ↥(Spec R)))) :
          Type u))
        {Subtype.mk (p := fun (x_1 : ↥(Spec S)) ↦
            Membership.mem (γ := Set ↥(Spec S))
              (Set.preimage (β := ↥(Spec R)) (⇑(Spec.map φ)) (singleton (α := ↥(Spec R)) ((Spec.map φ) x : ↥(Spec R))))
              x_1)
            x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥(Spec S)) ↦
          Membership.mem (γ := Set ↥(Spec S))
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
          x ⋯}

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : LocallyOfFiniteType (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at ‹LocallyOfFiniteType (Spec.map φ)›

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.LocallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
⊢ Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
rw : QuasiFiniteAt (Spec.map φ) x ↔ Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑(Spec.map φ)) (singleton (α := ↥(Spec R)) ((Spec.map φ) x : ↥(Spec R)))) :
        Type u))
      {Subtype.mk (p := fun (x_1 : ↥(Spec S)) ↦
          Membership.mem (γ := Set ↥(Spec S))
            (Set.preimage (β := ↥(Spec R)) (⇑(Spec.map φ)) (singleton (α := ↥(Spec R)) ((Spec.map φ) x : ↥(Spec R))))
            x_1)
          x ⋯}

Tactic:
rw [← Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber]

Premises used: Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
trans :
  QuasiFiniteAt (Spec.map φ) x ↔
    Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal)
trans₁ :
  Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal) ↔
    Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔ Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal

Tactic:
trans Algebra.QuasiFinite (Localization.AtPrime (x.asIdeal.under R))
    (Localization.AtPrime x.asIdeal)

Premises used: CommRingCat.carrier, Algebra.QuasiFinite, Localization.AtPrime, PrimeSpectrum.asIdeal, Ideal.under
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
rw :
  QuasiFiniteAt (Spec.map φ) x ↔
    RingHom.QuasiFinite.{u, u} (R := Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (S := Localization.AtPrime x.asIdeal)
      (algebraMap (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
        (Localization.AtPrime x.asIdeal))
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal)

Tactic:
rw [← RingHom.quasiFinite_algebraMap]

Premises used: RingHom.quasiFinite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    RingHom.QuasiFinite.{u, u} (R := Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (S := Localization.AtPrime x.asIdeal)
      (algebraMap (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
        (Localization.AtPrime x.asIdeal))

Tactic:
RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso ..)

Premises used: IsLocalization.map, Set.Mem, OreLocalization, Localization.localRingHom, setOf, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, RingHom.QuasiFinite.respectsIso, IsLocalization.lift, AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, Quotient, Ideal.comap, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    RingHom.QuasiFinite.{u, u} (R := Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (S := Localization.AtPrime x.asIdeal)
      (algebraMap (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
        (Localization.AtPrime x.asIdeal))

Tactic:
exact RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso ..)

Premises used: RingHom.QuasiFinite.respectsIso, AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
⊢ Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal) ↔
    Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal

Tactic:
⟨fun _ ↦ .trans _ (Localization.AtPrime (x.asIdeal.under R)) _,
    fun _ ↦ .of_restrictScalars R _ _⟩

Premises used: Algebra.QuasiFinite.of_restrictScalars, CommRingCat.carrier, Localization.AtPrime, Algebra.QuasiFinite.trans, Iff.intro, PrimeSpectrum.asIdeal, Ideal.under
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
⊢ Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal) ↔
    Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal

Tactic:
exact ⟨fun _ ↦ .trans _ (Localization.AtPrime (x.asIdeal.under R)) _,
    fun _ ↦ .of_restrictScalars R _ _⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
hx : QuasiFiniteAt f x
⊢ IsOpen (X := ↥(fiber f (f x))) {asFiber f x}

Tactic:
have := Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber.mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
hx : QuasiFiniteAt f x
this : IsOpen (X := ↥(fiber f (f x))) {asFiber f x}
⊢ IsClopen (X := ↥(fiber f (f x))) {asFiber f x}

Tactic:
⟨isClosed_singleton_of_isLocallyClosed_singleton this.isLocallyClosed, this⟩

Premises used: isClosed_singleton_of_isLocallyClosed_singleton, IsOpen.isLocallyClosed, And.intro, IsClopen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
rw :
  (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ QuasiSeparatedSpace.{u_1} ↥X ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
rw [quasiSeparatedSpace_iff]

Premises used: quasiSeparatedSpace_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
mp :
  (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr :
  (∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))) →
    ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
U V : (↑X.affineOpens : Type u_1)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, SetLike.coe, TopologicalSpace.Opens.is_open', Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
U V : (↑X.affineOpens : Type u_1)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
exact H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, SetLike.coe, TopologicalSpace.Opens.is_open', Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↥X
hU : IsOpen U
hU' : IsCompact U
hV : IsOpen V
hV' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'

Premises used: TopologicalSpace.Opens.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↥X
hU : IsOpen U
hU' : IsCompact U
hV : IsOpen V
hV' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'

Premises used: TopologicalSpace.Opens.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
⊢ ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
suffices
      ∀ (U : X.Opens) (_ : IsCompact U.1) (V : X.Opens) (_ : IsCompact V.1),
        IsCompact (U ⊓ V).1
      by intro U V hU hU' hV hV'; exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
⊢ IsCompact (U ⊓ V).carrier

Tactic:
compact_open_induction_on V hV ?_ ?_

Premises used: AlgebraicGeometry.compact_open_induction_on
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
mpr : IsCompact (U ⊓ ⊥).carrier
mpr₁ :
  ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U_1 : (↑X.affineOpens : Type u_1)), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ (↑U_1 : X.Opens))).carrier
⊢ IsCompact (U ⊓ V).carrier

Tactic:
refine compact_open_induction_on V hV ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
⊢ IsCompact (U ⊓ ⊥).carrier

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
S : X.Opens
mpr :
  IsCompact S.carrier →
    ∀ (U_1 : (↑X.affineOpens : Type u_1)), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ (↑U_1 : X.Opens))).carrier
⊢ IsCompact S.carrier →
    ∀ (U_1 : (↑X.affineOpens : Type u_1)), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ (↑U_1 : X.Opens))).carrier

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV_1 : IsCompact V_1.carrier
S : X.Opens
h : IsCompact S.carrier
V : (↑X.affineOpens : Type u_1)
hV : IsCompact (U ⊓ S).carrier
mpr : IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact (U.carrier ∩ (S.carrier ∪ (↑(↑V : X.Opens) : Set ↥X)))

Tactic:
rw [Set.inter_union_distrib_left]

Premises used: Set.inter_union_distrib_left