Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃✝ : Type u_8
inst✝⁷⁰ : CommSemiring R
inst✝⁶⁹ : AddCommMonoid M
inst✝⁶⁸ : AddCommMonoid M₂✝
inst✝⁶⁷ : AddCommMonoid M₃✝
inst✝⁶⁶ : Module R M
inst✝⁶⁵ : Module R M₂✝
inst✝⁶⁴ : Module R M₃✝
R₁ : Type u_9
R₂ : Type u_10
R₃ : Type u_11
R₁' : Type u_12
R₂' : Type u_13
R₃' : Type u_14
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₃ : Type u_19
M₁' : Type u_20
M₂' : Type u_21
M₃' : Type u_22
M₁'' : Type u_23
M₂'' : Type u_24
inst✝⁶³ : Semiring R₁
inst✝⁶² : Semiring R₂
inst✝⁶¹ : Semiring R₃
inst✝⁶⁰ : CommSemiring R₁'
inst✝⁵⁹ : CommSemiring R₂'
inst✝⁵⁸ : CommSemiring R₃'
inst✝⁵⁷ : CommSemiring R₁''
inst✝⁵⁶ : CommSemiring R₂''
inst✝⁵⁵ : AddCommMonoid M₁
inst✝⁵⁴ : AddCommMonoid M₂
inst✝⁵³ : AddCommMonoid M₃
inst✝⁵² : AddCommMonoid M₁'
inst✝⁵¹ : AddCommMonoid M₂'
inst✝⁵⁰ : AddCommMonoid M₃'
inst✝⁴⁹ : AddCommMonoid M₁''
inst✝⁴⁸ : AddCommMonoid M₂''
inst✝⁴⁷ : Module R₁ M₁
inst✝⁴⁶ : Module R₂ M₂
inst✝⁴⁵ : Module R₃ M₃
inst✝⁴⁴ : Module R₁' M₁'
inst✝⁴³ : Module R₂' M₂'
inst✝⁴² : Module R₃' M₃'
inst✝⁴¹ : Module R₁'' M₁''
inst✝⁴⁰ : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₂'₃' : R₂' →+* R₃'
σ₃'₂' : R₃' →+* R₂'
σ₁'₃' : R₁' →+* R₃'
σ₃'₁' : R₃' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₃₃' : R₃ →+* R₃'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₃₂' : R₃ →+* R₂'
σ₂₃' : R₂ →+* R₃'
σ₃₁' : R₃ →+* R₁'
σ₁₃' : R₁ →+* R₃'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst✝³⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁷ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝³⁶ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝³⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³³ : RingHomInvPair σ₂'₃' σ₃'₂'
inst✝³² : RingHomInvPair σ₃'₂' σ₂'₃'
inst✝³¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝³⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁹ : RingHomInvPair σ₁'₃' σ₃'₁'
inst✝²⁸ : RingHomInvPair σ₃'₁' σ₁'₃'
inst✝²⁷ : RingHomInvPair σ₁''₂'' σ₂''₁''
inst✝²⁶ : RingHomInvPair σ₂''₁'' σ₁''₂''
inst✝²⁵ : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst✝²⁴ : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst✝²³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝²² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝²¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝¹⁹ : RingHomCompTriple σ₁₁' σ₁'₃' σ₁₃'
inst✝¹⁸ : RingHomCompTriple σ₃₁ σ₁₃' σ₃₃'
inst✝¹⁷ : RingHomCompTriple σ₃₃' σ₃'₁' σ₃₁'
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₁' σ₁₁'
inst✝¹⁵ : RingHomCompTriple σ₂₂' σ₂'₃' σ₂₃'
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₃' σ₃₃'
inst✝¹³ : RingHomCompTriple σ₃₃' σ₃'₂' σ₃₂'
inst✝¹² : RingHomCompTriple σ₂₃ σ₃₂' σ₂₂'
inst✝¹¹ : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst✝¹⁰ : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst✝⁹ : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst✝⁷ : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst✝⁶ : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst✝⁵ : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst✝⁴ : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'
inst✝ : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
c : R₁'
f : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ (e₁.arrowCongrAddEquiv e₂).toFun (c • f) = σ₁'₂' c • (e₁.arrowCongrAddEquiv e₂).toFun f

Tactic:
ext

