awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
e : (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) :
    Type u) ≃ₐ[(↑Γ(X, V) : Type u)]
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal.primeCompl
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
have rw : RingHom.QuasiFinite.{u, u} (R := (↑Γ(Y, U) : Type u)) (S :=
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
  (algebraMap (↑Γ(Y, U) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal))
Tactic: rw [RingHom.QuasiFiniteAt, Algebra.QuasiFiniteAt, ← RingHom.quasiFinite_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
e : (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) :
    Type u) ≃ₐ[(↑Γ(X, V) : Type u)]
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal.primeCompl
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
⊢ RingHom.QuasiFinite.{u, u} (R := (↑Γ(Y, U) : Type u)) (S :=
    Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
    (algebraMap (↑Γ(Y, U) : Type u)
      (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal))
have h : algebraMap (↑Γ(Y, U) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal) =
  e.toRingEquiv.toRingHom.comp
    ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) sorry)))
Tactic: convert! (RingHom.QuasiFinite.of_finite e.finite).comp (hx.comp H)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
x : ↥X
⊢ QuasiFiniteAt f x
have refine : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.QuasiFinite →
    ∀ (J : Ideal S) (x : J.IsPrime),
      RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
        (Localization.localRingHom (Ideal.comap f J) J f sorry)
Tactic: refine HasRingHomProperty.stalkMap ?_ ‹_› x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
⊢ RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
    (Localization.localRingHom (Ideal.comap f J) J f ⋯)
have algebraizeInst : Algebra.QuasiFinite R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
⊢ RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
    (Localization.localRingHom (Ideal.comap f J) J f ⋯)
have refine : RingHom.QuasiFinite (S := Localization.AtPrime J)
  (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f sorry)
    (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
Tactic: refine .of_comp (g := algebraMap R _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
⊢ RingHom.QuasiFinite (S := Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
have h : Eq (α := R →+* Localization.AtPrime J)
  (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f sorry)
    (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
  (algebraMap R (Localization.AtPrime J))
Tactic: convert!
    RingHom.quasiFinite_algebraMap.mpr
      (inferInstance : Algebra.QuasiFinite R (Localization.AtPrime J))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
⊢ Eq (α := R →+* Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
    (algebraMap R (Localization.AtPrime J))
have h : ∀ (x : R),
  Eq (α := Localization.AtPrime J)
    ((RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f sorry)
            (algebraMap R (Localization.AtPrime (Ideal.comap f J))) :
          (a : R) → Localization.AtPrime J)
        x :
      Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
x_1 : R
⊢ Eq (α := Localization.AtPrime J)
    ((RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
            (algebraMap R (Localization.AtPrime (Ideal.comap f J))) :
          (a : R) → Localization.AtPrime J)
        x_1 :
      Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x_1 : Localization.AtPrime J)
have h : Eq (α := Localization.AtPrime J)
  ((algebraMap S (Localization.AtPrime J) : (a : S) → Localization.AtPrime J) ((f : (a : R) → S) x_1) :
    Localization.AtPrime J)
  ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x_1 : Localization.AtPrime J)
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst : LocallyQuasiFinite g
⊢ QuasiFiniteAt (f ≫ g) x ↔ QuasiFiniteAt f x
have simp : (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
Tactic: simp only [QuasiFiniteAt, stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)
have rw : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))
Tactic: rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
rw : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)
have rw₁ : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))
Tactic: rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
rw : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))
rw₁ : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)
have rw₂ : QuasiFiniteAt f x ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
Tactic: rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
rw : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))
rw₁ : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))
rw₂ : QuasiFiniteAt f x ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)
have rw₃ : (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
Tactic: rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
⊢ QuasiFiniteAt f x ↔ IsOpen (X := ↥(fiber f (f x))) {asFiber f x}
have rw : QuasiFiniteAt f x ↔
  IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
    (Set.image (α := ↥(fiber f (f x))) (⇑(fiberHomeo f (f x)) : (a : ↥(fiber f (f x))) → (↑(⇑f ⁻¹' {f x}) : Type u))
      {asFiber f x})
Tactic: rw [← (f.fiberHomeo (f x)).isOpen_image]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      (Set.image (α := ↥(fiber f (f x))) (⇑(fiberHomeo f (f x)) : (a : ↥(fiber f (f x))) → (↑(⇑f ⁻¹' {f x}) : Type u))
        {asFiber f x})
have simp : QuasiFiniteAt f x ↔
  IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
    {Subtype.mk (p := fun (x_1 : ↥X) ↦
        Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x sorry}
Tactic: simp only [Set.image_singleton, asFiber, Homeomorph.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
      QuasiFiniteAt f x ↔
        IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
          {Subtype.mk (p := fun (x_1 : ↥X) ↦
              Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x sorry})
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
  QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x sorry}
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        QuasiFiniteAt f x ↔
          IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
            {Subtype.mk (p := fun (x_1 : ↥X) ↦
                Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯})
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x sorry}
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
have inr : ∀ (i : Y.affineCover.I₀) (y : ↥(Y.affineCover.X i)) (hy : Eq (α := ↥Y) ((Y.affineCover.f i) y : ↥Y) (f x : ↥Y)),
  QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x sorry}
Tactic: obtain ⟨i, y, hy⟩ := Y.affineCover.exists_eq (f x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
y : ↥(Y.affineCover.X i)
hy : Eq (α := ↥Y) ((Y.affineCover.f i) y : ↥Y) (f x : ↥Y)
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
have inr : ∀ (x : ↥(pullback f (Y.affineCover.f i)))
  (hy :
    Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
      (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)),
  QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1)
            ((pullback.fst f (Y.affineCover.f i)) x) sorry :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1 }))
Tactic: obtain ⟨x, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback _ _ hy.symm
Cleared hypotheses: x, y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1)
            ((pullback.fst f (Y.affineCover.f i)) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1 }))
have h : QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x
Tactic: convert! this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩ using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
h : QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1)
            ((pullback.fst f (Y.affineCover.f i)) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1 }))
have h₁ : IsOpen (X :=
    (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
      Type u))
    (singleton (α :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
            x_1)
          ((pullback.fst f (Y.affineCover.f i)) x) sorry :
        { x_1 : ↥X //
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
            x_1 })) ↔
  IsOpen (X :=
    (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
          (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
      Type u))
    {Subtype.mk (p := fun (x_1 : ↥(pullback f ι)) ↦
        Membership.mem (γ := Set ↥(pullback f ι))
          (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
            (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
          x_1)
        x sorry}
Tactic: convert! this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩ using 1