case a
M' : Type u_2
X : Type ?u.188449
inst✝²⁵ : SMul M' X
Y : Type ?u.188456
inst✝²⁴ : SMul M' Y
Z : Type ?u.188463
inst✝²³ : SMul M' Z
M : Type ?u.188470
inst✝²² : Monoid M
A : Type ?u.188476
inst✝²¹ : AddMonoid A
inst✝²⁰ : DistribMulAction M A
A' : Type ?u.188504
inst✝¹⁹ : AddGroup A'
inst✝¹⁸ : DistribMulAction M A'
B : Type ?u.188780
inst✝¹⁷ : AddMonoid B
inst✝¹⁶ : DistribMulAction M B
B' : Type ?u.188806
inst✝¹⁵ : AddGroup B'
inst✝¹⁴ : DistribMulAction M B'
C : Type ?u.189082
inst✝¹³ : AddMonoid C
inst✝¹² : DistribMulAction M C
R : Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : MulSemiringAction M R
R' : Type ?u.189135
inst✝⁹ : Ring R'
inst✝⁸ : MulSemiringAction M R'
S : Type ?u.189331
inst✝⁷ : Semiring S
inst✝⁶ : MulSemiringAction M S
S' : Type ?u.189358
inst✝⁵ : Ring S'
inst✝⁴ : MulSemiringAction M S'
T : Type ?u.189554
inst✝³ : Semiring T
inst✝² : MulSemiringAction M T
inst✝¹ : AddMonoid M'
inst✝ : DistribMulAction R M'
f g : R →+[R] M'
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
M' : Type u_2
X : Type ?u.188449
inst✝²⁵ : SMul M' X
Y : Type ?u.188456
inst✝²⁴ : SMul M' Y
Z : Type ?u.188463
inst✝²³ : SMul M' Z
M : Type ?u.188470
inst✝²² : Monoid M
A : Type ?u.188476
inst✝²¹ : AddMonoid A
inst✝²⁰ : DistribMulAction M A
A' : Type ?u.188504
inst✝¹⁹ : AddGroup A'
inst✝¹⁸ : DistribMulAction M A'
B : Type ?u.188780
inst✝¹⁷ : AddMonoid B
inst✝¹⁶ : DistribMulAction M B
B' : Type ?u.188806
inst✝¹⁵ : AddGroup B'
inst✝¹⁴ : DistribMulAction M B'
C : Type ?u.189082
inst✝¹³ : AddMonoid C
inst✝¹² : DistribMulAction M C
R : Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : MulSemiringAction M R
R' : Type ?u.189135
inst✝⁹ : Ring R'
inst✝⁸ : MulSemiringAction M R'
S : Type ?u.189331
inst✝⁷ : Semiring S
inst✝⁶ : MulSemiringAction M S
S' : Type ?u.189358
inst✝⁵ : Ring S'
inst✝⁴ : MulSemiringAction M S'
T : Type ?u.189554
inst✝³ : Semiring T
inst✝² : MulSemiringAction M T
inst✝¹ : AddMonoid M'
inst✝ : DistribMulAction R M'
f g : R →+[R] M'
h : ↑f 1 = ↑g 1
⊢ f = g
ext x
no goals
case a
M' : Type u_2
X : Type ?u.188449
inst✝²⁵ : SMul M' X
Y : Type ?u.188456
inst✝²⁴ : SMul M' Y
Z : Type ?u.188463
inst✝²³ : SMul M' Z
M : Type ?u.188470
inst✝²² : Monoid M
A : Type ?u.188476
inst✝²¹ : AddMonoid A
inst✝²⁰ : DistribMulAction M A
A' : Type ?u.188504
inst✝¹⁹ : AddGroup A'
inst✝¹⁸ : DistribMulAction M A'
B : Type ?u.188780
inst✝¹⁷ : AddMonoid B
inst✝¹⁶ : DistribMulAction M B
B' : Type ?u.188806
inst✝¹⁵ : AddGroup B'
inst✝¹⁴ : DistribMulAction M B'
C : Type ?u.189082
inst✝¹³ : AddMonoid C
inst✝¹² : DistribMulAction M C
R : Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : MulSemiringAction M R
R' : Type ?u.189135
inst✝⁹ : Ring R'
inst✝⁸ : MulSemiringAction M R'
S : Type ?u.189331
inst✝⁷ : Semiring S
inst✝⁶ : MulSemiringAction M S
S' : Type ?u.189358
inst✝⁵ : Ring S'
inst✝⁴ : MulSemiringAction M S'
T : Type ?u.189554
inst✝³ : Semiring T
inst✝² : MulSemiringAction M T
inst✝¹ : AddMonoid M'
inst✝ : DistribMulAction R M'
f g : R →+[R] M'
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
rw [← mul_one x, ← smul_eq_mul R, f.map_smul, g.map_smul, h]