Goal state after:
R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃✝ : Type u_8
inst✝⁷⁰ : CommSemiring R
inst✝⁶⁹ : AddCommMonoid M
inst✝⁶⁸ : AddCommMonoid M₂✝
inst✝⁶⁷ : AddCommMonoid M₃✝
inst✝⁶⁶ : Module R M
inst✝⁶⁵ : Module R M₂✝
inst✝⁶⁴ : Module R M₃✝
R₁ : Type u_9
R₂ : Type u_10
R₃ : Type u_11
R₁' : Type u_12
R₂' : Type u_13
R₃' : Type u_14
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₃ : Type u_19
M₁' : Type u_20
M₂' : Type u_21
M₃' : Type u_22
M₁'' : Type u_23
M₂'' : Type u_24
inst✝⁶³ : Semiring R₁
inst✝⁶² : Semiring R₂
inst✝⁶¹ : Semiring R₃
inst✝⁶⁰ : CommSemiring R₁'
inst✝⁵⁹ : CommSemiring R₂'
inst✝⁵⁸ : CommSemiring R₃'
inst✝⁵⁷ : CommSemiring R₁''
inst✝⁵⁶ : CommSemiring R₂''
inst✝⁵⁵ : AddCommMonoid M₁
inst✝⁵⁴ : AddCommMonoid M₂
inst✝⁵³ : AddCommMonoid M₃
inst✝⁵² : AddCommMonoid M₁'
inst✝⁵¹ : AddCommMonoid M₂'
inst✝⁵⁰ : AddCommMonoid M₃'
inst✝⁴⁹ : AddCommMonoid M₁''
inst✝⁴⁸ : AddCommMonoid M₂''
inst✝⁴⁷ : Module R₁ M₁
inst✝⁴⁶ : Module R₂ M₂
inst✝⁴⁵ : Module R₃ M₃
inst✝⁴⁴ : Module R₁' M₁'
inst✝⁴³ : Module R₂' M₂'
inst✝⁴² : Module R₃' M₃'
inst✝⁴¹ : Module R₁'' M₁''
inst✝⁴⁰ : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₂'₃' : R₂' →+* R₃'
σ₃'₂' : R₃' →+* R₂'
σ₁'₃' : R₁' →+* R₃'
σ₃'₁' : R₃' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₃₃' : R₃ →+* R₃'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₃₂' : R₃ →+* R₂'
σ₂₃' : R₂ →+* R₃'
σ₃₁' : R₃ →+* R₁'
σ₁₃' : R₁ →+* R₃'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst✝³⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁷ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝³⁶ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝³⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³³ : RingHomInvPair σ₂'₃' σ₃'₂'
inst✝³² : RingHomInvPair σ₃'₂' σ₂'₃'
inst✝³¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝³⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁹ : RingHomInvPair σ₁'₃' σ₃'₁'
inst✝²⁸ : RingHomInvPair σ₃'₁' σ₁'₃'
inst✝²⁷ : RingHomInvPair σ₁''₂'' σ₂''₁''
inst✝²⁶ : RingHomInvPair σ₂''₁'' σ₁''₂''
inst✝²⁵ : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst✝²⁴ : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst✝²³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝²² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝²¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝¹⁹ : RingHomCompTriple σ₁₁' σ₁'₃' σ₁₃'
inst✝¹⁸ : RingHomCompTriple σ₃₁ σ₁₃' σ₃₃'
inst✝¹⁷ : RingHomCompTriple σ₃₃' σ₃'₁' σ₃₁'
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₁' σ₁₁'
inst✝¹⁵ : RingHomCompTriple σ₂₂' σ₂'₃' σ₂₃'
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₃' σ₃₃'
inst✝¹³ : RingHomCompTriple σ₃₃' σ₃'₂' σ₃₂'
inst✝¹² : RingHomCompTriple σ₂₃ σ₃₂' σ₂₂'
inst✝¹¹ : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst✝¹⁰ : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst✝⁹ : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst✝⁷ : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst✝⁶ : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst✝⁵ : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst✝⁴ : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'
inst✝ : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
c : R₁'
f : M₁ →ₛₗ[σ₁₁'] M₁'
x✝ : M₂
⊢ ((e₁.arrowCongrAddEquiv e₂).toFun (c • f)) x✝ = (σ₁'₂' c • (e₁.arrowCongrAddEquiv e₂).toFun f) x✝