case mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : { x // x ∈ S }), β (mk m s)
x✝ : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ β (Quot.mk Setoid.r (m, s))
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : { x // x ∈ S }), β (mk m s)
⊢ ∀ (x : LocalizedModule S M), β x
rintro ⟨⟨m, s⟩⟩
no goals
case mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : { x // x ∈ S }), β (mk m s)
x✝ : LocalizedModule S M
m : M
s : { x // x ∈ S }
⊢ β (Quot.mk Setoid.r (m, s))
exact h m s