awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
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)))
⊢ WeaklyQuasiFiniteAt R q

Tactic:
rw [weaklyQuasiFiniteAt_iff]

Premises used: Algebra.weaklyQuasiFiniteAt_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
⊢ 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:
.of_surjective_algHom (Ideal.Quotient.mkₐ _ _) Ideal.Quotient.mk_surjective

Premises used: Algebra.QuasiFinite.of_surjective_algHom, Ideal.Quotient.mk_surjective, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
⊢ 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:
exact .of_surjective_algHom (Ideal.Quotient.mkₐ _ _) Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
rw :
  QuasiFinite.{u_1, u_2} R
      (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
          (Ideal.under R p))) →
    ∀ (q : Ideal T) [inst_9 : q.IsPrime]
      (f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q))
      (hf :
        Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
          (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)),
      QuasiFinite.{u_1, u_3} R
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (Ideal.under R q)))
⊢ WeaklyQuasiFiniteAt R q

Tactic:
rw [weaklyQuasiFiniteAt_iff] at *

Premises used: Algebra.weaklyQuasiFiniteAt_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
rw :
  LE.le (α := Ideal R) (Ideal.under R p)
    (Ideal.comap (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
      (Ideal.under R p))
    (Ideal.comap f.toRingHom
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
rw [Ideal.map_le_iff_le_comap, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
      AlgHom.comp_algebraMap_of_tower]

Premises used: AlgHom.comp_algebraMap_of_tower, Ideal.map_le_iff_le_comap, AlgHom.toRingHom_eq_coe, Ideal.comap_comap
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
grw : LE.le (α := Ideal R) (Ideal.under R p) (Ideal.under R q)
⊢ LE.le (α := Ideal R) (Ideal.under R p)
    (Ideal.comap (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
grw [← Ideal.le_comap_map]

Premises used: Ideal.le_comap_map
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
by_contra : ∀ (hx' : x ∉ Ideal.under R q), False
⊢ Membership.mem (γ := Submodule R R) (Ideal.under R q) x

Tactic:
by_contra hx'
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
⊢ IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom

Tactic:
have : IsLocalHom f.toRingHom := .of_surjective _ hf
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this_1 : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
this :
  IsUnit.{u_3} (M := Localization.AtPrime q)
    (IsLocalization.mk' (R := T) (M := q.primeCompl) (Localization.AtPrime q) ((algebraMap R T : (a : R) → T) x : T)
      (1 : ↥q.primeCompl))
⊢ IsUnit.{u_3} (M := Localization.AtPrime q)
    ((f.toRingHom : (a : Localization.AtPrime p) → Localization.AtPrime q)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x) :
      Localization.AtPrime q)

Tactic:
simpa [IsLocalization.mk'_one] using this

Premises used: IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
suffices :
  IsUnit.{u_3} (M := Localization.AtPrime q)
    (IsLocalization.mk' (R := T) (M := q.primeCompl) (Localization.AtPrime q) ((algebraMap R T : (a : R) → T) x : T)
      (1 : ↥q.primeCompl))
⊢ IsUnit.{u_3} (M := Localization.AtPrime q)
    ((f.toRingHom : (a : Localization.AtPrime p) → Localization.AtPrime q)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x) :
      Localization.AtPrime q)

Tactic:
suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
⊢ IsUnit.{u_3} (M := Localization.AtPrime q)
    (IsLocalization.mk' (R := T) (M := q.primeCompl) (Localization.AtPrime q) ((algebraMap R T : (a : R) → T) x : T)
      (1 : ↥q.primeCompl))

Tactic:
simpa [IsLocalization.AtPrime.isUnit_mk'_iff]

Premises used: IsLocalization.AtPrime.isUnit_mk'_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
⊢ IsUnit.{u_2} (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p)

Tactic:
have := this.1 (algebraMap _ _ x) (by
      suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff])
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this_1 : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
this :
  IsUnit.{u_2} (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p)
⊢ IsUnit.{u_2} (M := Localization.AtPrime p)
    (IsLocalization.mk' (R := S) (M := p.primeCompl) (Localization.AtPrime p) ((algebraMap R S : (a : R) → S) x : S)
      (1 : ↥p.primeCompl))

Tactic:
simpa [IsLocalization.mk'_one]

Premises used: IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this_1 : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
this :
  IsUnit.{u_2} (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p)
⊢ False

Tactic:
exact (IsLocalization.AtPrime.isUnit_mk'_iff (Localization.AtPrime p) p
      (algebraMap _ _ x) 1).mp (by simpa [IsLocalization.mk'_one]) hx

Premises used: Algebra.algebraMap, Localization.AtPrime, Iff.mp, IsLocalization.AtPrime.isUnit_mk'_iff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
      (Ideal.under R p))
    (Ideal.comap f.toRingHom
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
have H : (p.under R).map (algebraMap R _) ≤
      ((q.under R).map (algebraMap R _)).comap f.toRingHom := by
    rw [Ideal.map_le_iff_le_comap, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
      AlgHom.comp_algebraMap_of_tower]
    grw [← Ideal.le_comap_map]
    intro x hx
    by_contra hx'
    have : IsLocalHom f.toRingHom := .of_surjective _ hf
    have := this.1 (algebraMap _ _ x) (by
      suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff])
    exact (IsLocalization.AtPrime.isUnit_mk'_iff (Localization.AtPrime p) p
      (algebraMap _ _ x) 1).mp (by simpa [IsLocalization.mk'_one]) hx
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
H :
  LE.le (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
      (Ideal.under R p))
    (Ideal.comap f.toRingHom
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
⊢ QuasiFinite.{u_1, u_3} R
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
.of_surjective_algHom (S := Localization.AtPrime p ⧸
    (p.under R).map (algebraMap R (Localization.AtPrime p))) (Ideal.quotientMapₐ _ f H)
    (Ideal.quotientMap_surjective (H := H) hf)

Premises used: Algebra.QuasiFinite.of_surjective_algHom, Ideal.quotientMapₐ, Ideal.quotientMap_surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
H :
  LE.le (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
      (Ideal.under R p))
    (Ideal.comap f.toRingHom
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
⊢ QuasiFinite.{u_1, u_3} R
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))

Tactic:
exact .of_surjective_algHom (S := Localization.AtPrime p ⧸
    (p.under R).map (algebraMap R (Localization.AtPrime p))) (Ideal.quotientMapₐ _ f H)
    (Ideal.quotientMap_surjective (H := H) hf)
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 S
inst_5 : p.IsPrime
inst_6 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_7 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
⊢ Ideal.IsPrime (Ideal.comap f q)

Tactic:
subst hq
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing T
inst_5 : Algebra R T
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_8 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
inst : Ideal.IsPrime (Ideal.comap f q)
⊢ WeaklyQuasiFiniteAt R (Ideal.comap f q)

Tactic:
subst hq
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
q : Ideal T
inst_5 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
inst_6 : Ideal.IsPrime (Ideal.comap f q)
inst_7 : WeaklyQuasiFiniteAt R (Ideal.comap f q)
⊢ WeaklyQuasiFiniteAt R q

Tactic:
of_algHom_localization _ _ (Localization.localAlgHom _ _ f rfl) (hf _ _)

Premises used: Localization.localAlgHom, Algebra.WeaklyQuasiFiniteAt.of_algHom_localization, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
q : Ideal T
inst_5 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
inst_6 : Ideal.IsPrime (Ideal.comap f q)
inst_7 : WeaklyQuasiFiniteAt R (Ideal.comap f q)
⊢ WeaklyQuasiFiniteAt R q

Tactic:
exact of_algHom_localization _ _ (Localization.localAlgHom _ _ f rfl) (hf _ _)

Premises used: Localization.localAlgHom, Algebra.WeaklyQuasiFiniteAt.of_algHom_localization, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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_1 : Ideal R
q : Ideal S
inst_5 : q.IsPrime
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : T ≃ₐ[R] S
h :
  ∀ (x : S),
    x ∈ p ↔ Membership.mem (γ := Ideal S) (Ideal.comap (↑f.symm : S →ₐ[R] T) (Ideal.comap f.toRingEquiv.toRingHom p)) x
⊢ p = Ideal.comap (↑f.symm : S →ₐ[R] T) (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
ext