R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ ↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (↑(divBy s) (Quotient.mk (r.setoid S M) (m, t))) =
    Quotient.mk (r.setoid S M) (m, t)
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
⊢ ∀ (a : M × { x // x ∈ S }),
    ↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (↑(divBy s) (Quotient.mk (r.setoid S M) a)) =
      Quotient.mk (r.setoid S M) a
intro ⟨m, t⟩
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ ↑s •
      liftOn (Quotient.mk (r.setoid S M) (m, t)) (fun p => mk p.fst (s * p.snd))
        (_ :
          ∀ (x x_1 : M × { x // x ∈ S }),
            x ≈ x_1 → (fun p => mk p.fst (s * p.snd)) x = (fun p => mk p.fst (s * p.snd)) x_1) =
    Quotient.mk (r.setoid S M) (m, t)
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ ↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (↑(divBy s) (Quotient.mk (r.setoid S M) (m, t))) =
    Quotient.mk (r.setoid S M) (m, t)
simp only [LocalizedModule.liftOn_mk, divBy_apply, Module.algebraMap_end_apply, smul'_mk]
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ mk (↑s • (m, t).fst) (s * (m, t).snd) = Quotient.mk (r.setoid S M) (m, t)
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ ↑s •
      liftOn (Quotient.mk (r.setoid S M) (m, t)) (fun p => mk p.fst (s * p.snd))
        (_ :
          ∀ (x x_1 : M × { x // x ∈ S }),
            x ≈ x_1 → (fun p => mk p.fst (s * p.snd)) x = (fun p => mk p.fst (s * p.snd)) x_1) =
    Quotient.mk (r.setoid S M) (m, t)
erw [LocalizedModule.liftOn_mk, smul'_mk]
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ mk (s • m) (s * t) = mk m t
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ mk (↑s • (m, t).fst) (s * (m, t).snd) = Quotient.mk (r.setoid S M) (m, t)
change mk (s • m) (s * t) = mk m t
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
p : LocalizedModule S M
m : M
t : { x // x ∈ S }
⊢ mk (s • m) (s * t) = mk m t
rw [mk_cancel_common_left s t]