-- Mathlib/RingTheory/Trace/Basic.lean
lemma Algebra.trace_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [CommRing B₁]
    [CommRing A₂] [CommRing B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) :
    Algebra.trace A₁ B₁ x = e₁.symm (Algebra.trace A₂ B₂ (e₂ x))

Proof state:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }

Result:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Proof state:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra

Result:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Proof state:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e',
  RingEquiv.symm_apply_apply]

Result:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₂) (e' x) = (trace A₁ B₂) (e₂ x)

Proof state:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₂) (e' x) = (trace A₁ B₂) (e₂ x)

Tactic:
rfl

Result:
no goals