awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this_1 : DecidableEq ι
this : DecidableEq κ
val : Fintype ι
val_1 : Fintype κ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i : ι,
      Matrix.diag
        ((leftMulMatrix b : (a : S) → Matrix ι ι R)
          (∑ i : κ, Matrix.diag ((leftMulMatrix c : (a : T) → Matrix κ κ S) x) i))
        i)
    (∑ x_1 : ι, ∑ y : κ, Matrix.diag ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (ι × κ) (ι × κ) R) x) (x_1, y))

Tactic:
Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this_1 : DecidableEq ι
this : DecidableEq κ
val : Fintype ι
val_1 : Fintype κ
intro :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      Eq.{u_1 + 1} (α := R)
        (Matrix.diag
          ((leftMulMatrix b : (a : S) → Matrix ι ι R)
            (∑ i : κ, Matrix.diag ((leftMulMatrix c : (a : T) → Matrix κ κ S) x) i))
          i)
        (∑ y : κ, Matrix.diag ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (ι × κ) (ι × κ) R) x) (i, y))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i : ι,
      Matrix.diag
        ((leftMulMatrix b : (a : S) → Matrix ι ι R)
          (∑ i : κ, Matrix.diag ((leftMulMatrix c : (a : T) → Matrix κ κ S) x) i))
        i)
    (∑ x_1 : ι, ∑ y : κ, Matrix.diag ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (ι × κ) (ι × κ) R) x) (x_1, y))

Tactic:
refine Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this_1 : DecidableEq ι
this : DecidableEq κ
val : Fintype ι
val_1 : Fintype κ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Eq.{u_1 + 1} (α := R)
    (Matrix.diag
      ((leftMulMatrix b : (a : S) → Matrix ι ι R)
        (∑ i : κ, Matrix.diag ((leftMulMatrix c : (a : T) → Matrix κ κ S) x) i))
      i)
    (∑ y : κ, Matrix.diag ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (ι × κ) (ι × κ) R) x) (i, y))

Tactic:
simp only [map_sum, smulTower_leftMulMatrix, Finset.sum_apply, Matrix.diag,
    Finset.sum_apply i (Finset.univ : Finset κ) fun y => leftMulMatrix b (leftMulMatrix c x y y)]

Premises used: Matrix.diag, Finset.univ, Finset.sum_apply, map_sum, Algebra.smulTower_leftMulMatrix, Algebra.leftMulMatrix, DFunLike.coe
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
h :
  ∀ (x : T),
    Eq.{u_1 + 1} (α := R)
      ((trace R S ∘ₗ
              (↑R :
                  {S : Type u_2} →
                    {M : Type u_3} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (trace S T) :
            (a : T) → R)
          x :
        R)
      ((trace R T : (a : T) → R) x : R)
⊢ Eq (α := T →ₗ[R] R)
    (trace R S ∘ₗ
      (↑R :
          {S : Type u_2} →
            {M : Type u_3} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (trace S T))
    (trace R T)

Tactic:
ext
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
h :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (((↑R :
                  {S : Type u_2} →
                    {M : Type u_3} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (trace S T) :
              (a : T) → S)
            x :
          S) :
      R)
    ((trace R T : (a : T) → R) x : R)
h₁ :
  Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) ((trace S T : (a : T) → S) x : S) : R)
    ((trace R T : (a : T) → R) x : R)
h₂ h₃ : Eq.{u_1 + 1} (α := R) ((trace R T : (a : T) → R) x : R) ((trace R T : (a : T) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R S ∘ₗ
            (↑R :
                {S : Type u_2} →
                  {M : Type u_3} →
                    {M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_9 : Semiring S] →
                          [inst_10 : AddCommMonoid M] →
                            [inst_11 : AddCommMonoid M₂] →
                              [inst_12 : Module R M] →
                                [inst_13 : Module R M₂] →
                                  [inst_14 : Module S M] →
                                    [inst_15 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (trace S T) :
          (a : T) → R)
        x :
      R)
    ((trace R T : (a : T) → R) x : R)

Tactic:
rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]

Premises used: LinearMap.restrictScalars_apply, LinearMap.comp_apply, Algebra.trace_trace_of_basis
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Free R S
inst_8 : Module.Finite R S
inst_9 : Free S T
inst_10 : Module.Finite S T
x : T
⊢ Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) ((trace S T : (a : T) → S) x : S) : R)
    ((trace R T : (a : T) → R) x : R)

