Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst✝³⁷ : Semiring R₁
inst✝³⁶ : Semiring 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✝²⁵ : 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₂''
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 σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
⊢ (e₁.arrowCongr e₃) (g ∘ₛₗ f) = (e₂.arrowCongr e₃) g ∘ₛₗ (e₁.arrowCongr e₂) f

Tactic:
ext

Goal state after:
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst✝³⁷ : Semiring R₁
inst✝³⁶ : Semiring 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✝²⁵ : 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₂''
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 σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
x✝ : M₂
⊢ ((e₁.arrowCongr e₃) (g ∘ₛₗ f)) x✝ = ((e₂.arrowCongr e₃) g ∘ₛₗ (e₁.arrowCongr e₂) f) x✝