awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
have rw : Eq (α := 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))))
  (Set.preimage (β := ↥Y) (⇑(pullback.snd f ι ≫ ι)) (singleton (α := ↥Y) ((pullback.snd f ι ≫ ι) x : ↥Y)))
Tactic: rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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
⊢ 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 })) ↔
    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 ⋯}
have H : Eq (α := 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))))
  (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
Tactic: have H : pullback.snd f ι ⁻¹' {pullback.snd f ι x} =
        pullback.fst f ι ⁻¹' f ⁻¹' {f (pullback.fst f ι x)} := by
      rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]
      simp [← Set.image_singleton, Set.preimage_comp, Set.preimage_image_eq _ ι.injective]
-- 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 :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
⊢ Topology.IsOpenEmbedding f'
have a : Topology.IsOpenEmbedding f' ↔
  Topology.IsOpenEmbedding (X :=
    (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
          (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
      Type u))
    (Set.restrictPreimage (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))
      ⇑(pullback.fst f ι))
Tactic: convert!
        (f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding using 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : 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 ⋯}
have obtain : ∀ (R : CommRingCat.{u}) {f : X ⟶ 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 : ↥X) ↦
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
          x sorry}
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : 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 : ↥X) ↦
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
          x ⋯}
have inr : ∀
  (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 sorry})
  (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 sorry}
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inr :
  ∀
    (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),
    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 ⋯}
⊢ 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 ⋯}
have wlog : ∀ {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 sorry}
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, x, R, f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
x : ↥X
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
⊢ 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 ⋯}
have inr : ∀ (i : X.affineCover.I₀) (x : ↥(X.affineCover.X i)),
  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) sorry :
          { 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: obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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) ↔
    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 }))
have h : QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x
Tactic: convert! this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩ using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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
⊢ 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 }))
have 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) sorry :
        { 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 sorry}
Tactic: convert! this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩ using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : 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 ⋯}
have 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 sorry}
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, x, f, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
f : Spec S ⟶ Spec R
inst : 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 ⋯}
have 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 sorry}
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : 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 ⋯}
have inst : (CommRingCat.Hom.hom φ).FiniteType
Tactic: rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at ‹LocallyOfFiniteType (Spec.map φ)›
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
⊢ 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 ⋯}
have algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
⊢ 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 ⋯}
have rw : QuasiFiniteAt (Spec.map φ) x ↔ Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal
Tactic: rw [← Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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 ↔ Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal
have 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)
Tactic: trans Algebra.QuasiFinite (Localization.AtPrime (x.asIdeal.under R))
    (Localization.AtPrime x.asIdeal)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
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)
⊢ QuasiFiniteAt (Spec.map φ) x ↔ Algebra.QuasiFiniteAt (↑R : Type u) x.asIdeal
have 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
Tactic: trans Algebra.QuasiFinite (Localization.AtPrime (x.asIdeal.under R))
    (Localization.AtPrime x.asIdeal)