awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
refine_1 :
  LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
have refine_2 : ∀
  (e :
    Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
      (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)),
  False
Tactic: refine lt_of_le_of_ne (Ideal.map_le_iff_le_comap.mpr ?_) fun e ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
⊢ LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
have refine_1 : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.comap (F := R →+* S) (RingHom.comp (↑f : R[X] →+* S) C) P)
Tactic: rw [Ideal.comap_comap, ← algebraMap_eq, f.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
refine_1 : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.comap (F := R →+* S) (RingHom.comp (↑f : R[X] →+* S) C) P)
⊢ LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
have refine_1₁ : LE.le (α := Ideal R) (Ideal.under R P)
  (Ideal.comap (F := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R[X] →+* S) (algebraMap R R[X])) P)
Tactic: rw [Ideal.comap_comap, ← algebraMap_eq, f.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
refine_1 : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.comap (F := R →+* S) (RingHom.comp (↑f : R[X] →+* S) C) P)
refine_1₁ :
  LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R[X] →+* S) (algebraMap R R[X])) P)
⊢ LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
have refine_1₂ : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.under R P)
Tactic: rw [Ideal.comap_comap, ← algebraMap_eq, f.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ False
have this₁ : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
Tactic: have : Module.Finite (Ideal.under R P).ResidueField P.ResidueField :=
    Algebra.WeaklyQuasiFiniteAt.finite_residueField ..
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
⊢ False
have this₁ : Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))
Tactic: have : Module.Finite (P.under R).ResidueField (P.under R[X]).ResidueField :=
    .of_injective (IsScalarTower.toAlgHom _ _ P.ResidueField).toLinearMap
      (algebraMap (P.under R[X]).ResidueField P.ResidueField).injective
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this_4 : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
this :
  Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))
⊢ False
have this₁ : Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (RatFunc (Ideal.ResidueField (Ideal.under R P)))
Tactic: have : Module.Finite (P.under R).ResidueField (RatFunc (P.under R).ResidueField) :=
    .of_surjective (residueFieldMapCAlgEquiv _ (P.under _) e.symm).toLinearMap
      (residueFieldMapCAlgEquiv _ (P.under _) e.symm).surjective
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
⊢ Eq (α := Ideal p.ResidueField[X])
    (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥
have rw : LE.le (α := Ideal R[X]) (RingHom.ker f)
  (Ideal.comap (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) ⊥)
Tactic: rw [← le_bot_iff, Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
⊢ False
have H' : Eq (α := Ideal p.ResidueField[X])
  (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥
Tactic: have H' : (RingHom.ker f).map (mapRingHom (algebraMap R p.ResidueField)) = ⊥ := by
    rw [← le_bot_iff, Ideal.map_le_iff_le_comap]
    intro x hx
    simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using H hx
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
H' :
  Eq (α := Ideal p.ResidueField[X])
    (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥
g' : p.ResidueField[X] ≃ₐ[p.ResidueField] p.Fiber S :=
  AlgEquiv.trans
    (AlgEquiv.trans (AlgEquiv.symm (AlgEquiv.quotientBot p.ResidueField p.ResidueField[X]))
      (Ideal.quotientEquivAlgOfEq p.ResidueField ⋯))
    (AlgEquiv.symm (fiberEquivQuotient f hf p))
⊢ False
have obtain : ∀ (Q : PrimeSpectrum ({ asIdeal := p, isPrime := sorry : PrimeSpectrum R }.asIdeal.Fiber S))
  (hQ :
    Eq.{u_2 + 1} (α :=
      (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }}) :
        Type u_2))
      ((Equiv.symm (PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := sorry }) :
            (a : PrimeSpectrum ({ asIdeal := p, isPrime := sorry }.asIdeal.Fiber S)) →
              (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := sorry }}) : Type u_2))
          Q :
        (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }}) :
          Type u_2))
      (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }})
            x)
          { asIdeal := P, isPrime := inst_3 } sorry :
        { x : PrimeSpectrum S //
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }})
            x })),
  False
Tactic: obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber _ _
      ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, PrimeSpectrum.ext (P.over_def p).symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
H' :
  Eq (α := Ideal p.ResidueField[X])
    (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥
g' : p.ResidueField[X] ≃ₐ[p.ResidueField] p.Fiber S :=
  AlgEquiv.trans
    (AlgEquiv.trans (AlgEquiv.symm (AlgEquiv.quotientBot p.ResidueField p.ResidueField[X]))
      (Ideal.quotientEquivAlgOfEq p.ResidueField ⋯))
    (AlgEquiv.symm (fiberEquivQuotient f hf p))
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S)
hQ :
  Eq.{u_2 + 1} (α :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
      Type u_2))
    ((Equiv.symm (PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ }) :
          (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S)) →
            (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2))
        Q :
      (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
        Type u_2))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
          x)
        { asIdeal := P, isPrime := inst_3 } ⋯ :
      { x : PrimeSpectrum S //
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
          x })
