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 Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
h₂ : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R Q)
inst_5 : WeaklyQuasiFiniteAt R Q
this_1 :
  Ideal.IsPrime (α :=
    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))) P)
this_2 :
  Eq (α := 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))) P)
    (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)
this : P ⊔ Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q) = Q
⊢ P = Q

Tactic:
simpa [Ideal.map_comap_le, ← h₂] using this

Premises used: 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)))
⊢ 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)))

Tactic:
have hφ₁ : Function.Surjective φ :=
    Algebra.TensorProduct.map_surjective _ _
      Ideal.Quotient.mk_surjective Ideal.Quotient.mk_surjective
-- 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)))
⊢ Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))

Tactic:
(Algebra.TensorProduct.map_ker _ _
      Ideal.Quotient.mk_surjective Ideal.Quotient.mk_surjective).trans ?_

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, Algebra.TensorProduct.map_ker, Ideal.comap, Eq.trans, RingHom.ker
-- 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)))
refine :
  Eq (α := Ideal (A ⊗[R] S))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] S) TensorProduct.includeLeft
        (RingHom.ker (F := A →ₐ[A] HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
          (Ideal.Quotient.mkₐ A (Ideal.under A q))) ⊔
      Ideal.map (F := S →ₐ[R] A ⊗[R] S) TensorProduct.includeRight
        (RingHom.ker (F :=
          S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
          (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))))
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
⊢ Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))

Tactic:
refine (Algebra.TensorProduct.map_ker _ _
      Ideal.Quotient.mk_surjective Ideal.Quotient.mk_surjective).trans ?_

Premises used: Algebra.TensorProduct.map_ker, Eq.trans
-- 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)))
simp :
  Eq (α := Ideal (A ⊗[R] S))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
        (Ideal.comap (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) q) ⊔
      Ideal.map (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S))
        (Ideal.comap (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S)) q))
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S))
      (Ideal.comap (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) q))
⊢ Eq (α := Ideal (A ⊗[R] S))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
        (RingHom.ker (F := A →+* HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
          (↑(Ideal.Quotient.mkₐ A (Ideal.under A q)) : A →+* A ⧸ Ideal.under A q)) ⊔
      Ideal.map (F := S →+* A ⊗[R] S) (↑TensorProduct.includeRight : S →+* A ⊗[R] S)
        (RingHom.ker (F :=
          S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
          (↑(Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :
            S →+* S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p))))
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))

Tactic:
simp only [Ideal.under, Ideal.Quotient.mkₐ_ker, hq, AlgHom.toRingHom_eq_coe, Ideal.comap_comap,
      AlgHom.comp_algebraMap_of_tower, Ideal.map_map]

Premises used: AlgHom.comp_algebraMap_of_tower, Ideal.Quotient.mkₐ_ker, Ideal.map_map, AlgHom.toRingHom_eq_coe, Ideal.under, Ideal.comap_comap
-- 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)))
⊢ Eq (α := Ideal (A ⊗[R] S))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
        (Ideal.comap (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) q) ⊔
      Ideal.map (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S))
        (Ideal.comap (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S)) q))
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S))
      (Ideal.comap (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) q))

Tactic:
sup_eq_left.mpr ?_

Premises used: Iff.mpr, sup_eq_left, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- 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)))
simp :
  LE.le (α := Ideal (A ⊗[R] S))
    (Ideal.map (R := A) (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.map (F := R →+* A) (algebraMap R A)
        (Ideal.comap (F := R →+* A) (algebraMap R A)
          (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q))))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.comap (F := A →+* A) (algebraMap A A)
        (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q)))
⊢ LE.le (α := Ideal (A ⊗[R] S))
    (Ideal.map (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S))
      (Ideal.comap (F := R →+* A ⊗[R] S) (algebraMap R (A ⊗[R] S)) q))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.comap (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) q))

Tactic:
simp only [← TensorProduct.includeLeft.comp_algebraMap, ← Ideal.map_map, ← Ideal.comap_comap]

Premises used: AlgHom.comp_algebraMap, Algebra.TensorProduct.includeLeft, Ideal.map_map, Ideal.comap_comap
-- 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)))
⊢ LE.le (α := Ideal (A ⊗[R] S))
    (Ideal.map (R := A) (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.map (F := R →+* A) (algebraMap R A)
        (Ideal.comap (F := R →+* A) (algebraMap R A)
          (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q))))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.comap (F := A →+* A) (algebraMap A A)
        (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q)))

Tactic:
Ideal.map_mono Ideal.map_comap_le

Premises used: Set.Mem, setOf, Ideal.map_mono, 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)))
⊢ LE.le (α := Ideal (A ⊗[R] S))
    (Ideal.map (R := A) (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.map (F := R →+* A) (algebraMap R A)
        (Ideal.comap (F := R →+* A) (algebraMap R A)
          (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q))))
    (Ideal.map (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S)
      (Ideal.comap (F := A →+* A) (algebraMap A A)
        (Ideal.comap (F := A →+* A ⊗[R] S) (↑TensorProduct.includeLeft : A →+* A ⊗[R] S) q)))

Tactic:
exact Ideal.map_mono Ideal.map_comap_le

Premises used: Ideal.map_mono, 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)))
⊢ Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))

Tactic:
have hφ₂ : RingHom.ker φ.toRingHom = (q.under A).map (algebraMap _ _) := by
    refine (Algebra.TensorProduct.map_ker _ _
      Ideal.Quotient.mk_surjective Ideal.Quotient.mk_surjective).trans ?_
    rw [← RingHom.ker_coe_toRingHom, ← RingHom.ker_coe_toRingHom (F := AlgHom _ _ _),
      ← Ideal.map_coe, ← Ideal.map_coe (F := AlgHom _ _ _)]
    simp only [Ideal.under, Ideal.Quotient.mkₐ_ker, hq, AlgHom.toRingHom_eq_coe, Ideal.comap_comap,
      AlgHom.comp_algebraMap_of_tower, Ideal.map_map]
    refine sup_eq_left.mpr ?_
    simp only [← TensorProduct.includeLeft.comp_algebraMap, ← Ideal.map_map, ← Ideal.comap_comap]
    exact Ideal.map_mono 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))
⊢ φ.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)))

Tactic:
have hφ₃ : φ.toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.toRingHom.comp (Ideal.Quotient.mk _) := rfl