case a
M' : Type ?u.113752
X : Type ?u.113755
inst✝²³ : SMul M' X
Y : Type ?u.113762
inst✝²² : SMul M' Y
Z : Type ?u.113769
inst✝²¹ : SMul M' Z
M : Type u_1
inst✝²⁰ : Monoid M
A : Type u_2
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type ?u.113810
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_3
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type ?u.114112
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type ?u.114388
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type ?u.114414
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type ?u.114441
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type ?u.114637
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type ?u.114664
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type ?u.114860
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
M' : Type ?u.113752
X : Type ?u.113755
inst✝²³ : SMul M' X
Y : Type ?u.113762
inst✝²² : SMul M' Y
Z : Type ?u.113769
inst✝²¹ : SMul M' Z
M : Type u_1
inst✝²⁰ : Monoid M
A : Type u_2
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type ?u.113810
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_3
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type ?u.114112
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type ?u.114388
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type ?u.114414
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type ?u.114441
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type ?u.114637
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type ?u.114664
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type ?u.114860
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
⊢ f = g
ext a
no goals
case a
M' : Type ?u.113752
X : Type ?u.113755
inst✝²³ : SMul M' X
Y : Type ?u.113762
inst✝²² : SMul M' Y
Z : Type ?u.113769
inst✝²¹ : SMul M' Z
M : Type u_1
inst✝²⁰ : Monoid M
A : Type u_2
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type ?u.113810
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type u_3
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type ?u.114112
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type ?u.114388
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type ?u.114414
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type ?u.114441
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type ?u.114637
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type ?u.114664
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type ?u.114860
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f g : A →+[M] B
h : ↑f = ↑g
a : A
⊢ ↑f a = ↑g a
exact MulActionHom.congr_fun h a