-- Mathlib/LinearAlgebra/Trace.lean
@[simp]
lemma trace_baseChange [Module.Free R M] [Module.Finite R M]
    (f : M →ₗ[R] M) (A : Type*) [CommRing A] [Algebra R A] :
    trace A _ (f.baseChange A) = algebraMap R A (trace R _ f)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
let b' := Algebra.TensorProduct.basis A b

Result:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
let b := Module.Free.chooseBasis R M

Result:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
change _ = (algebraMap R A : R →+ A) _

Result:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = ↑(algebraMap R A) ((trace R M) f)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = ↑(algebraMap R A) ((trace R M) f)

Tactic:
simp [b', trace_eq_matrix_trace R b, trace_eq_matrix_trace A b', AddMonoidHom.map_trace]

Result:
no goals