no goals
R : Type u_1
inst✝³² : Semiring R
S : Type u_6
inst✝³¹ : Semiring S
R₂ : Type u_2
inst✝³⁰ : Semiring R₂
S₂ : Type u_7
inst✝²⁹ : Semiring S₂
M : Type u_3
N : Type u_5
P : Type u_4
M₂ : Type ?u.174405
N₂ : Type ?u.174408
P₂ : Type ?u.174411
Nₗ : Type ?u.174414
Pₗ : Type ?u.174417
M' : Type ?u.174420
N' : Type ?u.174423
P' : Type ?u.174426
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : flip f = flip g
m : M
n : N
⊢ ↑(↑(flip f) n) m = ↑(↑(flip g) n) m
rw [H]