awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (1 ⊗ₜ[R] s) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
have suffices : s ∉ q
Tactic: suffices s ∉ q by
        have := (IsLocalization.map_units (M := q.primeCompl) Sq ⟨_, this⟩).map
          (algebraMap _ (Sq ⧸ p.map (algebraMap R Sq)))
        simpa [φ₂, ← IsScalarTower.algebraMap_apply] using 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
⊢ s ∉ q
have suffices : HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q
Tactic: suffices algebraMap _ _ r * y ∉ Q by simpa [← hQ, ← H, Algebra.smul_def]
-- 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
⊢ HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q
have refine : Membership.mem (α := p.Fiber S) Q.primeCompl ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S)
Tactic: refine Q.primeCompl.mul_mem ?_ hy
-- 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)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
x : Sq
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          x :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
have obtain : ∀ (x s : S) (hs : s ∈ q.primeCompl),
  ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
Cleared hypotheses: x
-- 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)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
have refine_1 : 1 ⊗ₜ[R] s ∈ Q.primeCompl
Tactic: refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
-- 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)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
refine_1 : 1 ⊗ₜ[R] s ∈ Q.primeCompl
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
have refine_2 : Eq (α := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
  ((φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
      (IsLocalization.mk' (M := Q.primeCompl) (Localization.AtPrime (R := p.Fiber S) Q) (1 ⊗ₜ[R] x)
        (Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) (1 ⊗ₜ[R] s) sorry)) :
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) : (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
      (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
Tactic: refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
-- 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 : 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)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
⊢ 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)))
have this₁ : Function.Surjective (α := Localization.AtPrime (R := p.Fiber S) Q) (β :=
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
  (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
Tactic: have : Function.Surjective φ₃ := by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
    refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
    · simpa [← hQ] using hs
    · simp [φ₃, IsLocalization.lift_mk'_spec, φ₂, IsScalarTower.algebraMap_apply S Sq (Sq ⧸ _),
        -Ideal.Quotient.mk_algebraMap, ← map_mul]
-- 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)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
this :
  Function.Surjective (α := Localization.AtPrime (R := p.Fiber S) Q) (β :=
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
⊢ 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)))
have inst : QuasiFiniteAt R (S := p.Fiber S) Q
Tactic: have inst : QuasiFiniteAt R Q := .trans _ p.ResidueField _
-- Lean 4 proof step from Mathlib.RingTheory.QuotSMulTop (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ (map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ =
    (HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := QuotSMulTop r M')
    (((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
            (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ :
          (a : M) → QuotSMulTop r M')
        x :
      QuotSMulTop r M')
    (((HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f : (a : M) → QuotSMulTop r M') x : QuotSMulTop r M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuotSMulTop (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
H₁ :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M' ⧸ HSMul.hSMul (β := Submodule R M') r ⊤)
    (comp (β := M') (⇑(HSMul.hSMul (β := Submodule R M') r ⊤).mkQ : (a : M') → M' ⧸ r • ⊤) (⇑f : (a : M) → M'))
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (comp (β := QuotSMulTop r M)
      (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
            LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
        (a : QuotSMulTop r M) → QuotSMulTop r M')
      (⇑(HSMul.hSMul (β := Submodule R M) r ⊤).mkQ : (a : M) → M ⧸ r • ⊤))
have rwa : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
  (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
        (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ) :
    (a : M) → QuotSMulTop r M')
Tactic: rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.QuotSMulTop (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
H₁ :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M' ⧸ HSMul.hSMul (β := Submodule R M') r ⊤)
    (comp (β := M') (⇑(HSMul.hSMul (β := Submodule R M') r ⊤).mkQ : (a : M') → M' ⧸ r • ⊤) (⇑f : (a : M) → M'))
rwa :
  Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f ∘ₗ
          (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ) :
      (a : M) → QuotSMulTop r M')
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
    (comp (β := QuotSMulTop r M)
      (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f :
            LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
        (a : QuotSMulTop r M) → QuotSMulTop r M')
      (⇑(HSMul.hSMul (β := Submodule R M) r ⊤).mkQ : (a : M) → M ⧸ r • ⊤))
have rwa₁ : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := QuotSMulTop r M')
  (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mkQ ∘ₗ f) : (a : M) → QuotSMulTop r M')
Tactic: rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.QuotSMulTop (goal)
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_2, u_1} R (QuotSMulTop x M)) x
have refine : ∀ (m : QuotSMulTop x M), x • m = 0
Tactic: refine Module.mem_annihilator.mpr (fun m ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.QuotSMulTop (goal)
Goal:
R : Type u_2
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
m : QuotSMulTop x M
⊢ x • m = 0
have rcases : ∀ (m' : M) (hm' : Submodule.Quotient.mk m' = m), x • m = 0
Tactic: rcases Submodule.Quotient.mk_surjective _ m with ⟨m', hm'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ (normalizedFactors a).toFinset = (normalizedFactors b).toFinset
have rw : (normalizedFactors b).toFinset = (normalizedFactors b).toFinset
Tactic: rw [h.normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ (↑(primeFactors a) : Set M).Pairwise IsRelPrime
have inl : (↑(primeFactors 0) : Set M).Pairwise IsRelPrime
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inl : (↑(primeFactors 0) : Set M).Pairwise IsRelPrime
⊢ (↑(primeFactors a) : Set M).Pairwise IsRelPrime
have inr : ∀ (ha₀ : a ≠ 0), (↑(primeFactors a) : Set M).Pairwise IsRelPrime
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
hx : x ∈ (↑(primeFactors a) : Set M)
y : M
hy : y ∈ (↑(primeFactors a) : Set M)
hxy : x ≠ y
⊢ IsRelPrime x y
have hx₁ : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
Tactic: simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
hx : x ∈ (↑(primeFactors a) : Set M)
y : M
hy : y ∈ (↑(primeFactors a) : Set M)
hxy : x ≠ y
hx₁ : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
⊢ IsRelPrime x y
have hy₁ : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
Tactic: simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
⊢ IsRelPrime x y
have inr : ¬x ∣ y
Tactic: rw [hx.1.isRelPrime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
⊢ ¬x ∣ y
have inr : ∀ (hxy : x ∣ y), x = y
Tactic: contrapose hxy
Cleared hypotheses: hxy