awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
a :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ σ : L →ₐ[K] AlgebraicClosure K,
      (σ : (a : L) → AlgebraicClosure K)
        (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
          pb.gen ^ (↑j : ℕ)))
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
⊢ Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        ((Algebra.trace K L : (a : L) → K)
          (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
            pb.gen ^ (↑j : ℕ))) :
      AlgebraicClosure K)
    (if j = i then 1 else 0 : AlgebraicClosure K)

Tactic:
rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]

Premises used: trace_eq_sum_embeddings, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
a :
  ∀ (x : L →ₐ[K] AlgebraicClosure K),
    Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ x →
      (x : (a : L) → AlgebraicClosure K)
          (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
            pb.gen ^ (↑j : ℕ)) =
        HMul.hMul (β := AlgebraicClosure K)
          (HDiv.hDiv (β := AlgebraicClosure K)
            (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
              (↑j : ℕ))
            ((x : (a : L) → AlgebraicClosure K)
                ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
              AlgebraicClosure K))
          ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
⊢ Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ σ : L →ₐ[K] AlgebraicClosure K,
      (σ : (a : L) → AlgebraicClosure K)
        (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
          pb.gen ^ (↑j : ℕ)))
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
σ : L →ₐ[K] AlgebraicClosure K
a :
  Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ σ →
    (σ : (a : L) → AlgebraicClosure K)
        (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
          pb.gen ^ (↑j : ℕ)) =
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((σ : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
⊢ Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ σ →
    (σ : (a : L) → AlgebraicClosure K)
        (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
          pb.gen ^ (↑j : ℕ)) =
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((σ : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)

Tactic:
_
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
σ : L →ₐ[K] AlgebraicClosure K
h : Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ σ
a :
  HDiv.hDiv (α := AlgebraicClosure K) (β := AlgebraicClosure K)
        ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
        ((σ : (a : L) → AlgebraicClosure K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          AlgebraicClosure K) *
      HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ) =
    HMul.hMul (β := AlgebraicClosure K)
      (HDiv.hDiv (β := AlgebraicClosure K)
        (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ))
        ((σ : (a : L) → AlgebraicClosure K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          AlgebraicClosure K))
      ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
⊢ (σ : (a : L) → AlgebraicClosure K)
      (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
        pb.gen ^ (↑j : ℕ)) =
    HMul.hMul (β := AlgebraicClosure K)
      (HDiv.hDiv (β := AlgebraicClosure K)
        (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ))
        ((σ : (a : L) → AlgebraicClosure K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          AlgebraicClosure K))
      ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)

Tactic:
simp only [map_mul, map_div₀, map_pow]

Premises used: map_pow, map_mul, map_div₀
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
σ : L →ₐ[K] AlgebraicClosure K
h : Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ σ
⊢ HDiv.hDiv (α := AlgebraicClosure K) (β := AlgebraicClosure K)
        ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
        ((σ : (a : L) → AlgebraicClosure K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          AlgebraicClosure K) *
      HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ) =
    HMul.hMul (β := AlgebraicClosure K)
      (HDiv.hDiv (β := AlgebraicClosure K)
        (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ))
        ((σ : (a : L) → AlgebraicClosure K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          AlgebraicClosure K))
      ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)

Tactic:
ring
-- 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 : S
⊢ Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) x : R)
    ((LinearMap.trace R S : (a : S →ₗ[R] S) → R) ((lmul R S : (a : S) → End R S) x : End R S) : 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
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
h₁ : ∀ (s : S), Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) s : R) ((0 : (a : S) → R) s : R)
⊢ Eq (α := S →ₗ[R] R) (trace R S) 0

Tactic:
ext s
-- 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
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
s : S
⊢ Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) s : R) ((0 : (a : S) → R) s : R)

Tactic:
simp [trace_apply, LinearMap.trace, h]

Premises used: LinearMap.trace, Algebra.trace_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
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
s : S
rw :
  Eq.{u_1 + 1} (α := R)
    (Matrix.trace.{w, u_1} (n := ι)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lmul R S : (a : S) → End R S) s)))
    (Matrix.trace.{w, u_1} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) (mulLeft R s)))
