awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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)))
⊢ QuasiFiniteAt A (S :=
    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)))
    (Ideal.map (F :=
      A ⊗[R] S →+*
        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)))
      (Ideal.Quotient.mk (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)
have 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)
Tactic: have : (Ideal.map φ.toRingHom q).IsPrime :=
    Ideal.map_isPrime_of_surjective ‹_› <| hφ₂.trans_le Ideal.map_comap_le
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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
⊢ WeaklyQuasiFiniteAt S q
have 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)
Tactic: have : Algebra.QuasiFiniteAt S (q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R T)))) :=
    .of_restrictScalars R _ _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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)
⊢ WeaklyQuasiFiniteAt S q
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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))
⊢ 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)
have 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))
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)) _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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))
⊢ 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))
have a : Eq (α := Ideal T)
  (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.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 :=
    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 :=
      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)))
Tactic: apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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)
have 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))) ⊥
Tactic: refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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
⊢ WeaklyQuasiFiniteAt R q
have 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)))
Tactic: rw [Algebra.weaklyQuasiFiniteAt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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
⊢ 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))
have 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)
Tactic: rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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
⊢ 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))
have 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))
Tactic: obtain ⟨r, hrp, s, H⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ y
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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.{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))
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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
⊢ 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))
have 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))
Tactic: suffices IsUnit (φ₂ (1 ⊗ₜ s)) by
        rw [← H, map_smul, Algebra.smul_def, IsUnit.mul_iff] at this
        exact this.2
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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.{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))
have 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) : 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)))