awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
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))
obtain :
  ∀ (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
⊢ False

Tactic:
obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber _ _
      ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, PrimeSpectrum.ext (P.over_def p).symm⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.ext, inferInstance, PrimeSpectrum.preimageEquivFiber, Subtype.mk, Equiv.surjective, Ideal.over_def, Equiv.symm, Eq.symm
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
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 })
⊢ Algebra.WeaklyQuasiFiniteAt p.ResidueField (S := { asIdeal := p, isPrime := ⋯ : 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)
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : 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_4 : P.IsPrime
inst_5 : 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_4 } ⋯ :
      { x : PrimeSpectrum S //
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
          x })
inst :
  Algebra.WeaklyQuasiFiniteAt p.ResidueField (S := { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S)
    Q.asIdeal
⊢ False

Tactic:
Polynomial.not_weaklyQuasiFiniteAt (Q.asIdeal.comap g'.toRingHom) inferInstance

Premises used: inferInstance, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Ideal.comap, Polynomial.not_weaklyQuasiFiniteAt, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : 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_4 : P.IsPrime
inst_5 : 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_4 } ⋯ :
      { x : PrimeSpectrum S //
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
          x })
inst :
  Algebra.WeaklyQuasiFiniteAt p.ResidueField (S := { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S)
    Q.asIdeal
⊢ False

Tactic:
exact Polynomial.not_weaklyQuasiFiniteAt (Q.asIdeal.comap g'.toRingHom) inferInstance

Premises used: inferInstance, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Ideal.comap, Polynomial.not_weaklyQuasiFiniteAt, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
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.QuasiFiniteAt R P
⊢ ¬LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))

Tactic:
not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt f hf P

Premises used: Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
⊢ q =
    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))) ⊥

Tactic:
simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

Premises used: RingHom.ker_eq_comap_bot, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
⊢ 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
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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'
⊢ 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'
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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)))

Tactic:
Algebra.QuasiFinite.iff_of_algEquiv ((Ideal.quotientEquivAlg _ _ (.refl) ?_).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)).symm

Premises used: AlgEquiv.symm, Algebra.QuasiFinite.iff_of_algEquiv, AlgEquiv.trans, AlgEquiv.refl, Ideal.quotientEquivAlg, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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')
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)))
⊢ 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)))

Tactic:
refine Algebra.QuasiFinite.iff_of_algEquiv ((Ideal.quotientEquivAlg _ _ (.refl) ?_).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)).symm

Premises used: AlgEquiv.symm, Algebra.QuasiFinite.iff_of_algEquiv, AlgEquiv.trans, AlgEquiv.refl, Ideal.quotientEquivAlg, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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')
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
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
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))
⊢ 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:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 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:
simp [φ₁, IsScalarTower.algebraMap_eq R S (Localization.AtPrime q), ← Ideal.map_map,
    IsLocalization.mk'_mem_map_algebraMap_iff, IsLocalization.mk'_eq_zero_iff,
    Ideal.Quotient.mk_surjective.exists, ← map_mul, Ideal.Quotient.eq_zero_iff_mem,
    ← Ideal.mem_comap, ← hq']

Premises used: Function.Surjective.exists, Localization.AtPrime, IsLocalization.mk'_mem_map_algebraMap_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.mk_surjective, map_mul, Ideal.map_map, IsScalarTower.algebraMap_eq, IsLocalization.mk'_eq_zero_iff, Ideal.mem_comap