case h
R : Type u_2
R₁ : Type ?u.342124
R₂ : Type ?u.342127
R₃ : Type ?u.342130
k : Type ?u.342133
S : Type ?u.342136
M : Type u_1
M₁ : Type ?u.342142
M₂ : Type ?u.342145
M₃ : Type ?u.342148
N₁ : Type ?u.342151
N₂ : Type ?u.342154
N₃ : Type ?u.342157
N₄ : Type ?u.342160
ι : Type ?u.342163
M₄ : Type ?u.342166
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Subsingleton M
inst✝ : Subsingleton M₂
x✝ : M
⊢ ↑(ofSubsingleton M M) x✝ = ↑(refl R M) x✝
R : Type u_2
R₁ : Type ?u.342124
R₂ : Type ?u.342127
R₃ : Type ?u.342130
k : Type ?u.342133
S : Type ?u.342136
M : Type u_1
M₁ : Type ?u.342142
M₂ : Type ?u.342145
M₃ : Type ?u.342148
N₁ : Type ?u.342151
N₂ : Type ?u.342154
N₃ : Type ?u.342157
N₄ : Type ?u.342160
ι : Type ?u.342163
M₄ : Type ?u.342166
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Subsingleton M
inst✝ : Subsingleton M₂
⊢ ofSubsingleton M M = refl R M
ext
no goals
case h
R : Type u_2
R₁ : Type ?u.342124
R₂ : Type ?u.342127
R₃ : Type ?u.342130
k : Type ?u.342133
S : Type ?u.342136
M : Type u_1
M₁ : Type ?u.342142
M₂ : Type ?u.342145
M₃ : Type ?u.342148
N₁ : Type ?u.342151
N₂ : Type ?u.342154
N₃ : Type ?u.342157
N₄ : Type ?u.342160
ι : Type ?u.342163
M₄ : Type ?u.342166
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Subsingleton M
inst✝ : Subsingleton M₂
x✝ : M
⊢ ↑(ofSubsingleton M M) x✝ = ↑(refl R M) x✝
simp