R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
z : S
w w' v : (fun x => P) z
⊢ ↑↑(RingHom.toMonoidWithZeroHom g)
            (Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).fst *
          w +
        ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).snd * w' =
      ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).snd * v ↔
    ↑g (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).fst * w +
        ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * w' =
      ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * v
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
z : S
w w' v : (fun x => P) z
⊢ ↑(Submonoid.LocalizationWithZeroMap.lift (toLocalizationWithZeroMap M S) (RingHom.toMonoidWithZeroHom g) hg) z * w +
        w' =
      v ↔
    ↑g (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).fst * w +
        ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * w' =
      ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * v
erw [mul_comm, ← mul_assoc, mul_add_inv_left hg, mul_comm]
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
z : S
w w' v : (fun x => P) z
⊢ ↑↑(RingHom.toMonoidWithZeroHom g)
            (Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).fst *
          w +
        ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).snd * w' =
      ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationWithZeroMap M S).toLocalizationMap z).snd * v ↔
    ↑g (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).fst * w +
        ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * w' =
      ↑g ↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).snd * v
rfl