M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * z
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
⊢ ↑(lift k (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
      (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z) =
    z
rw [lift_spec]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * z
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * z
cases' f.surj z with x hx
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * mk' f x.fst x.snd
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * z
conv_rhs =>
  congr
  next => skip
  rw [f.eq_mk'_iff_mul_eq.2 hx]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) ((sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst * ↑x.snd) =
    ↑(toMap f) (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst)
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst =
    ↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * mk' f x.fst x.snd
rw [mk', ← mul_assoc, mul_inv_right f.map_units, ← f.toMap.map_mul, ← f.toMap.map_mul]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k) ((sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst * ↑x.snd) =
    ↑(toMap k) (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst)
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) ((sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst * ↑x.snd) =
    ↑(toMap f) (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst)
apply k.eq_of_eq f.map_units
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k) (sec f z).fst *
      (↑(toMap k) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap k) ↑x.snd) =
    ↑(toMap k) ↑(sec f z).snd *
      (↑(toMap k) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap k) x.fst)
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k) ((sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).fst * ↑x.snd) =
    ↑(toMap k) (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst)
rw [k.toMap.map_mul, k.toMap.map_mul, ← sec_spec, mul_assoc, lift_spec_mul]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap k)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k) (sec f z).fst *
      (↑(toMap k) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap k) ↑x.snd) =
    ↑(toMap k) ↑(sec f z).snd *
      (↑(toMap k) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap k) x.fst)
repeat' rw [← k.toMap.map_mul]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap f)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap k)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
apply f.eq_of_eq k.map_units
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec f z).fst *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) x.fst)
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap f)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
repeat' rw [f.toMap.map_mul]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) ↑(sec f z).snd * z *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd *
        (z * ↑(toMap f) ↑x.snd))
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec f z).fst *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) x.fst)
rw [sec_spec', ← hx]
no goals
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) ↑(sec f z).snd * z *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd *
        (z * ↑(toMap f) ↑x.snd))
ac_rfl
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap k)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap k)
      ((sec f z).fst * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑x.snd)) =
    ↑(toMap k)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
rw [← k.toMap.map_mul]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec f z).fst *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) x.fst)
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
k : LocalizationMap S P
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑(toMap f) (sec f z).fst *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) ↑x.snd) =
    ↑(toMap f) ↑(sec f z).snd *
      (↑(toMap f) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap f) x.fst)
rw [f.toMap.map_mul]