⊢ Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) s : R)
    (Matrix.trace.{w, u_1} (n := ι) ((leftMulMatrix b : (a : S) → Matrix ι ι R) s) : R)

Tactic:
rw [trace_apply, LinearMap.trace_eq_matrix_trace _ b, ← toMatrix_lmul_eq]

Premises used: Algebra.toMatrix_lmul_eq, LinearMap.trace_eq_matrix_trace, Algebra.trace_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
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
s : S
⊢ Eq.{u_1 + 1} (α := R)
    (Matrix.trace.{w, u_1} (n := ι)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lmul R S : (a : S) → End R S) s)))
    (Matrix.trace.{w, u_1} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) (mulLeft R s)))

Tactic:
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
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
haveI : ∀ (this : DecidableEq ι), (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x

Tactic:
haveI := Classical.decEq ι
-- 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 ι
b : Basis ι R S
x : R
this : DecidableEq ι
rw :
  ∑ i : ι,
      Matrix.diag
        ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
        i =
    Fintype.card ι • x
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x

Tactic:
rw [trace_apply, LinearMap.trace_eq_matrix_trace R b, Matrix.trace]

Premises used: Matrix.trace, LinearMap.trace_eq_matrix_trace, Algebra.trace_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
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ∑ _x : ι, x = Finset.card.{w} (α := ι) Finset.univ • x

Tactic:
Finset.sum_const x

Premises used: Finset.sum_const
-- 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 ι
b : Basis ι R S
x : R
this : DecidableEq ι
h :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ x_1 →
      Matrix.diag
          ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
            ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
          x_1 =
        x
⊢ ∑ i : ι,
      Matrix.diag
        ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
        i =
    Fintype.card ι • x

Tactic:
convert! Finset.sum_const x

Premises used: Finset.sum_const
-- 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 ι
b : Basis ι R S
x : R
this : DecidableEq ι
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
⊢ Matrix.diag
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
      x_1 =
    x

Tactic:
simp [-coe_lmul_eq_mul]

Premises used: Algebra.coe_lmul_eq_mul
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
inst : CommRing R
h : Eq (α := R) ((trace R R : (a : R) → R) 1 : R) ((LinearMap.id : (a : R) → R) 1 : R)
⊢ Eq (α := R →ₗ[R] R) (trace R R) LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R) ((trace R R : (a : R) → R) 1 : R) ((LinearMap.id : (a : R) → R) 1 : R)

Tactic:
simpa using trace_algebraMap_of_basis (.singleton (Fin 1) R) 1

Premises used: Algebra.trace_algebraMap_of_basis, Module.Basis.singleton, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Trace.Defs
Goal:
R : Type u_1
inst : CommRing R
a : R
⊢ (trace R R : (a : R) → R) a = a

Tactic:
simp
-- 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
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
pos :
  ∀ (H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
    (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
neg :
  ∀ (H : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
    (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x

Tactic:
by_cases H : ∃ s : Finset S, Nonempty (Basis s R S)

Premises used: Finset
-- 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
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
pos₁ 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
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x

Tactic:
rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]

Premises used: Exists.choose_spec, Nonempty.some, Module.finrank_eq_card_basis, Algebra.trace_algebraMap_of_basis
-- 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
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
H : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x

Tactic:
simp [trace_eq_zero_of_not_exists_basis R H, finrank_eq_zero_of_not_exists_basis_finset H]

Premises used: finrank_eq_zero_of_not_exists_basis_finset, Algebra.trace_eq_zero_of_not_exists_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
ι : Type u_4
κ : Type u_5
inst_7 : Finite ι
inst_8 : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
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)
⊢ 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 ι
-- 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 : DecidableEq ι
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)
⊢ 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 κ
-- 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 κ
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)
⊢ 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 ι

Premises used: nonempty_fintype
-- 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 ι
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)
⊢ 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 κ

Premises used: nonempty_fintype
-- 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 :
  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))
⊢ 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 [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]

Premises used: Matrix.trace, Finset.univ_product_univ, Algebra.trace_eq_matrix_trace, Module.Basis.smulTower, Finset.sum_product