awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)
pos : Fintype.card.{u_2} ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))) • x = finrank R S • x
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
have pos₁ : Fintype.card.{u_2} ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))) • x =
  Fintype.card.{u_2} ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))) • x
Tactic: rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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
⊢ 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)
have haveI : ∀ (this : DecidableEq ι),
  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: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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 : DecidableEq ι
⊢ 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)
have haveI : ∀ (this : DecidableEq κ),
  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: haveI := Classical.decEq κ
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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 κ
⊢ 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)
have intro : ∀ (val : Fintype ι),
  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: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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 ι
⊢ 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)
have intro : ∀ (val : Fintype κ),
  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: cases nonempty_fintype κ
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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) ((trace R S : (a : S) → R) ((trace S T : (a : T) → S) x : S) : R)
    ((trace R T : (a : T) → R) x : R)
have intro : 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: rw [trace_eq_matrix_trace (b.smulTower c), trace_eq_matrix_trace b, trace_eq_matrix_trace c,
    Matrix.trace, Matrix.trace, Matrix.trace, ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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))
have 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))
Tactic: refine Finset.sum_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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)
⊢ 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)
have h₂ : Eq.{u_1 + 1} (α := R) ((trace R 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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (hypothesis)
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))
⊢ (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)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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
⊢ (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)
have 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)
Tactic: simp_rw [trace, this]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [coprod_apply, trace_prod_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [coprod_apply, trace_prod_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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 : ι
⊢ 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)
have 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)
Tactic: rw [LinearMap.BilinForm.toMatrix_apply, traceForm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [LinearMap.BilinForm.toMatrix_apply, traceForm_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
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
⊢ 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 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)))
Tactic: rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
-- 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
ι : Type u_2 := Free.ChooseBasisIndex R S
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)))
have 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)))
Tactic: congr 1
-- 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
ι : Type u_2 := Free.ChooseBasisIndex R S
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)))
have 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))
Tactic: ext i j