-- Mathlib/RingTheory/Derivation/DifferentialRing.lean
/--
Transfer a `DifferentialAlgebra` instance across a `AlgEquiv`.
-/
lemma DifferentialAlgebra.equiv {A : Type*} [CommRing A] [Differential A]
    {R R₂ : Type*} [CommRing R] [CommRing R₂] [Differential R₂] [Algebra A R]
    [Algebra A R₂] [DifferentialAlgebra A R₂] (h : R ≃ₐ[A] R₂) :
    letI := Differential.equiv h.toRingEquiv
    DifferentialAlgebra A R :=
  letI := Differential.equiv h.toRingEquiv
  ⟨fun a ↦ by
    change (LinearMap.comp ..) _ = _
    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.toAddMonoidHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
      AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
      Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]
    apply h.symm.commutes⟩

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ ((algebraMap A R) a)′ = (algebraMap A R) a′

Tactic:
change (LinearMap.comp ..) _ = _

Result:
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ (h.toRingEquiv.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
        ↑Differential.deriv ∘ₗ h.toRingEquiv.toAddMonoidHom.toIntLinearMap)
      ((algebraMap A R) a) =
    (algebraMap A R) a′

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ (h.toRingEquiv.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
        ↑Differential.deriv ∘ₗ h.toRingEquiv.toAddMonoidHom.toIntLinearMap)
      ((algebraMap A R) a) =
    (algebraMap A R) a′

Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.toAddMonoidHom_eq_coe,
  RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
  AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
  Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]

Result:
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ (↑h).symm ((algebraMap A R₂) a′) = (algebraMap A R) a′

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ (↑h).symm ((algebraMap A R₂) a′) = (algebraMap A R) a′

Tactic:
apply h.symm.commutes

Result:
no goals