awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
⊢ Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)

Tactic:
have : (Ideal.map φ.toRingHom q).IsPrime :=
    Ideal.map_isPrime_of_surjective ‹_› <| hφ₂.trans_le 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ.toRingHom : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))

Tactic:
hφ₁
-- 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ.toRingHom : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))

Tactic:
exact hφ₁
-- 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ QuasiFiniteAt (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q)) (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)

Tactic:
have := QuasiFiniteAt.baseChange (R := R) (S := _) (A := A ⧸ q.under A)
    (p.map (Ideal.Quotient.mk ((p.under R).map (algebraMap R S)))) (q.map φ.toRingHom) (by
    apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective
    rwa [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, sup_eq_left.mpr Ideal.map_comap_le,
      ← hφ₃, ← Ideal.comap_comap, Ideal.comap_map_of_surjective _ (by exact hφ₁),
      ← RingHom.ker_eq_comap_bot, hφ₂, sup_eq_left.mpr 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this_1 :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
this :
  QuasiFiniteAt (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q)) (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ QuasiFiniteAt A (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)

Tactic:
have : QuasiFiniteAt A (q.map φ.toRingHom) := .trans _ (A ⧸ q.under A) _
-- 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this_1 :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
this_2 :
  QuasiFiniteAt (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q)) (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
this :
  QuasiFiniteAt A (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ)
    (Ideal.map (R := A ⊗[R] S) (F := A ⊗[R] S →+* A ⊗[R] S) (↑AlgEquiv.refl : A ⊗[R] S →+* A ⊗[R] S)
      (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q)))

Tactic:
simpa
-- 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this_1 :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
this_2 :
  QuasiFiniteAt (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q)) (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
this :
  QuasiFiniteAt A (S :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
e : HasQuotient.Quotient (A ⊗[R] S) (B := Ideal (A ⊗[R] S))
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q)) ≃ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (AlgHom.toRingHom ?m.733).SurjectiveOnStalks

Tactic:
e
-- 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
⊢ QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)

Tactic:
have : Algebra.QuasiFiniteAt S (q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R T)))) :=
    .of_restrictScalars R _ _
-- 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
this :
  QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)
⊢ LE.le.{u_3} (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))

Tactic:
simpa [Ideal.under, IsScalarTower.algebraMap_eq R S T, ← Ideal.map_map,
      ← Ideal.comap_comap, -Ideal.under_under] using Ideal.map_mono Ideal.map_comap_le

Premises used: Ideal.under_under, Ideal.map_map, IsScalarTower.algebraMap_eq, Ideal.map_mono, Ideal.map_comap_le, Ideal.under, 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
this :
  QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)
⊢ LE.le.{u_3} (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))

Tactic:
have H : (q.under R).map (algebraMap R T) ≤ (q.under S).map (algebraMap S T) := by
    simpa [Ideal.under, IsScalarTower.algebraMap_eq R S T, ← Ideal.map_map,
      ← Ideal.comap_comap, -Ideal.under_under] using Ideal.map_mono Ideal.map_comap_le
-- 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
this :
  QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)
H :
  LE.le.{u_3} (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))
⊢ LE.le (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.comap (F := T →ₐ[S] T) (AlgHom.id S T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))

Tactic:
H

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.preimage
-- 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
this :
  QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)
H :
  LE.le.{u_3} (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))
⊢ LE.le (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.comap (F := T →ₐ[S] T) (AlgHom.id S T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))

Tactic:
exact H