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
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 →+* T) (↑(AlgHom.id S T) : T →+* 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 →+* T) (↑(AlgHom.id S T) : T →+* T)
      (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))

Tactic:
exact H
-- 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))
refine :
  Eq (α := Ideal (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)
    (Ideal.comap (F :=
      HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)) →+*
        HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
      (AlgHom.toRingHom
        (Ideal.quotientMapₐ (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H))
      (Ideal.map (F :=
        T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q))
⊢ QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
      (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q)

Tactic:
refine .of_surjectiveOnStalks (q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R T))))
    (Ideal.quotientMapₐ _ (.id _ _) (by exact H)) (RingHom.surjectiveOnStalks_of_surjective
      (Ideal.quotientMap_surjective (H := by exact H) Function.surjective_id)) _ ?_
-- 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))
⊢ q ⊔
      Ideal.comap (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))) ⊥ =
    Ideal.comap (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
      (@RingHom.comp _
        (HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) _ _
        Semiring.toNonAssocSemiring _
        (AlgHom.toRingHom
          (Ideal.quotientMapₐ (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H))
        (Ideal.Quotient.mk (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 := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q)

Tactic:
.trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm

Premises used: Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, Eq.symm, Eq.trans
-- 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))
a :
  q ⊔
      Ideal.comap (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 ⊔
      Ideal.comap (F :=
        T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) ⊥
⊢ q ⊔
      Ideal.comap (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))) ⊥ =
    Ideal.comap (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
      (@RingHom.comp _
        (HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) _ _
        Semiring.toNonAssocSemiring _
        (AlgHom.toRingHom
          (Ideal.quotientMapₐ (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H))
        (Ideal.Quotient.mk (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 := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q)

Tactic:
refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
-- 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))
⊢ q ⊔
      Ideal.comap (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 ⊔
      Ideal.comap (F :=
        T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S 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
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) 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 [Algebra.weaklyQuasiFiniteAt_iff]

Premises used: Algebra.weaklyQuasiFiniteAt_iff
-- 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
rw :
  p ≤
    Ideal.comap (F := R →+* Sq)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) : Localization.AtPrime p →+* Sq)
        (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
⊢ LE.le (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p))
    (Ideal.comap (F := Localization.AtPrime p →ₐ[R] Sq) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq)
      (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]

Premises used: Ideal.map_le_iff_le_comap, IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.comap_coe, 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
⊢ p ≤
    Ideal.comap (F := R →+* Sq)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) : Localization.AtPrime p →+* Sq)
        (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)

Tactic:
simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map

Premises used: Ideal.le_comap_map, IsScalarTower.algebraMap_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
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
obtain :
  ∀ (r : R) (hrp : r ∉ p) (s : S) (H : r • y = 1 ⊗ₜ[R] s),
    IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (↑(Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) y hy) : p.Fiber S) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        (↑(Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) y hy) : p.Fiber S) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
obtain ⟨r, hrp, s, H⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ y

Premises used: Ideal.Fiber.exists_smul_eq_one_tmul
-- 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
this :
  IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p) (1 ⊗ₜ[R] s) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ IsUnit
    (HSMul.hSMul (β := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) r
      ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p) y :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))

Tactic:
rw [← H, map_smul, Algebra.smul_def, IsUnit.mul_iff] at this

Premises used: IsUnit.mul_iff, Algebra.smul_def, map_smul
-- 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
suffices :
  IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p) (1 ⊗ₜ[R] s) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        (↑(Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) y hy) : p.Fiber S) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
suffices IsUnit (φ₂ (1 ⊗ₜ s)) by
        rw [← H, map_smul, Algebra.smul_def, IsUnit.mul_iff] at this
        exact this.2
-- 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
this : s ∉ q
⊢ IsUnit (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((algebraMap Sq (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :
          (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        ((algebraMap S Sq : (a : S) → Sq) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s this) : S)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
have := (IsLocalization.map_units (M := q.primeCompl) Sq ⟨_, this⟩).map
          (algebraMap _ (Sq ⧸ p.map (algebraMap R Sq)))
-- 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 R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
this_2 : s ∉ q
this :
  IsUnit (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((algebraMap Sq (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :
          (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        ((algebraMap S Sq : (a : S) → Sq) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s this_2) : S)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p) (1 ⊗ₜ[R] s) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
simpa [φ₂, ← IsScalarTower.algebraMap_apply] using this

Premises used: IsScalarTower.algebraMap_apply