-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃_1 : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M₃_1
inst_4 : Module R M
inst_5 : Module R M₂_1
inst_6 : Module R M₃_1
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_7 : Semiring R₁
inst_8 : Semiring R₂
inst_9 : Semiring R₃
inst_10 : CommSemiring R₁'
inst_11 : CommSemiring R₂'
inst_12 : CommSemiring R₃'
inst_13 : CommSemiring R₁''
inst_14 : CommSemiring R₂''
inst_15 : AddCommMonoid M₁
inst_16 : AddCommMonoid M₂
inst_17 : AddCommMonoid M₃
inst_18 : AddCommMonoid M₁'
inst_19 : AddCommMonoid M₂'
inst_20 : AddCommMonoid M₃'
inst_21 : AddCommMonoid M₁''
inst_22 : AddCommMonoid M₂''
inst_23 : Module R₁ M₁
inst_24 : Module R₂ M₂
inst_25 : Module R₃ M₃
inst_26 : Module R₁' M₁'
inst_27 : Module R₂' M₂'
inst_28 : Module R₃' M₃'
inst_29 : Module R₁'' M₁''
inst_30 : 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_31 : RingHomInvPair σ₁₂ σ₂₁
inst_32 : RingHomInvPair σ₂₁ σ₁₂
inst_33 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_34 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_35 : RingHomInvPair σ₂₃ σ₃₂
inst_36 : RingHomInvPair σ₃₂ σ₂₃
inst_37 : RingHomInvPair σ₂'₃' σ₃'₂'
inst_38 : RingHomInvPair σ₃'₂' σ₂'₃'
inst_39 : RingHomInvPair σ₁₃ σ₃₁
inst_40 : RingHomInvPair σ₃₁ σ₁₃
inst_41 : RingHomInvPair σ₁'₃' σ₃'₁'
inst_42 : RingHomInvPair σ₃'₁' σ₁'₃'
inst_43 : RingHomInvPair σ₁''₂'' σ₂''₁''
inst_44 : RingHomInvPair σ₂''₁'' σ₁''₂''
inst_45 : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst_46 : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst_47 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_48 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_49 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_50 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_51 : RingHomCompTriple σ₁₁' σ₁'₃' σ₁₃'
inst_52 : RingHomCompTriple σ₃₁ σ₁₃' σ₃₃'
inst_53 : RingHomCompTriple σ₃₃' σ₃'₁' σ₃₁'
inst_54 : RingHomCompTriple σ₁₃ σ₃₁' σ₁₁'
inst_55 : RingHomCompTriple σ₂₂' σ₂'₃' σ₂₃'
inst_56 : RingHomCompTriple σ₃₂ σ₂₃' σ₃₃'
inst_57 : RingHomCompTriple σ₃₃' σ₃'₂' σ₃₂'
inst_58 : RingHomCompTriple σ₂₃ σ₃₂' σ₂₂'
inst_59 : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst_60 : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst_61 : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst_62 : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst_63 : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst_64 : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst_65 : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst_66 : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
inst_67 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_68 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_69 : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'
inst_70 : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
c : R₁'
f : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ (e₁.arrowCongrAddEquiv e₂).toFun (c • f) =
    HSMul.hSMul (α := R₂') ((σ₁'₂' : (a : R₁') → R₂') c : R₂') ((e₁.arrowCongrAddEquiv e₂).toFun f)
have h : ∀ (x : M₂),
  Eq.{u_21 + 1} (α := M₂') (((e₁.arrowCongrAddEquiv e₂).toFun (c • f) : (a : M₂) → M₂') x : M₂')
    ((HSMul.hSMul (α := R₂') ((σ₁'₂' : (a : R₁') → R₂') c : R₂') ((e₁.arrowCongrAddEquiv e₂).toFun f) : (a : M₂) → M₂')
        x :
      M₂')
Tactic: ext