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 }
⊢ ↑(divBy s) (↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑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 }),
    ↑(divBy s) (↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑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 }
⊢ liftOn (↑s • 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 }
⊢ ↑(divBy s) (↑(↑(algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (Quotient.mk (r.setoid S M) (m, t))) =
    Quotient.mk (r.setoid S M) (m, t)
simp only [Module.algebraMap_end_apply, smul'_mk, divBy_apply]
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 ((↑(algebraMap R R) ↑s, 1).fst • (m, t).fst, (↑(algebraMap R R) ↑s, 1).snd * (m, t).snd).fst
      (s * ((↑(algebraMap R R) ↑s, 1).fst • (m, t).fst, (↑(algebraMap R R) ↑s, 1).snd * (m, t).snd).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 }
⊢ liftOn (↑s • 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]
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 (↑(algebraMap R R) ↑s • m) (s * 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
m : M
t : { x // x ∈ S }
⊢ mk ((↑(algebraMap R R) ↑s, 1).fst • (m, t).fst, (↑(algebraMap R R) ↑s, 1).snd * (m, t).snd).fst
      (s * ((↑(algebraMap R R) ↑s, 1).fst • (m, t).fst, (↑(algebraMap R R) ↑s, 1).snd * (m, t).snd).snd) =
    Quotient.mk (r.setoid S M) (m, t)
simp only [one_mul]
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 (↑(algebraMap R R) ↑s • m) (s * t) = 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]