⊢ False
have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField (S := { asIdeal := p, isPrime := sorry : PrimeSpectrum R }.asIdeal.Fiber S)
  Q.asIdeal
Tactic: have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
    .baseChange P Q.asIdeal congr($(hQ.symm).1.1)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
q' : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
⊢ WeaklyQuasiFiniteAt R q ↔
    QuasiFinite.{u_1, u_2} R
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
have hq' : q =
  Ideal.comap (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q'
Tactic: have hq' : q = q'.comap (Ideal.Quotient.mk _) := .trans
    (by simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le])
    (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
q' : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
hq' :
  q =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) hq'
⊢ WeaklyQuasiFiniteAt R q ↔
    QuasiFinite.{u_1, u_2} R
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
have hφ₁ : Function.Surjective (α := Localization.AtPrime q) (β := Localization.AtPrime q')
  (⇑φ₁ : (a : Localization.AtPrime q) → Localization.AtPrime q')
Tactic: have hφ₁ : Function.Surjective φ₁ :=
    (RingHom.surjectiveOnStalks_of_surjective
      Ideal.Quotient.mk_surjective).localRingHom_surjective _ _ hq'
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
q' : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
hq' :
  q =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) hq'
hφ₁ :
  Function.Surjective (α := Localization.AtPrime q) (β := Localization.AtPrime q')
    (⇑φ₁ : (a : Localization.AtPrime q) → Localization.AtPrime q')
⊢ WeaklyQuasiFiniteAt R q ↔
    QuasiFinite.{u_1, u_2} R
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
have refine : Eq (α := Ideal (Localization.AtPrime q)) (RingHom.ker φ₁)
  (Ideal.map (R := Localization.AtPrime q) (F := Localization.AtPrime q →+* Localization.AtPrime q)
    (↑AlgEquiv.refl : Localization.AtPrime q →+* Localization.AtPrime q)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.under R q)))
Tactic: refine Algebra.QuasiFinite.iff_of_algEquiv ((Ideal.quotientEquivAlg _ _ (.refl) ?_).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)).symm
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
q' : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
hq' :
  q =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) hq'
hφ₁ :
  Function.Surjective (α := Localization.AtPrime q) (β := Localization.AtPrime q')
    (⇑φ₁ : (a : Localization.AtPrime q) → Localization.AtPrime q')
⊢ Eq (α := Ideal (Localization.AtPrime q)) (RingHom.ker φ₁)
    (Ideal.map (R := Localization.AtPrime q) (F := Localization.AtPrime q →+* Localization.AtPrime q)
      (↑AlgEquiv.refl : Localization.AtPrime q →+* Localization.AtPrime q)
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
have h : ∀ (x : Localization.AtPrime q),
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (RingHom.ker φ₁) x ↔
    Membership.mem (γ := Ideal (Localization.AtPrime q))
      (Ideal.map (R := Localization.AtPrime q) (F := Localization.AtPrime q →+* Localization.AtPrime q)
        (↑AlgEquiv.refl : Localization.AtPrime q →+* Localization.AtPrime q)
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
q' : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
hq' :
  q =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) hq'
hφ₁ :
  Function.Surjective (α := Localization.AtPrime q) (β := Localization.AtPrime q')
    (⇑φ₁ : (a : Localization.AtPrime q) → Localization.AtPrime q')
x : Localization.AtPrime q
⊢ Membership.mem (γ := Ideal (Localization.AtPrime q)) (RingHom.ker φ₁) x ↔
    Membership.mem (γ := Ideal (Localization.AtPrime q))
      (Ideal.map (R := Localization.AtPrime q) (F := Localization.AtPrime q →+* Localization.AtPrime q)
        (↑AlgEquiv.refl : Localization.AtPrime q →+* Localization.AtPrime q)
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
      x
have h : ∀ (x s : S) (hs : s ∈ q.primeCompl),
  Membership.mem (γ := Ideal (Localization.AtPrime q)) (RingHom.ker φ₁)
      (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) ↔
    Membership.mem (γ := Ideal (Localization.AtPrime q))
      (Ideal.map (R := Localization.AtPrime q) (F := Localization.AtPrime q →+* Localization.AtPrime q)
        (↑AlgEquiv.refl : Localization.AtPrime q →+* Localization.AtPrime q)
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
      (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs))
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
p : Ideal R
q : Ideal S
inst_5 : q.IsPrime
inst_6 : QuasiFiniteAt R q
⊢ WeaklyQuasiFiniteAt R q
have rw : QuasiFinite.{u_1, u_2} R
  (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.under R q)))
Tactic: rw [weaklyQuasiFiniteAt_iff]