Tactic:
trace_trace_of_basis (Module.Free.chooseBasis R S) (Module.Free.chooseBasis S T) x

Premises used: Algebra.trace_trace_of_basis, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Free R S
inst_8 : Module.Finite R S
inst_9 : Free S T
inst_10 : Module.Finite S T
⊢ Eq (α := T →ₗ[R] R)
    (trace R S ∘ₗ
      (↑R :
          {S : Type u_2} →
            {M : Type u_3} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (trace S T))
    (trace R T)

Tactic:
LinearMap.ext trace_trace

Premises used: LinearMap.ext, Algebra.trace_trace
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Free R S
inst_6 : Free R T
inst_7 : Module.Finite R S
inst_8 : Module.Finite R T
x : S × T
f : S × T →ₗ[R] Prod.{u_2, u_3} (End R S) (End R T) :=
  prodMap (AlgHom.toLinearMap (lmul R S)) (AlgHom.toLinearMap (lmul R T))
⊢ AlgHom.toLinearMap (lmul R (S × T)) = prodMapLinear R S T S T R ∘ₗ f

Tactic:
have : (lmul R (S × T)).toLinearMap = (prodMapLinear R S T S T R).comp f :=
    LinearMap.ext₂ Prod.mul_def
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Free R S
inst_6 : Free R T
inst_7 : Module.Finite R S
inst_8 : Module.Finite R T
x : S × T
f : S × T →ₗ[R] Prod.{u_2, u_3} (End R S) (End R T) :=
  prodMap (AlgHom.toLinearMap (lmul R S)) (AlgHom.toLinearMap (lmul R T))
this : AlgHom.toLinearMap (lmul R (S × T)) = prodMapLinear R S T S T R ∘ₗ f
simp_rw :
  (LinearMap.trace R (S × T) ∘ₗ prodMapLinear R S T S T R ∘ₗ f : (a : S × T) → R) x =
    HAdd.hAdd (α := R) (β := R) ((LinearMap.trace R S ∘ₗ AlgHom.toLinearMap (lmul R S) : (a : S) → R) x.1 : R)
      ((LinearMap.trace R T ∘ₗ AlgHom.toLinearMap (lmul R T) : (a : T) → R) x.2 : R)
⊢ (trace R (S × T) : (a : S × T) → R) x =
    HAdd.hAdd (α := R) (β := R) ((trace R S : (a : S) → R) x.1 : R) ((trace R T : (a : T) → R) x.2 : R)

Tactic:
simp_rw [trace, this]

Premises used: Algebra.trace
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Free R S
inst_6 : Free R T
inst_7 : Module.Finite R S
inst_8 : Module.Finite R T
x : S × T
f : S × T →ₗ[R] Prod.{u_2, u_3} (End R S) (End R T) :=
  prodMap (AlgHom.toLinearMap (lmul R S)) (AlgHom.toLinearMap (lmul R T))
this : AlgHom.toLinearMap (lmul R (S × T)) = prodMapLinear R S T S T R ∘ₗ f
⊢ (LinearMap.trace R (S × T) ∘ₗ prodMapLinear R S T S T R ∘ₗ f : (a : S × T) → R) x =
    HAdd.hAdd (α := R) (β := R) ((LinearMap.trace R S ∘ₗ AlgHom.toLinearMap (lmul R S) : (a : S) → R) x.1 : R)
      ((LinearMap.trace R T ∘ₗ AlgHom.toLinearMap (lmul R T) : (a : T) → R) x.2 : R)

Tactic:
trace_prodMap' _ _

Premises used: LinearMap.prod, LinearMap.trace_prodMap', LinearMap.prodMap
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Free R S
inst_6 : Free R T
inst_7 : Module.Finite R S
inst_8 : Module.Finite R T
x : S × T
f : S × T →ₗ[R] Prod.{u_2, u_3} (End R S) (End R T) :=
  prodMap (AlgHom.toLinearMap (lmul R S)) (AlgHom.toLinearMap (lmul R T))
this : AlgHom.toLinearMap (lmul R (S × T)) = prodMapLinear R S T S T R ∘ₗ f
⊢ (LinearMap.trace R (S × T) ∘ₗ prodMapLinear R S T S T R ∘ₗ f : (a : S × T) → R) x =
    HAdd.hAdd (α := R) (β := R) ((LinearMap.trace R S ∘ₗ AlgHom.toLinearMap (lmul R S) : (a : S) → R) x.1 : R)
      ((LinearMap.trace R T ∘ₗ AlgHom.toLinearMap (lmul R T) : (a : T) → R) x.2 : R)

Tactic:
exact trace_prodMap' _ _

Premises used: LinearMap.trace_prodMap'
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Free R S
inst_6 : Free R T
inst_7 : Module.Finite R S
inst_8 : Module.Finite R T
p : S × T
rw :
  (trace R (S × T) : (a : S × T) → R) p =
    HAdd.hAdd (α := R) (β := R) ((trace R S : (a : S) → R) p.1 : R) ((trace R T : (a : T) → R) p.2 : R)
rw₁ rw₂ :
  HAdd.hAdd (α := R) (β := R) ((trace R S : (a : S) → R) p.1 : R) ((trace R T : (a : T) → R) p.2 : R) =
    HAdd.hAdd (α := R) (β := R) ((trace R S : (a : S) → R) p.1 : R) ((trace R T : (a : T) → R) p.2 : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R (S × T) : (a : S × T) → R) p : R)
    ((coprod (trace R S) (trace R T) : (a : S × T) → R) p : R)

