awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Free R S
inst_4 : Module.Finite R S
inst_5 : IsLocalRing R
x : S
let let₁ let₂ let₃ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
have let₄ : let ι := Free.ChooseBasisIndex R S;
let b : Basis ι R S := Free.chooseBasis R S;
Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) p)
  (Matrix.trace.{u_2, u_1} (n := ι)
    ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x)))
  (Matrix.trace.{u_2, u_1} (n := ι)
    (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)))
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex R S
  let b : Module.Basis ι R S := Module.Free.chooseBasis R S
  rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
  congr 1
  ext i j
  simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
    basisQuotient_apply, LinearMap.mul_apply', Matrix.map_apply, ← map_mul,
    basisQuotient_repr]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Free R S
inst_4 : Module.Finite R S
inst_5 : IsLocalRing R
x : S
let let₁ let₂ let₃ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
let₄ :
  let ι := Free.ChooseBasisIndex R S;
  let b : Basis ι R S := Free.chooseBasis R S;
  Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) p)
    (Matrix.trace.{u_2, u_1} (n := ι)
      ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x)))
    (Matrix.trace.{u_2, u_1} (n := ι)
      (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
have e_A : let ι := Free.ChooseBasisIndex R S;
let b : Basis ι R S := Free.chooseBasis R S;
Eq (α := Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) p))
  ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
    Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) p))
  (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p) :
    Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) (p : Ideal R)))
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex R S
  let b : Module.Basis ι R S := Module.Free.chooseBasis R S
  rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
  congr 1
  ext i j
  simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
    basisQuotient_apply, LinearMap.mul_apply', Matrix.map_apply, ← map_mul,
    basisQuotient_repr]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
⊢ IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
have h : Eq (α :=
  RingHom.{u_1, u_4} R
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (algebraMap R
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (@RingHom.comp.{u_1, u_3, u_4} _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _
    Semiring.toNonAssocSemiring _
    (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))))
Tactic: apply IsScalarTower.of_algebraMap_eq'
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
⊢ Eq (α :=
    RingHom.{u_1, u_4} R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (algebraMap R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp.{u_1, u_3, u_4} _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _
      Semiring.toNonAssocSemiring _
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))))
have h : Eq (α :=
  RingHom.{u_1, u_4} R
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (algebraMap R
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (@RingHom.comp _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) (algebraMap R Rₚ)))
Tactic: rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
      ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
h :
  Eq (α :=
    RingHom.{u_1, u_4} R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (algebraMap R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) (algebraMap R Rₚ)))
⊢ Eq (α :=
    RingHom.{u_1, u_4} R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (algebraMap R
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp.{u_1, u_3, u_4} _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _
      Semiring.toNonAssocSemiring _
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))))
have h₁ : Eq (α :=
  RingHom.{u_1, u_4} R
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (algebraMap Rₚ
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (algebraMap R Rₚ))
  (@RingHom.comp _ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) (algebraMap R Rₚ)))
Tactic: rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
      ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
⊢ Eq.{u_1 + 1} (α := R ⧸ p)
    ((Algebra.trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      R ⧸ p)
    (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
            RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
        ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          ((algebraMap S
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
              (a : S) → Sₚ ⧸ pSₚ)
            x)) :
      R ⧸ p)
have this : IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
Tactic: have : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) := by
    apply IsScalarTower.of_algebraMap_eq'
    rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
      ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
this :
  IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ Eq (α :=
    RingHom.{u_1, u_4} (R ⧸ p)
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (↑(equivQuotMaximalIdeal p Rₚ) : R ⧸ p →+* Rₚ ⧸ maximalIdeal Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ) : S ⧸ pS →+* Sₚ ⧸ pSₚ)
      (algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))))
have he : ∀ (x : R),
  Eq.{u_4 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
              (↑(equivQuotMaximalIdeal p Rₚ) : R ⧸ p →+* Rₚ ⧸ maximalIdeal Rₚ))
            (Ideal.Quotient.mk p) :
          (a : R) → Sₚ ⧸ pSₚ)
        x :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ) : S ⧸ pS →+* Sₚ ⧸ pSₚ)
                (algebraMap (R ⧸ p)
                  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))))
              (Ideal.Quotient.mk p) :
            RingHom.{u_1, u_4} R
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : R) → Sₚ ⧸ pSₚ)
        x :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x_1 : S
this :
  IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
x : R
⊢ Eq.{u_4 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ pSₚ)
        (((algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
              RingHom.{u_1, u_3} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R) → Rₚ ⧸ maximalIdeal Rₚ)
          x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            RingHom.{u_2, u_4} S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S) → Sₚ ⧸ pSₚ)
        ((algebraMap R S : (a : R) → S) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
have he : Eq.{u_4 + 1} (α :=
  HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
  ((algebraMap R
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
        (a : R) → Sₚ ⧸ pSₚ)
      x :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
  (((algebraMap S
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          RingHom.{u_2, u_4} S
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
        (a : S) → Sₚ ⧸ pSₚ)
      ((algebraMap R S : (a : R) → S) x) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (RingHom.comp (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
have rw : Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
  (RingHom.comp (IsLocalization.map (T := algebraMapSubmonoid S p.primeCompl) Sₚ (algebraMap R S) sorry) (algebraMap R Rₚ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
rw :
  Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
    (RingHom.comp (IsLocalization.map (T := algebraMapSubmonoid S p.primeCompl) Sₚ (algebraMap R S) ⋯)
      (algebraMap R Rₚ))
⊢ Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (RingHom.comp (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
have rw₁ : Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
rw :
  Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
    (RingHom.comp (IsLocalization.map (T := algebraMapSubmonoid S p.primeCompl) Sₚ (algebraMap R S) ⋯)
      (algebraMap R Rₚ))
rw₁ :
  Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S))
⊢ Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (RingHom.comp (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
have rw₂ : Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (algebraMap R Sₚ)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ Eq.{u_1 + 1} (α := R ⧸ p)
    ((trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      R ⧸ p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x) : R ⧸ p)
have this₁ : IsScalarTower R Rₚ Sₚ
Tactic: haveI : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])