Theorem: TensorProduct.congr'_coe (DividedPowers/ForMathlib/RingTheory/TensorProduct/LinearEquiv.lean)

State before:
R : Type u
M : Type v
N : Type w
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
S : Type u_1
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_2
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
e : M ≃ₗ[S] N
f : P ≃ₗ[R] Q
⊢ ⇑(congr' e f) = ⇑(congr (LinearEquiv.restrictScalars R e) f)
Tactic:
rfl
State after:
no goals