-- Mathlib/RingTheory/Trace/Basic.lean
lemma Algebra.trace_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C) (x) :
    e (Algebra.trace A C x) = Algebra.trace B C x

Proof state:
case pos.intro.intro.e_A
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ (↑e.toAddMonoidHom).mapMatrix ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x) = (leftMulMatrix b) x

Tactic:
ext i j

Result:
case pos.intro.intro.e_A.a
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
i j : { x // x ∈ s }
⊢ (↑e.toAddMonoidHom).mapMatrix ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x) i j = (leftMulMatrix b) x i j

Proof state:
case pos.intro.intro
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e.toAddMonoidHom ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x).trace = ((leftMulMatrix b) x).trace

Tactic:
rw [AddMonoidHom.map_trace]

Result:
case pos.intro.intro
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ ((↑e.toAddMonoidHom).mapMatrix ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x)).trace = ((leftMulMatrix b) x).trace

Proof state:
case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } B C)
⊢ e ((trace A C) x) = (trace B C) x

Tactic:
rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
  LinearMap.zero_apply, LinearMap.zero_apply, map_zero]

Result:
case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } B C)
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } A C)

Proof state:
case pos
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ∃ s, Nonempty (Basis { x // x ∈ s } B C)
⊢ e ((trace A C) x) = (trace B C) x

Tactic:
obtain ⟨s, ⟨b⟩⟩ := h

Result:
case pos.intro.intro
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
⊢ e ((trace A C) x) = (trace B C) x

Proof state:
case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } B C)
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } A C)

Tactic:
intro ⟨s, ⟨b⟩⟩

Result:
case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } B C)
s : Finset C
b : Basis { x // x ∈ s } A C
⊢ False