Tactic:
rw [coprod_apply, trace_prod_apply]

Premises used: LinearMap.coprod_apply, Algebra.trace_prod_apply
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y : S
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R S : (a : S) → S →ₗ[R] R) x : S →ₗ[R] R) : (a : S) → R) y : R)
    ((trace R S : (a : S) → R) (x * y) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ BilinForm.IsSymm (traceForm R S)

Tactic:
⟨fun _ _ => congr_arg (trace R S) (mul_comm _ _)⟩

Premises used: LinearMap.BilinForm.IsSymm.mk, congr_arg, mul_comm, Algebra.trace, DFunLike.coe
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
i j : ι
rw :
  Eq.{u_1 + 1} (α := R)
    ((((traceForm R S : (a : S) → S →ₗ[R] R) ((b : (a : ι) → S) i) : S →ₗ[R] R) : (a : S) → R)
        ((b : (a : ι) → S) j : S) :
      R)
    ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) : R)
    ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) : R)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.BilinForm.toMatrix b : (a : BilinForm R S) → Matrix ι ι R) (traceForm R S) i j : R)
    ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) : R)

Tactic:
rw [LinearMap.BilinForm.toMatrix_apply, traceForm_apply]

Premises used: Algebra.traceForm_apply, LinearMap.BilinForm.toMatrix_apply
-- Module: Mathlib.RingTheory.Trace.Quotient
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
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
rw :
  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))

Tactic:
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]

Premises used: AddMonoidHom.map_trace, Algebra.trace_eq_matrix_trace, IsLocalRing.basisQuotient
-- Module: Mathlib.RingTheory.Trace.Quotient
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
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
e_A :
  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)))
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.Trace.Quotient
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
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
e_A :
  ∀ (i j : ι),
    Eq.{u_1 + 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) i j :
        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) i
          j :
        HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
⊢ 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:
ext i j
-- Module: Mathlib.RingTheory.Trace.Quotient
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
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
i j : ι
⊢ Eq.{u_1 + 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) i j :
      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) i j :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))

Tactic:
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
    basisQuotient_apply, LinearMap.mul_apply', Matrix.map_apply, ← map_mul,
    basisQuotient_repr]

Premises used: LinearMap.mul_apply', IsLocalRing.basisQuotient_repr, Matrix.map_apply, map_mul, IsLocalRing.basisQuotient_apply, Algebra.coe_lmul_eq_mul, Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Trace.Quotient
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.{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ₚ))))
⊢ 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:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.RingTheory.Trace.Quotient
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ₚ)))

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ₚ]