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