[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ Con (M × { x // x ∈ S })
[PROOFSTEP]
refine
  { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
    iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
    mul' := ?_ }
[GOAL]
case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {x y z : M × { x // x ∈ S }},
    (∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)) →
      (∃ c, ↑c * (↑z.snd * y.fst) = ↑c * (↑y.snd * z.fst)) → ∃ c, ↑c * (↑z.snd * x.fst) = ↑c * (↑x.snd * z.fst)
[PROOFSTEP]
rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
[GOAL]
case refine_1.intro.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ∃ c_1, ↑c_1 * (↑c.snd * a.fst) = ↑c_1 * (↑a.snd * c.fst)
[PROOFSTEP]
use t₂ * t₁ * b.2
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑(t₂ * t₁ * b.snd) * (↑c.snd * a.fst) = ↑(t₂ * t₁ * b.snd) * (↑a.snd * c.fst)
[PROOFSTEP]
simp only [Submonoid.coe_mul]
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₂ * ↑t₁ * ↑b.snd * (↑c.snd * a.fst) = ↑t₂ * ↑t₁ * ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
calc
  (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
  _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
  _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₂ * ↑t₁ * ↑b.snd * (↑c.snd * a.fst) = ↑t₂ * ↑c.snd * (↑t₁ * (↑b.snd * a.fst))
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₂ * ↑c.snd * (↑t₁ * (↑b.snd * a.fst)) = ↑t₁ * ↑a.snd * (↑t₂ * (↑c.snd * b.fst))
[PROOFSTEP]
rw [ht₁]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₂ * ↑c.snd * (↑t₁ * (↑a.snd * b.fst)) = ↑t₁ * ↑a.snd * (↑t₂ * (↑c.snd * b.fst))
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₁ * ↑a.snd * (↑t₂ * (↑c.snd * b.fst)) = ↑t₂ * ↑t₁ * ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
rw [ht₂]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑c.snd * b.fst) = ↑t₂ * (↑b.snd * c.fst)
⊢ ↑t₁ * ↑a.snd * (↑t₂ * (↑b.snd * c.fst)) = ↑t₂ * ↑t₁ * ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
ac_rfl
[GOAL]
case refine_2
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {w x y z : M × { x // x ∈ S }}, Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
[PROOFSTEP]
rintro a b c d ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
[GOAL]
case refine_2.intro.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑d.snd * c.fst) = ↑t₂ * (↑c.snd * d.fst)
⊢ Setoid.r (a * c) (b * d)
[PROOFSTEP]
use t₂ * t₁
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑d.snd * c.fst) = ↑t₂ * (↑c.snd * d.fst)
⊢ ↑(t₂ * t₁) * (↑(b * d).snd * (a * c).fst) = ↑(t₂ * t₁) * (↑(a * c).snd * (b * d).fst)
[PROOFSTEP]
calc
  (t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
  _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑d.snd * c.fst) = ↑t₂ * (↑c.snd * d.fst)
⊢ ↑t₂ * ↑t₁ * (↑b.snd * ↑d.snd * (a.fst * c.fst)) = ↑t₂ * (↑d.snd * c.fst) * (↑t₁ * (↑b.snd * a.fst))
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑d.snd * c.fst) = ↑t₂ * (↑c.snd * d.fst)
⊢ ↑t₂ * (↑d.snd * c.fst) * (↑t₁ * (↑b.snd * a.fst)) = ↑t₂ * ↑t₁ * (↑a.snd * ↑c.snd * (b.fst * d.fst))
[PROOFSTEP]
rw [ht₁, ht₂]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × { x // x ∈ S }
t₁ : { x // x ∈ S }
ht₁ : ↑t₁ * (↑b.snd * a.fst) = ↑t₁ * (↑a.snd * b.fst)
t₂ : { x // x ∈ S }
ht₂ : ↑t₂ * (↑d.snd * c.fst) = ↑t₂ * (↑c.snd * d.fst)
⊢ ↑t₂ * (↑c.snd * d.fst) * (↑t₁ * (↑a.snd * b.fst)) = ↑t₂ * ↑t₁ * (↑a.snd * ↑c.snd * (b.fst * d.fst))
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x✝ : { x // x ∈ S }
⊢ ↑1 * (↑(↑x✝, x✝).snd * 1.fst) = ↑1 * (↑1.snd * (↑x✝, x✝).fst)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b (p, q) (x, y)
[PROOFSTEP]
rw [← one_mul (p, q), ← one_mul (x, y)]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b (1 * (p, q)) (1 * (x, y))
[PROOFSTEP]
refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b ((↑(t * y), t * y) * (p, q)) (1 * (x, y))
[PROOFSTEP]
convert b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
[GOAL]
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ (↑(t * y), t * y) * (p, q) = (↑(t * q), t * q) * (x, y)
[PROOFSTEP]
dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
[GOAL]
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)
[PROOFSTEP]
simp_rw [mul_assoc, ht, mul_comm y q]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
⊢ ↑(r S) x y ↔ ∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)
[PROOFSTEP]
rw [r_eq_r' S]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
⊢ ↑(r' S) x y ↔ ∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y z : Localization S
⊢ Localization.mul S (Localization.mul S x y) z = Localization.mul S x (Localization.mul S y z)
[PROOFSTEP]
rw [Localization.mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y z : Localization S
⊢ Mul.mul (Mul.mul x y) z = Mul.mul x (Mul.mul y z)
[PROOFSTEP]
apply (r S).commMonoid.mul_assoc
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Localization.mul S (Localization.one S) x = x
[PROOFSTEP]
rw [Localization.mul, Localization.one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Mul.mul One.one x = x
[PROOFSTEP]
apply (r S).commMonoid.one_mul
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Localization.mul S x (Localization.one S) = x
[PROOFSTEP]
rw [Localization.mul, Localization.one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Mul.mul x One.one = x
[PROOFSTEP]
apply (r S).commMonoid.mul_one
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Localization.npow S 0 x = Localization.one S
[PROOFSTEP]
rw [Localization.npow, Localization.one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : Localization S
⊢ Monoid.npow 0 x = One.one
[PROOFSTEP]
apply (r S).commMonoid.npow_zero
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
n : ℕ
x : Localization S
⊢ Localization.npow S (Nat.succ n) x = Localization.mul S x (Localization.npow S n x)
[PROOFSTEP]
rw [Localization.npow, Localization.mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
n : ℕ
x : Localization S
⊢ Monoid.npow (Nat.succ n) x = Mul.mul x (Monoid.npow n x)
[PROOFSTEP]
apply (r S).commMonoid.npow_succ
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : Localization S
⊢ Localization.mul S x y = Localization.mul S y x
[PROOFSTEP]
rw [Localization.mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : Localization S
⊢ Mul.mul x y = Mul.mul y x
[PROOFSTEP]
apply (r S).commMonoid.mul_comm
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : { x // x ∈ S }) → p (mk a b)
H : ∀ {a c : M} {b d : { x // x ∈ S }} (h : ↑(r S) (a, b) (c, d)), (_ : mk a b = mk c d) ▸ f a b = f c d
x : Localization S
y : M × { x // x ∈ S }
⊢ mk y.fst y.snd = Quot.mk Setoid.r y
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : { x // x ∈ S }) → p (mk a b)
H : ∀ {a c : M} {b d : { x // x ∈ S }} (h : ↑(r S) (a, b) (c, d)), (_ : mk a b = mk c d) ▸ f a b = f c d
x : Localization S
y z : M × { x // x ∈ S }
h : Setoid.r y z
⊢ (_ : Quot.mk Setoid.r y = Quot.mk Setoid.r z) ▸ (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) y =
    (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) z
[PROOFSTEP]
cases y
[GOAL]
case mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : { x // x ∈ S }) → p (mk a b)
H : ∀ {a c : M} {b d : { x // x ∈ S }} (h : ↑(r S) (a, b) (c, d)), (_ : mk a b = mk c d) ▸ f a b = f c d
x : Localization S
z : M × { x // x ∈ S }
fst✝ : M
snd✝ : { x // x ∈ S }
h : Setoid.r (fst✝, snd✝) z
⊢ (_ : Quot.mk Setoid.r (fst✝, snd✝) = Quot.mk Setoid.r z) ▸
      (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) (fst✝, snd✝) =
    (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) z
[PROOFSTEP]
cases z
[GOAL]
case mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : { x // x ∈ S }) → p (mk a b)
H : ∀ {a c : M} {b d : { x // x ∈ S }} (h : ↑(r S) (a, b) (c, d)), (_ : mk a b = mk c d) ▸ f a b = f c d
x : Localization S
fst✝¹ : M
snd✝¹ : { x // x ∈ S }
fst✝ : M
snd✝ : { x // x ∈ S }
h : Setoid.r (fst✝¹, snd✝¹) (fst✝, snd✝)
⊢ (_ : Quot.mk Setoid.r (fst✝¹, snd✝¹) = Quot.mk Setoid.r (fst✝, snd✝)) ▸
      (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) (fst✝¹, snd✝¹) =
    (fun y => (_ : mk y.fst y.snd = mk y.fst y.snd) ▸ f y.fst y.snd) (fst✝, snd✝)
[PROOFSTEP]
exact H h
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a c : M
b d : { x // x ∈ S }
⊢ Localization.mul S (mk a b) (mk c d) = mk (a * c) (b * d)
[PROOFSTEP]
rw [Localization.mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a c : M
b d : { x // x ∈ S }
⊢ Mul.mul (mk a b) (mk c d) = mk (a * c) (b * d)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ mk 1 1 = Localization.one S
[PROOFSTEP]
rw [Localization.one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ mk 1 1 = One.one
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
n : ℕ
a : M
b : { x // x ∈ S }
⊢ Localization.npow S n (mk a b) = mk (a ^ n) (b ^ n)
[PROOFSTEP]
rw [Localization.npow]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
n : ℕ
a : M
b : { x // x ∈ S }
⊢ Monoid.npow n (mk a b) = mk (a ^ n) (b ^ n)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Sort u
x : Localization S
f : M → { x // x ∈ S } → p
H : ∀ {a c : M} {b d : { x // x ∈ S }}, ↑(r S) (a, b) (c, d) → f a b = f c d
a✝ c✝ : M
b✝ d✝ : { x // x ∈ S }
h : ↑(r S) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a✝ b✝ = mk c✝ d✝) ▸ f a✝ b✝ = f c✝ d✝
[PROOFSTEP]
simpa only [eq_rec_constant] using H h
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
h : ↑y.snd * x.fst = ↑x.snd * y.fst
⊢ ↑1 * (↑y.snd * x.fst) = ↑1 * (↑x.snd * y.fst)
[PROOFSTEP]
rw [h]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ mk (↑a) a = 1
[PROOFSTEP]
symm
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ 1 = mk (↑a) a
[PROOFSTEP]
rw [← mk_one, mk_eq_mk_iff]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ ↑(r S) (1, 1) (↑a, a)
[PROOFSTEP]
exact one_rel a
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' : M
b b' : { x // x ∈ S }
h : ↑(r S) (a, b) (a', b')
⊢ ↑(r S) (c • a, b) (c • a', b')
[PROOFSTEP]
cases' b with b hb
[GOAL]
case mk
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' : M
b' : { x // x ∈ S }
b : M
hb : b ∈ S
h : ↑(r S) (a, { val := b, property := hb }) (a', b')
⊢ ↑(r S) (c • a, { val := b, property := hb }) (c • a', b')
[PROOFSTEP]
cases' b' with b' hb'
[GOAL]
case mk.mk
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
h : ↑(r S) (a, { val := b, property := hb }) (a', { val := b', property := hb' })
⊢ ↑(r S) (c • a, { val := b, property := hb }) (c • a', { val := b', property := hb' })
[PROOFSTEP]
rw [r_eq_r'] at h ⊢
[GOAL]
case mk.mk
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
h : ↑(r' S) (a, { val := b, property := hb }) (a', { val := b', property := hb' })
⊢ ↑(r' S) (c • a, { val := b, property := hb }) (c • a', { val := b', property := hb' })
[PROOFSTEP]
cases' h with t ht
[GOAL]
case mk.mk.intro
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
t : { x // x ∈ S }
ht :
  ↑t * (↑(a', { val := b', property := hb' }).snd * (a, { val := b, property := hb }).fst) =
    ↑t * (↑(a, { val := b, property := hb }).snd * (a', { val := b', property := hb' }).fst)
⊢ ↑(r' S) (c • a, { val := b, property := hb }) (c • a', { val := b', property := hb' })
[PROOFSTEP]
use t
[GOAL]
case h
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
t : { x // x ∈ S }
ht :
  ↑t * (↑(a', { val := b', property := hb' }).snd * (a, { val := b, property := hb }).fst) =
    ↑t * (↑(a, { val := b, property := hb }).snd * (a', { val := b', property := hb' }).fst)
⊢ ↑t * (↑(c • a', { val := b', property := hb' }).snd * (c • a, { val := b, property := hb }).fst) =
    ↑t * (↑(c • a, { val := b, property := hb }).snd * (c • a', { val := b', property := hb' }).fst)
[PROOFSTEP]
dsimp only [Subtype.coe_mk] at ht ⊢
  -- TODO: this definition should take `SMulCommClass R M M` instead of `IsScalarTower R M M` if
  -- we ever want to generalize to the non-commutative case.
[GOAL]
case h
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
t : { x // x ∈ S }
ht : ↑t * (b' * a) = ↑t * (b * a')
⊢ ↑t * (b' * c • a) = ↑t * (b * c • a')
[PROOFSTEP]
haveI : SMulCommClass R M M := ⟨fun r m₁ m₂ ↦ by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
t : { x // x ∈ S }
ht : ↑t * (b' * a) = ↑t * (b * a')
r : R
m₁ m₂ : M
⊢ r • m₁ • m₂ = m₁ • r • m₂
[PROOFSTEP]
simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]
[GOAL]
case h
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
z : Localization S
a a' b : M
hb : b ∈ S
b' : M
hb' : b' ∈ S
t : { x // x ∈ S }
ht : ↑t * (b' * a) = ↑t * (b * a')
this : SMulCommClass R M M
⊢ ↑t * (b' * c • a) = ↑t * (b * c • a')
[PROOFSTEP]
simp only [mul_smul_comm, ht]
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ c • mk a b = mk (c • a) b
[PROOFSTEP]
simp only [HSMul.hSMul, instHSMul, SMul.smul, instSMulLocalization, Localization.smul]
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (SMul.smul c a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
[PROOFSTEP]
show liftOn (mk a b) (fun a b => mk (c • a) b) _ = _
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (c • a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
[PROOFSTEP]
exact liftOn_mk (fun a b => mk (c • a) b) _ a b
[GOAL]
M : Type u_1
inst✝⁷ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁶ : CommMonoid N
P : Type u_3
inst✝⁵ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴ : SMul R₁ M
inst✝³ : SMul R₂ M
inst✝² : IsScalarTower R₁ M M
inst✝¹ : IsScalarTower R₂ M M
inst✝ : SMulCommClass R₁ R₂ M
s : R₁
t : R₂
r : M
x : { x // x ∈ S }
⊢ s • t • mk (r, x).fst (r, x).snd = t • s • mk (r, x).fst (r, x).snd
[PROOFSTEP]
simp only [smul_mk, smul_comm s t r]
[GOAL]
M : Type u_1
inst✝⁸ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁷ : CommMonoid N
P : Type u_3
inst✝⁶ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝⁵ : SMul R₁ M
inst✝⁴ : SMul R₂ M
inst✝³ : IsScalarTower R₁ M M
inst✝² : IsScalarTower R₂ M M
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ M
s : R₁
t : R₂
r : M
x : { x // x ∈ S }
⊢ (s • t) • mk (r, x).fst (r, x).snd = s • t • mk (r, x).fst (r, x).snd
[PROOFSTEP]
simp only [smul_mk, smul_assoc s t r]
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R✝ : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : Type u_7
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
s : R
r₁ : M
x₁ : { x // x ∈ S }
r₂ : M
x₂ : { x // x ∈ S }
⊢ s • mk (r₁, x₁).fst (r₁, x₁).snd • mk (r₂, x₂).fst (r₂, x₂).snd =
    mk (r₁, x₁).fst (r₁, x₁).snd • s • mk (r₂, x₂).fst (r₂, x₂).snd
[PROOFSTEP]
simp only [smul_mk, smul_eq_mul, mk_mul, mul_comm r₁, smul_mul_assoc]
[GOAL]
M : Type u_1
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝³ : CommMonoid N
P : Type u_3
inst✝² : CommMonoid P
R✝ : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : Type u_7
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
s : R
r₁ : M
x₁ : { x // x ∈ S }
r₂ : M
x₂ : { x // x ∈ S }
⊢ (s • mk (r₁, x₁).fst (r₁, x₁).snd) • mk (r₂, x₂).fst (r₂, x₂).snd =
    s • mk (r₁, x₁).fst (r₁, x₁).snd • mk (r₂, x₂).fst (r₂, x₂).snd
[PROOFSTEP]
simp only [smul_mk, smul_eq_mul, mk_mul, smul_mul_assoc]
[GOAL]
M : Type u_1
inst✝⁷ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁶ : CommMonoid N
P : Type u_3
inst✝⁵ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴ : SMul R M
inst✝³ : SMul Rᵐᵒᵖ M
inst✝² : IsScalarTower R M M
inst✝¹ : IsScalarTower Rᵐᵒᵖ M M
inst✝ : IsCentralScalar R M
s : R
r : M
x : { x // x ∈ S }
⊢ MulOpposite.op s • mk (r, x).fst (r, x).snd = s • mk (r, x).fst (r, x).snd
[PROOFSTEP]
simp only [smul_mk, op_smul_eq_smul]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : IsScalarTower R M M
⊢ ∀ (fst : M) (snd : { x // x ∈ S }), 1 • mk (fst, snd).fst (fst, snd).snd = mk (fst, snd).fst (fst, snd).snd
[PROOFSTEP]
intros
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : IsScalarTower R M M
fst✝ : M
snd✝ : { x // x ∈ S }
⊢ 1 • mk (fst✝, snd✝).fst (fst✝, snd✝).snd = mk (fst✝, snd✝).fst (fst✝, snd✝).snd
[PROOFSTEP]
simp only [Localization.smul_mk, one_smul]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : IsScalarTower R M M
s₁ s₂ : R
⊢ ∀ (fst : M) (snd : { x // x ∈ S }),
    (s₁ * s₂) • mk (fst, snd).fst (fst, snd).snd = s₁ • s₂ • mk (fst, snd).fst (fst, snd).snd
[PROOFSTEP]
intros
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : IsScalarTower R M M
s₁ s₂ : R
fst✝ : M
snd✝ : { x // x ∈ S }
⊢ (s₁ * s₂) • mk (fst✝, snd✝).fst (fst✝, snd✝).snd = s₁ • s₂ • mk (fst✝, snd✝).fst (fst✝, snd✝).snd
[PROOFSTEP]
simp only [Localization.smul_mk, mul_smul]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulDistribMulAction R M
inst✝ : IsScalarTower R M M
s : R
x y : Localization S
r₁ : M
x₁ : { x // x ∈ S }
r₂ : M
x₂ : { x // x ∈ S }
⊢ s • (mk (r₁, x₁).fst (r₁, x₁).snd * mk (r₂, x₂).fst (r₂, x₂).snd) =
    s • mk (r₁, x₁).fst (r₁, x₁).snd * s • mk (r₂, x₂).fst (r₂, x₂).snd
[PROOFSTEP]
simp only [Localization.smul_mk, Localization.mk_mul, smul_mul']
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
R : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst✝² : Monoid R
inst✝¹ : MulDistribMulAction R M
inst✝ : IsScalarTower R M M
s : R
⊢ s • 1 = 1
[PROOFSTEP]
simp only [← Localization.mk_one, Localization.smul_mk, smul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f g : LocalizationMap S N
h : ∀ (x : M), ↑(toMap f) x = ↑(toMap g) x
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟩⟩
[GOAL]
case mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : LocalizationMap S N
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
map_units'✝ : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑x.snd =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x.fst
eq_iff_exists'✝ :
  ∀ (x y : M),
    OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) y ↔
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    ↑(toMap
            { toMonoidHom := { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }, map_units' := map_units'✝,
              surj' := surj'✝, eq_iff_exists' := eq_iff_exists'✝ })
        x =
      ↑(toMap g) x
⊢ { toMonoidHom := { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }, map_units' := map_units'✝, surj' := surj'✝,
      eq_iff_exists' := eq_iff_exists'✝ } =
    g
[PROOFSTEP]
rcases g with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
map_units'✝¹ : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } ↑y)
surj'✝¹ :
  ∀ (z : N),
    ∃ x,
      z * OneHom.toFun ↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } ↑x.snd =
        OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) x.fst
eq_iff_exists'✝¹ :
  ∀ (x y : M),
    OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) x =
        OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) y ↔
      ∃ c, ↑c * x = ↑c * y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
map_units'✝ : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑x.snd =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x.fst
eq_iff_exists'✝ :
  ∀ (x y : M),
    OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) y ↔
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    ↑(toMap
            { toMonoidHom := { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }, map_units' := map_units'✝¹,
              surj' := surj'✝¹, eq_iff_exists' := eq_iff_exists'✝¹ })
        x =
      ↑(toMap
            { toMonoidHom := { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }, map_units' := map_units'✝,
              surj' := surj'✝, eq_iff_exists' := eq_iff_exists'✝ })
        x
⊢ { toMonoidHom := { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }, map_units' := map_units'✝¹, surj' := surj'✝¹,
      eq_iff_exists' := eq_iff_exists'✝¹ } =
    { toMonoidHom := { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }, map_units' := map_units'✝, surj' := surj'✝,
      eq_iff_exists' := eq_iff_exists'✝ }
[PROOFSTEP]
simp only [mk.injEq, MonoidHom.mk.injEq]
[GOAL]
case mk.mk.mk.mk
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
map_units'✝¹ : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } ↑y)
surj'✝¹ :
  ∀ (z : N),
    ∃ x,
      z * OneHom.toFun ↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } ↑x.snd =
        OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) x.fst
eq_iff_exists'✝¹ :
  ∀ (x y : M),
    OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) x =
        OneHom.toFun (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }) y ↔
      ∃ c, ↑c * x = ↑c * y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
map_units'✝ : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * OneHom.toFun ↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ } ↑x.snd =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x.fst
eq_iff_exists'✝ :
  ∀ (x y : M),
    OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) x =
        OneHom.toFun (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }) y ↔
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    ↑(toMap
            { toMonoidHom := { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }, map_units' := map_units'✝¹,
              surj' := surj'✝¹, eq_iff_exists' := eq_iff_exists'✝¹ })
        x =
      ↑(toMap
            { toMonoidHom := { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }, map_units' := map_units'✝,
              surj' := surj'✝, eq_iff_exists' := eq_iff_exists'✝ })
        x
⊢ toOneHom✝¹ = toOneHom✝
[PROOFSTEP]
exact OneHom.ext h
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
z : N
⊢ ↑(toMap f) (sec f z).fst = ↑(toMap f) ↑(sec f z).snd * z
[PROOFSTEP]
rw [mul_comm, sec_spec]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ w * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ = z ↔ w = ↑f ↑y * z
[PROOFSTEP]
rw [mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ * w = z ↔ w = ↑f ↑y * z
[PROOFSTEP]
exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ z = w * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ ↔ z * ↑f ↑y = w
[PROOFSTEP]
rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ ↑f x₁ * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y₁)⁻¹ =
      ↑f x₂ * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y₂)⁻¹ ↔
    ↑f (x₁ * ↑y₂) = ↑f (x₂ * ↑y₁)
[PROOFSTEP]
rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂, f.map_mul, f.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
hf : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y z : { x // x ∈ S }
h : (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) y)⁻¹ = (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹
⊢ ↑f ↑y = ↑f ↑z
[PROOFSTEP]
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
hf : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y z : { x // x ∈ S }
h : (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) y)⁻¹ = (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹
⊢ ↑f ↑z * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹ = 1
[PROOFSTEP]
exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
z : N
H : ↑f ↑y * z = 1
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ = z
[PROOFSTEP]
rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
z : N
H : ↑f ↑y * z = 1
⊢ ↑1 = ↑f ↑y * z
[PROOFSTEP]
exact H.symm
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) (↑c * x) = ↑(toMap f) (↑c * y)
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
rw [f.toMap.map_mul, f.toMap.map_mul] at h 
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
cases' f.map_units c with u hu
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
u : ((fun x => N) ↑c)ˣ
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
rw [← hu] at h 
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
u : ((fun x => N) ↑c)ˣ
h : ↑u * ↑(toMap f) x = ↑u * ↑(toMap f) y
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
exact (Units.mul_right_inj u).1 h
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) (x * ↑c) = ↑(toMap f) (y * ↑c)
⊢ ↑(toMap f) (↑(?m.701298 h) * x) = ↑(toMap f) (↑(?m.701298 h) * y)
[PROOFSTEP]
rw [mul_comm _ x, mul_comm _ y, h]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ ↑(toMap f) (x₁ * x₂) =
    ↑(toMap f) ↑(y₁ * y₂) *
      (↑(toMap f) x₁ *
          ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
                y₁)⁻¹ *
        (↑(toMap f) x₂ *
          ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
                y₂)⁻¹))
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, mul_inv_right f.map_units, mul_assoc, mul_assoc, mul_comm _ (f.toMap x₂), ← mul_assoc, ←
  mul_assoc, mul_inv_right f.map_units, Submonoid.coe_mul, f.toMap.map_mul, f.toMap.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ ↑(toMap f) x₁ * ↑(toMap f) x₂ * ↑(toMap f) ↑y₂ * ↑(toMap f) ↑y₁ =
    ↑(toMap f) ↑y₁ * ↑(toMap f) ↑y₂ * ↑(toMap f) x₁ * ↑(toMap f) x₂
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
⊢ mk' f x 1 = ↑(toMap f) x
[PROOFSTEP]
rw [mk', MonoidHom.map_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
⊢ ↑(toMap f) x * ↑1⁻¹ = ↑(toMap f) x
[PROOFSTEP]
exact mul_one _
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
z : N
⊢ ↑(toMap f) (sec f z).fst *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
            (sec f z).snd)⁻¹ =
    z
[PROOFSTEP]
rw [← sec_spec, mul_inv_left, mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) x *
        ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
              y)⁻¹ *
      ↑(toMap f) ↑y =
    ↑(toMap f) x
[PROOFSTEP]
rw [mul_assoc, mul_comm _ (f.toMap y), ← mul_assoc, mul_inv_left, mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) ↑y * mk' f x y = ↑(toMap f) x
[PROOFSTEP]
rw [mul_comm, mk'_spec]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
z : N
H : z = mk' f x y
⊢ z * ↑(toMap f) ↑y = ↑(toMap f) x
[PROOFSTEP]
rw [H, mk'_spec]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
z : N
H : z * ↑(toMap f) ↑y = ↑(toMap f) x
⊢ z = mk' f x y
[PROOFSTEP]
erw [mul_inv_right, H]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
z : N
⊢ mk' f x y = z ↔ ↑(toMap f) x = z * ↑(toMap f) ↑y
[PROOFSTEP]
rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
H : mk' f x₁ y₁ = mk' f x₂ y₂
⊢ ↑(toMap f) (↑y₂ * x₁) = ↑(toMap f) (↑y₁ * x₂)
[PROOFSTEP]
rw [f.toMap.map_mul, f.toMap.map_mul, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm ((toMap f) x₂) _]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
H : ↑(toMap f) (↑y₂ * x₁) = ↑(toMap f) (↑y₁ * x₂)
⊢ mk' f x₁ y₁ = mk' f x₂ y₂
[PROOFSTEP]
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f.toMap y₁), ← mul_assoc, ← f.toMap.map_mul, mul_comm x₂, ← H, ←
  mul_comm x₁, f.toMap.map_mul, mul_inv_right f.map_units]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ mk' f x₁ y₁ = mk' f x₂ y₂ ↔ ↑(toMap f) (x₁ * ↑y₂) = ↑(toMap f) (x₂ * ↑y₁)
[PROOFSTEP]
simp only [f.mk'_eq_iff_eq, mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
a₁ b₁ : M
a₂ b₂ : { x // x ∈ S }
⊢ mk' f a₁ a₂ = mk' f b₁ b₂ ↔ ↑(Localization.r S) (a₁, a₂) (b₁, b₂)
[PROOFSTEP]
rw [f.eq, Localization.r_iff_exists]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
a₁ b₁ : M
a₂ b₂ : { x // x ∈ S }
H : b₁ * ↑a₂ = a₁ * ↑b₂
⊢ ↑a₂ * b₁ = ↑b₂ * a₁
[PROOFSTEP]
simpa only [mul_comm] using H
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
y : { x // x ∈ S }
⊢ ↑(toMap f) ↑y *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y))) y)⁻¹ =
    1
[PROOFSTEP]
rw [mul_inv_left, mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y : { x // x ∈ S }
⊢ ↑(toMap f) x₁ * mk' f x₂ y = mk' f (x₁ * x₂) y
[PROOFSTEP]
rw [← mk'_one, ← mk'_mul, one_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y : { x // x ∈ S }
⊢ mk' f x₂ y * ↑(toMap f) x₁ = mk' f (x₁ * x₂) y
[PROOFSTEP]
rw [mul_comm, mul_mk'_eq_mk'_of_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) x * mk' f 1 y = mk' f x y
[PROOFSTEP]
rw [mul_mk'_eq_mk'_of_mul, mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ mk' f (x * ↑y) y = ↑(toMap f) x
[PROOFSTEP]
rw [← mul_mk'_one_eq_mk', f.toMap.map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ mk' f (↑y * x) y = ↑(toMap f) x
[PROOFSTEP]
rw [mul_comm, mk'_mul_cancel_right]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M
h : ↑(toMap f) x = ↑(toMap f) y
⊢ ↑g x = ↑g y
[PROOFSTEP]
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑g x = ↑g y
[PROOFSTEP]
rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑(MonoidHom.restrict g S) c * ↑g x = ↑g y
[PROOFSTEP]
show _ * g c * _ = _
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑g ↑c * ↑g x = ↑g y
[PROOFSTEP]
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ (fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹) 1 = 1
[PROOFSTEP]
rw [mul_inv_left, mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ ↑g (sec f 1).fst = ↑g ↑(sec f 1).snd
[PROOFSTEP]
exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ ↑(toMap f) (sec f 1).fst = ↑(toMap f) ↑(sec f 1).snd
[PROOFSTEP]
rw [← sec_spec, one_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ OneHom.toFun
      { toFun := fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹,
        map_one' :=
          (_ : (fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹,
          map_one' :=
            (_ :
              (fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹,
          map_one' :=
            (_ :
              (fun z => ↑g (sec f z).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f z).snd)⁻¹) 1 = 1) }
        y
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g (sec f (x * y)).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f (x * y)).snd)⁻¹ =
    ↑g (sec f x).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f x).snd)⁻¹ *
      (↑g (sec f y).fst * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) (sec f y).snd)⁻¹)
[PROOFSTEP]
rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ← mul_assoc, ← mul_assoc,
  mul_inv_right hg]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g (sec f (x * y)).fst * ↑g ↑(sec f y).snd * ↑g ↑(sec f x).snd =
    ↑g (sec f y).fst * ↑g ↑(sec f (x * y)).snd * ↑g (sec f x).fst
[PROOFSTEP]
repeat' rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g (sec f (x * y)).fst * ↑g ↑(sec f y).snd * ↑g ↑(sec f x).snd =
    ↑g (sec f y).fst * ↑g ↑(sec f (x * y)).snd * ↑g (sec f x).fst
[PROOFSTEP]
rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g ((sec f (x * y)).fst * ↑(sec f y).snd) * ↑g ↑(sec f x).snd =
    ↑g (sec f y).fst * ↑g ↑(sec f (x * y)).snd * ↑g (sec f x).fst
[PROOFSTEP]
rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g ((sec f (x * y)).fst * ↑(sec f y).snd * ↑(sec f x).snd) =
    ↑g (sec f y).fst * ↑g ↑(sec f (x * y)).snd * ↑g (sec f x).fst
[PROOFSTEP]
rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g ((sec f (x * y)).fst * ↑(sec f y).snd * ↑(sec f x).snd) =
    ↑g ((sec f y).fst * ↑(sec f (x * y)).snd) * ↑g (sec f x).fst
[PROOFSTEP]
rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g ((sec f (x * y)).fst * ↑(sec f y).snd * ↑(sec f x).snd) = ↑g ((sec f y).fst * ↑(sec f (x * y)).snd * (sec f x).fst)
[PROOFSTEP]
rw [← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑g ((sec f (x * y)).fst * ↑(sec f y).snd * ↑(sec f x).snd) = ↑g ((sec f y).fst * ↑(sec f (x * y)).snd * (sec f x).fst)
[PROOFSTEP]
exact f.eq_of_eq hg (by simp_rw [f.toMap.map_mul, sec_spec']; ac_rfl)
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑(toMap f) ((sec f (x * y)).fst * ↑(sec f y).snd * ↑(sec f x).snd) =
    ↑(toMap f) ((sec f y).fst * ↑(sec f (x * y)).snd * (sec f x).fst)
[PROOFSTEP]
simp_rw [f.toMap.map_mul, sec_spec']
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : N
⊢ ↑(toMap f) ↑(sec f (x * y)).snd * (x * y) * ↑(toMap f) ↑(sec f y).snd * ↑(toMap f) ↑(sec f x).snd =
    ↑(toMap f) ↑(sec f y).snd * y * ↑(toMap f) ↑(sec f (x * y)).snd * (↑(toMap f) ↑(sec f x).snd * x)
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) ((sec f (mk' f x y)).fst * ↑y) = ↑(toMap f) (x * ↑(sec f (mk' f x y)).snd)
[PROOFSTEP]
simp_rw [f.toMap.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
z : N
w v : (fun x => P) z
⊢ ↑(lift f hg) z * w = v ↔ ↑g (sec f z).fst * w = ↑g ↑(sec f z).snd * v
[PROOFSTEP]
erw [mul_comm, ← mul_assoc, mul_inv_left hg, mul_comm]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
v : P
y : { x // x ∈ S }
⊢ ↑(lift f hg) (mk' f x y) = v ↔ ↑g x = ↑g ↑y * v
[PROOFSTEP]
rw [f.lift_mk' hg]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
v : P
y : { x // x ∈ S }
⊢ ↑g x * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) y)⁻¹ = v ↔ ↑g x = ↑g ↑y * v
[PROOFSTEP]
exact mul_inv_left hg _ _ _
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
z : N
⊢ ↑(lift f hg) z * ↑g ↑(sec f z).snd = ↑g (sec f z).fst
[PROOFSTEP]
erw [mul_assoc, IsUnit.liftRight_inv_mul, mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
z : N
⊢ ↑g ↑(sec f z).snd * ↑(lift f hg) z = ↑g (sec f z).fst
[PROOFSTEP]
rw [mul_comm, lift_mul_right]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑(lift f hg) (↑(toMap f) x) = ↑g x
[PROOFSTEP]
rw [lift_spec, ← g.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑g (sec f (↑(toMap f) x)).fst = ↑g (↑(sec f (↑(toMap f) x)).snd * x)
[PROOFSTEP]
exact f.eq_of_eq hg (by rw [sec_spec', f.toMap.map_mul])
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑(toMap f) (sec f (↑(toMap f) x)).fst = ↑(toMap f) (↑(sec f (↑(toMap f) x)).snd * x)
[PROOFSTEP]
rw [sec_spec', f.toMap.map_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M × { x // x ∈ S }
⊢ ↑(lift f hg) (mk' f x.fst x.snd) = ↑(lift f hg) (mk' f y.fst y.snd) ↔ ↑g (x.fst * ↑y.snd) = ↑g (y.fst * ↑x.snd)
[PROOFSTEP]
rw [lift_mk', lift_mk', mul_inv hg]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ MonoidHom.comp (lift f hg) (toMap f) = g
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x✝ : M
⊢ ↑(MonoidHom.comp (lift f hg) (toMap f)) x✝ = ↑g x✝
[PROOFSTEP]
exact f.lift_eq hg _
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
⊢ lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y)) = j
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
x✝ : N
⊢ ↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y))) x✝ = ↑j x✝
[PROOFSTEP]
rw [lift_spec]
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
x✝ : N
⊢ ↑(MonoidHom.comp j (toMap f)) (sec f x✝).fst = ↑(MonoidHom.comp j (toMap f)) ↑(sec f x✝).snd * ↑j x✝
[PROOFSTEP]
show j _ = j _ * _
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd) * ↑j x✝
[PROOFSTEP]
erw [← j.map_mul, sec_spec']
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
⊢ j = k
[PROOFSTEP]
rw [← f.lift_of_comp j, ← f.lift_of_comp k]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
⊢ lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y)) =
    lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp k (toMap f)) ↑y))
[PROOFSTEP]
congr 1 with x
[GOAL]
case e_g.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
x : M
⊢ ↑(MonoidHom.comp j (toMap f)) x = ↑(MonoidHom.comp k (toMap f)) x
[PROOFSTEP]
exact h x
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
⊢ lift f hg = j
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(lift f hg) x✝ = ↑j x✝
[PROOFSTEP]
rw [lift_spec, ← hj, ← hj, ← j.map_mul]
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd * x✝)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
j : N →* P
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(toMap f) (sec f x✝).fst = ↑(toMap f) ↑(sec f x✝).snd * x✝
[PROOFSTEP]
rw [← sec_spec']
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
[PROOFSTEP]
rw [lift_spec]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
[PROOFSTEP]
cases' f.surj z with x hx
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
[PROOFSTEP]
conv_rhs =>
  congr
  next => skip
  rw [f.eq_mk'_iff_mul_eq.2 hx]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd * z
[PROOFSTEP]
  congr
  next => skip
  rw [f.eq_mk'_iff_mul_eq.2 hx]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd * z
[PROOFSTEP]
  congr
  next => skip
  rw [f.eq_mk'_iff_mul_eq.2 hx]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd * z
[PROOFSTEP]
congr
[GOAL]
case a
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd
case a
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
| z
[PROOFSTEP]
next => skip
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd
[PROOFSTEP]
skip
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd
[PROOFSTEP]
skip
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)).snd
[PROOFSTEP]
skip
[GOAL]
case a
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
| z
[PROOFSTEP]
rw [f.eq_mk'_iff_mul_eq.2 hx]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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
[PROOFSTEP]
rw [mk', ← mul_assoc, mul_inv_right f.map_units, ← f.toMap.map_mul, ← f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
apply k.eq_of_eq f.map_units
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
rw [k.toMap.map_mul, k.toMap.map_mul, ← sec_spec, mul_assoc, lift_spec_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
repeat' rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 * ↑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)
[PROOFSTEP]
rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 *
      (↑(toMap k) ↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * ↑(toMap k) x.fst)
[PROOFSTEP]
rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 *
      ↑(toMap k) (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst)
[PROOFSTEP]
rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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))
[PROOFSTEP]
rw [← k.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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))
[PROOFSTEP]
apply f.eq_of_eq k.map_units
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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))
[PROOFSTEP]
repeat' rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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))
[PROOFSTEP]
rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 * ↑x.snd) =
    ↑(toMap f)
      (↑(sec f z).snd * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
[PROOFSTEP]
rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 * (↑(sec k (↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap k) ↑y))) z)).snd * x.fst))
[PROOFSTEP]
rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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 * x.fst)
[PROOFSTEP]
rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
rw [f.toMap.map_mul]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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)
[PROOFSTEP]
rw [sec_spec', ← hx]
[GOAL]
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
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))
[PROOFSTEP]
ac_rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Surjective ↑(lift f hg) ↔ ∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Surjective ↑(lift f hg) → ∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
intro H v
[GOAL]
case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Surjective ↑(lift f hg)
v : P
⊢ ∃ x, v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
obtain ⟨z, hz⟩ := H v
[GOAL]
case mp.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Surjective ↑(lift f hg)
v : P
z : N
hz : ↑(lift f hg) z = v
⊢ ∃ x, v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
obtain ⟨x, hx⟩ := f.surj z
[GOAL]
case mp.intro.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Surjective ↑(lift f hg)
v : P
z : N
hz : ↑(lift f hg) z = v
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ∃ x, v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
use x
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Surjective ↑(lift f hg)
v : P
z : N
hz : ↑(lift f hg) z = v
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ v * ↑g ↑x.snd = ↑g x.fst
[PROOFSTEP]
rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2)]
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Surjective ↑(lift f hg)
v : P
z : N
hz : ↑(lift f hg) z = v
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑g x.fst * (↑g ↑x.snd * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) x.snd)⁻¹) = ↑g x.fst
[PROOFSTEP]
erw [IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
[GOAL]
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ (∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst) → Surjective ↑(lift f hg)
[PROOFSTEP]
intro H v
[GOAL]
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst
v : P
⊢ ∃ a, ↑(lift f hg) a = v
[PROOFSTEP]
obtain ⟨x, hx⟩ := H v
[GOAL]
case mpr.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst
v : P
x : M × { x // x ∈ S }
hx : v * ↑g ↑x.snd = ↑g x.fst
⊢ ∃ a, ↑(lift f hg) a = v
[PROOFSTEP]
use f.mk' x.1 x.2
[GOAL]
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (v : P), ∃ x, v * ↑g ↑x.snd = ↑g x.fst
v : P
x : M × { x // x ∈ S }
hx : v * ↑g ↑x.snd = ↑g x.fst
⊢ ↑(lift f hg) (mk' f x.fst x.snd) = v
[PROOFSTEP]
rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Injective ↑(lift f hg) ↔ ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Injective ↑(lift f hg) → ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
[PROOFSTEP]
intro H x y
[GOAL]
case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
[PROOFSTEP]
constructor
[GOAL]
case mp.mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y → ↑g x = ↑g y
[PROOFSTEP]
exact f.eq_of_eq hg
[GOAL]
case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑g x = ↑g y → ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
intro h
[GOAL]
case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑g x = ↑g y
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
rw [← f.lift_eq hg, ← f.lift_eq hg] at h 
[GOAL]
case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑(lift f hg) (↑(toMap f) x) = ↑(lift f hg) (↑(toMap f) y)
⊢ ↑(toMap f) x = ↑(toMap f) y
[PROOFSTEP]
exact H h
[GOAL]
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ (∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y) → Injective ↑(lift f hg)
[PROOFSTEP]
intro H z w h
[GOAL]
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
⊢ z = w
[PROOFSTEP]
obtain ⟨_, _⟩ := f.surj z
[GOAL]
case mpr.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝ : M × { x // x ∈ S }
h✝ : z * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
[PROOFSTEP]
obtain ⟨_, _⟩ := f.surj w
[GOAL]
case mpr.intro.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
[PROOFSTEP]
rw [← f.mk'_sec z, ← f.mk'_sec w]
[GOAL]
case mpr.intro.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ mk' f (sec f z).fst (sec f z).snd = mk' f (sec f w).fst (sec f w).snd
[PROOFSTEP]
exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
y : { x // x ∈ S }
⊢ ↑(map f hy k) (mk' f x y) = mk' k (↑g x) { val := ↑g ↑y, property := (_ : ↑g ↑y ∈ T) }
[PROOFSTEP]
rw [map, lift_mk', mul_inv_left]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
y : { x // x ∈ S }
⊢ ↑(MonoidHom.comp (toMap k) g) x =
    ↑(MonoidHom.comp (toMap k) g) ↑y * mk' k (↑g x) { val := ↑g ↑y, property := (_ : ↑g ↑y ∈ T) }
[PROOFSTEP]
show k.toMap (g x) = k.toMap (g y) * _
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
y : { x // x ∈ S }
⊢ ↑(toMap k) (↑g x) = ↑(toMap k) (↑g ↑y) * mk' k (↑g x) { val := ↑g ↑y, property := (_ : ↑g ↑y ∈ T) }
[PROOFSTEP]
rw [mul_mk'_eq_mk'_of_mul]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
y : { x // x ∈ S }
⊢ ↑(toMap k) (↑g x) = mk' k (↑g ↑y * ↑g x) { val := ↑g ↑y, property := (_ : ↑g ↑y ∈ T) }
[PROOFSTEP]
exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
z : N
⊢ ↑(toMap k) (↑g ↑(sec f z).snd) * ↑(map f hy k) z = ↑(toMap k) (↑g (sec f z).fst)
[PROOFSTEP]
rw [mul_comm, f.map_mul_right]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
⊢ MonoidHom.comp (map k hl j) (map f hy k) = map f (_ : ∀ (x : { x // x ∈ S }), ↑(MonoidHom.comp l g) ↑x ∈ U) j
[PROOFSTEP]
ext z
[GOAL]
case h
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(MonoidHom.comp (map k hl j) (map f hy k)) z =
    ↑(map f (_ : ∀ (x : { x // x ∈ S }), ↑(MonoidHom.comp l g) ↑x ∈ U) j) z
[PROOFSTEP]
show j.toMap _ * _ = j.toMap (l _) * _
[GOAL]
case h
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(toMap j) (↑l (sec k (↑(map f hy k) z)).fst) *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (MonoidHom.comp (toMap j) l) T)
                (_ : ∀ (y : { x // x ∈ T }), IsUnit (↑(toMap j) ↑{ val := ↑l ↑y, property := (_ : ↑l ↑y ∈ U) })))
            (sec k (↑(map f hy k) z)).snd)⁻¹ =
    ↑(toMap j) (↑l (↑g (sec f z).fst)) *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (MonoidHom.comp (toMap j) (MonoidHom.comp l g)) S)
                (_ :
                  ∀ (y : { x // x ∈ S }),
                    IsUnit
                      (↑(toMap j)
                        ↑{ val := ↑(MonoidHom.comp l g) ↑y, property := (_ : ↑(MonoidHom.comp l g) ↑y ∈ U) })))
            (sec f z).snd)⁻¹
[PROOFSTEP]
rw [mul_inv_left, ← mul_assoc, mul_inv_right]
[GOAL]
case h
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(toMap j) (↑l (sec k (↑(map f hy k) z)).fst) * ↑(MonoidHom.comp (toMap j) (MonoidHom.comp l g)) ↑(sec f z).snd =
    ↑(MonoidHom.comp (toMap j) l) ↑(sec k (↑(map f hy k) z)).snd * ↑(toMap j) (↑l (↑g (sec f z).fst))
[PROOFSTEP]
show j.toMap _ * j.toMap (l (g _)) = j.toMap (l _) * _
[GOAL]
case h
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(toMap j) (↑l (sec k (↑(map f hy k) z)).fst) * ↑(toMap j) (↑l (↑g ↑(sec f z).snd)) =
    ↑(toMap j) (↑l ↑(sec k (↑(map f hy k) z)).snd) * ↑(toMap j) (↑l (↑g (sec f z).fst))
[PROOFSTEP]
rw [← j.toMap.map_mul, ← j.toMap.map_mul, ← l.map_mul, ← l.map_mul]
[GOAL]
case h
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(toMap j) (↑l ((sec k (↑(map f hy k) z)).fst * ↑g ↑(sec f z).snd)) =
    ↑(toMap j) (↑l (↑(sec k (↑(map f hy k) z)).snd * ↑g (sec f z).fst))
[PROOFSTEP]
exact k.comp_eq_of_eq hl j (by rw [k.toMap.map_mul, k.toMap.map_mul, sec_spec', mul_assoc, map_mul_right])
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
z : N
⊢ ↑(toMap k) ((sec k (↑(map f hy k) z)).fst * ↑g ↑(sec f z).snd) =
    ↑(toMap k) (↑(sec k (↑(map f hy k) z)).snd * ↑g (sec f z).fst)
[PROOFSTEP]
rw [k.toMap.map_mul, k.toMap.map_mul, sec_spec', mul_assoc, map_mul_right]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
x : N
⊢ ↑(map k hl j) (↑(map f hy k) x) = ↑(map f (_ : ∀ (x : { x // x ∈ S }), ↑(MonoidHom.comp l g) ↑x ∈ U) j) x
[PROOFSTEP]
rw [← @map_comp_map M _ S N _ P _ f g T hy Q _ k A _ U R _ j l hl]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
x : N
⊢ ↑(map k hl j) (↑(map f hy k) x) = ↑(MonoidHom.comp (map k hl j) (map f hy k)) x
[PROOFSTEP]
simp only [MonoidHom.coe_comp, comp_apply]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg✝ : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
F : AwayMap x N
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ powers x }
⊢ IsUnit (↑g ↑y)
[PROOFSTEP]
obtain ⟨n, hn⟩ := y.2
[GOAL]
case intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg✝ : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
F : AwayMap x N
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ powers x }
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = ↑y
⊢ IsUnit (↑g ↑y)
[PROOFSTEP]
rw [← hn, g.map_pow]
[GOAL]
case intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg✝ : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
F : AwayMap x N
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ powers x }
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = ↑y
⊢ IsUnit (↑g x ^ n)
[PROOFSTEP]
exact IsUnit.pow n hg
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap T Q
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
⊢ ↑(toMap G) x * mk' G y { val := x * y, property := (_ : x * y ∈ powers (x * y)) } = 1
[PROOFSTEP]
rw [mul_mk'_eq_mk'_of_mul, mk'_self]
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (↑g x)
y : { x_1 // x_1 ∈ multiples x }
⊢ IsAddUnit (↑g ↑y)
[PROOFSTEP]
obtain ⟨n, hn⟩ := y.2
[GOAL]
case intro
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (↑g x)
y : { x_1 // x_1 ∈ multiples x }
n : ℕ
hn : (fun i => i • x) n = ↑y
⊢ IsAddUnit (↑g ↑y)
[PROOFSTEP]
rw [← hn]
[GOAL]
case intro
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (↑g x)
y : { x_1 // x_1 ∈ multiples x }
n : ℕ
hn : (fun i => i • x) n = ↑y
⊢ IsAddUnit (↑g ((fun i => i • x) n))
[PROOFSTEP]
dsimp
[GOAL]
case intro
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (↑g x)
y : { x_1 // x_1 ∈ multiples x }
n : ℕ
hn : (fun i => i • x) n = ↑y
⊢ IsAddUnit (↑g (n • x))
[PROOFSTEP]
rw [g.map_nsmul]
[GOAL]
case intro
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (↑g x)
y : { x_1 // x_1 ∈ multiples x }
n : ℕ
hn : (fun i => i • x) n = ↑y
⊢ IsAddUnit (n • ↑g x)
[PROOFSTEP]
exact IsAddUnit.map (nsmulAddMonoidHom n : C →+ C) hg
[GOAL]
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ ↑(toMap G) x + mk' G y { val := x + y, property := (_ : x + y ∈ multiples (x + y)) } = 0
[PROOFSTEP]
rw [add_mk'_eq_mk'_of_add, mk'_self]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : ↑k.toEquiv z = v
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ v * ↑k (↑(toMap f) ↑x.snd) = ↑k (↑(toMap f) x.fst)
[PROOFSTEP]
rw [← hx, k.map_mul, ← hz]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : ↑k.toEquiv z = v
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
⊢ ↑k.toEquiv z * ↑k (↑(toMap f) ↑x.snd) = ↑k z * ↑k (↑(toMap f) ↑x.snd)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : LocalizationMap S P
x : M
⊢ ↑(toMap (ofMulEquivOfLocalizations f (mulEquivOfLocalizations f k))) x = ↑(toMap k) x
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
x : N
⊢ ↑(mulEquivOfLocalizations f (ofMulEquivOfLocalizations f k)) x = ↑k x
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
⊢ ofMulEquivOfLocalizations f (MulEquiv.refl N) = f
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfLocalizations f (MulEquiv.refl N))) x✝ = ↑(toMap f) x✝
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
⊢ toMap (ofMulEquivOfLocalizations f (MulEquiv.trans k j)) =
    MonoidHom.comp (MulEquiv.toMonoidHom j) (toMap (ofMulEquivOfLocalizations f k))
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfLocalizations f (MulEquiv.trans k j))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom j) (toMap (ofMulEquivOfLocalizations f k))) x✝
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
z : N
x : M × { x // x ∈ S }
hx : z * ↑(toMap f) ↑x.snd = ↑(toMap f) x.fst
v : P
hv : ↑k.toEquiv v = x.fst
w : P
hw : ↑k.toEquiv w = ↑x.snd
⊢ z * ↑(toMap f) (↑k.toEquiv w) = ↑(toMap f) (↑k.toEquiv v)
[PROOFSTEP]
erw [hv, hw, hx]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
⊢ ↑(toMap f) (↑(MulEquiv.toMonoidHom k) x) = ↑(toMap f) (↑(MulEquiv.toMonoidHom k) y) ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
erw [f.eq_iff_exists]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
⊢ (∃ c, ↑c * ↑(MulEquiv.toMonoidHom k) x = ↑c * ↑(MulEquiv.toMonoidHom k) y) ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
exact
  ⟨fun ⟨c, hc⟩ ↦
    let ⟨d, hd⟩ := k.toEquiv.surjective c
    ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, by erw [← hd, ← k.map_mul, ← k.map_mul] at hc ;
      exact k.toEquiv.injective hc⟩,
    fun ⟨c, hc⟩ ↦ ⟨⟨k c, H ▸ Set.mem_image_of_mem k c.2⟩, by erw [← k.map_mul]; rw [hc, k.map_mul]; rfl⟩⟩
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
x✝ : ∃ c, ↑c * ↑(MulEquiv.toMonoidHom k) x = ↑c * ↑(MulEquiv.toMonoidHom k) y
c : { x // x ∈ S }
hc : ↑c * ↑(MulEquiv.toMonoidHom k) x = ↑c * ↑(MulEquiv.toMonoidHom k) y
d : P
hd : ↑k.toEquiv d = ↑c
⊢ ↑{ val := d, property := (_ : d ∈ T) } * x = ↑{ val := d, property := (_ : d ∈ T) } * y
[PROOFSTEP]
erw [← hd, ← k.map_mul, ← k.map_mul] at hc 
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
x✝ : ∃ c, ↑c * ↑(MulEquiv.toMonoidHom k) x = ↑c * ↑(MulEquiv.toMonoidHom k) y
c : { x // x ∈ S }
d : P
hc : ↑k (d * x) = ↑k (d * y)
hd : ↑k.toEquiv d = ↑c
⊢ ↑{ val := d, property := (_ : d ∈ T) } * x = ↑{ val := d, property := (_ : d ∈ T) } * y
[PROOFSTEP]
exact k.toEquiv.injective hc
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
x✝ : ∃ c, ↑c * x = ↑c * y
c : { x // x ∈ T }
hc : ↑c * x = ↑c * y
⊢ ↑{ val := ↑k ↑c, property := (_ : ↑k ↑c ∈ S) } * ↑(MulEquiv.toMonoidHom k) x =
    ↑{ val := ↑k ↑c, property := (_ : ↑k ↑c ∈ S) } * ↑(MulEquiv.toMonoidHom k) y
[PROOFSTEP]
erw [← k.map_mul]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
x✝ : ∃ c, ↑c * x = ↑c * y
c : { x // x ∈ T }
hc : ↑c * x = ↑c * y
⊢ ↑k (↑c * x) = ↑{ val := ↑k ↑c, property := (_ : ↑k ↑c ∈ S) } * ↑(MulEquiv.toMonoidHom k) y
[PROOFSTEP]
rw [hc, k.map_mul]
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map (MulEquiv.toMonoidHom k) T = S
H' : comap (MulEquiv.toMonoidHom k) S = T :=
  H ▸ SetLike.coe_injective (Set.preimage_image_eq T.carrier (Equiv.injective k.toEquiv))
x y : P
x✝ : ∃ c, ↑c * x = ↑c * y
c : { x // x ∈ T }
hc : ↑c * x = ↑c * y
⊢ ↑k ↑c * ↑k y = ↑{ val := ↑k ↑c, property := (_ : ↑k ↑c ∈ S) } * ↑(MulEquiv.toMonoidHom k) y
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
⊢ ofMulEquivOfDom f (_ : Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.refl M)) S = S) = f
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfDom f (_ : Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.refl M)) S = S))) x✝ = ↑(toMap f) x✝
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
x y : M
⊢ OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } x *
      OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } y
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
x y : M
⊢ mk (x * y) 1 = mk x 1 * mk y 1
[PROOFSTEP]
rw [mk_mul, mul_one]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
y : { x // x ∈ S }
⊢ OneHom.toFun
        ↑{ toOneHom := { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : M),
                  OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } y) }
        ↑y *
      mk 1 y =
    1
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
y : { x // x ∈ S }
⊢ mk (↑y) 1 * mk 1 y = 1
[PROOFSTEP]
rw [mk_mul, mul_one, one_mul, mk_self]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
z : Localization S
x : M × { x // x ∈ S }
⊢ mk x.fst x.snd *
      OneHom.toFun
        ↑{ toOneHom := { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : M),
                  OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } x *
                      OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } y) }
        ↑x.snd =
    OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : M),
                OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } x *
                    OneHom.toFun { toFun := fun x => mk x 1, map_one' := (_ : mk 1 1 = 1) } y) })
      x.fst
[PROOFSTEP]
dsimp only
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
z : Localization S
x : M × { x // x ∈ S }
⊢ mk x.fst x.snd * mk (↑x.snd) 1 = mk x.fst 1
[PROOFSTEP]
rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
src✝ : M →* Con.Quotient (r S) := MonoidHom.comp (Con.mk' (r S)) (MonoidHom.inl M { x // x ∈ S })
x y : M
⊢ (∃ c, ↑c * (1 * x) = ↑c * (1 * y)) ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rw [one_mul, one_mul]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk x y * ↑(Submonoid.LocalizationMap.toMap (monoidOf S)) ↑y = ↑(Submonoid.LocalizationMap.toMap (monoidOf S)) x
[PROOFSTEP]
rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk x 1
[PROOFSTEP]
conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
| mk (x * ↑y) (1 * y) = mk x 1
[PROOFSTEP]
rhs; rw [← mul_one 1]; rw [← mul_one x]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
| mk (x * ↑y) (1 * y) = mk x 1
[PROOFSTEP]
rhs; rw [← mul_one 1]; rw [← mul_one x]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
| mk (x * ↑y) (1 * y) = mk x 1
[PROOFSTEP]
rhs
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
| mk x 1
[PROOFSTEP]
rw [← mul_one 1]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
| mk x (1 * 1)
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)
[PROOFSTEP]
exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Sort u
f : M → { x // x ∈ S } → p
H : ∀ {a c : M} {b d : { x // x ∈ S }}, ↑(r S) (a, b) (c, d) → f a b = f c d
a : M
b : { x // x ∈ S }
⊢ liftOn (Submonoid.LocalizationMap.mk' (monoidOf S) a b) f H = f a b
[PROOFSTEP]
rw [← mk_eq_monoidOf_mk', liftOn_mk]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Sort u_4
f : M → { x // x ∈ S } → M → { x // x ∈ S } → p
H :
  ∀ {a a' : M} {b b' : { x // x ∈ S }} {c c' : M} {d d' : { x // x ∈ S }},
    ↑(r S) (a, b) (a', b') → ↑(r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : { x // x ∈ S }
⊢ liftOn₂ (Submonoid.LocalizationMap.mk' (monoidOf S) a b) (Submonoid.LocalizationMap.mk' (monoidOf S) c d) f H =
    f a b c d
[PROOFSTEP]
rw [← mk_eq_monoidOf_mk', liftOn₂_mk]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(mulEquivOfQuotient f) (mk x y) = Submonoid.LocalizationMap.mk' f x y
[PROOFSTEP]
rw [mk_eq_monoidOf_mk'_apply]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(mulEquivOfQuotient f) (Submonoid.LocalizationMap.mk' (monoidOf S) x y) = Submonoid.LocalizationMap.mk' f x y
[PROOFSTEP]
exact mulEquivOfQuotient_mk' _ _
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
⊢ ↑(mulEquivOfQuotient f) (↑(Submonoid.LocalizationMap.toMap (monoidOf S)) x) = ↑(Submonoid.LocalizationMap.toMap f) x
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(MulEquiv.symm (mulEquivOfQuotient f)) (Submonoid.LocalizationMap.mk' f x y) = mk x y
[PROOFSTEP]
rw [mk_eq_monoidOf_mk'_apply]
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(MulEquiv.symm (mulEquivOfQuotient f)) (Submonoid.LocalizationMap.mk' f x y) =
    Submonoid.LocalizationMap.mk' (monoidOf S) x y
[PROOFSTEP]
exact mulEquivOfQuotient_symm_mk' _ _
[GOAL]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
x : { x // x ∈ S }
⊢ ↑(0, 1).snd * (0, x).fst = ↑(0, x).snd * (0, 1).fst
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
x : Localization S
y : M × { x // x ∈ S }
⊢ 0 * mk y.fst y.snd = 0
[PROOFSTEP]
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
x : Localization S
y : M × { x // x ∈ S }
⊢ mk y.fst y.snd * 0 = 0
[PROOFSTEP]
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
p : Type u_4
f : M → { x // x ∈ S } → p
H : ∀ {a c : M} {b d : { x // x ∈ S }}, ↑(r S) (a, b) (c, d) → f a b = f c d
⊢ liftOn 0 f H = f 0 1
[PROOFSTEP]
rw [← mk_zero 1, liftOn_mk]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationMap S N
⊢ ↑(toMap f) (sec f 0).fst = 0
[PROOFSTEP]
rw [LocalizationMap.sec_spec', mul_zero]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationWithZeroMap S N
g : M →*₀ P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
src✝ : N →* P := LocalizationMap.lift f.toLocalizationMap hg
⊢ OneHom.toFun (↑src✝) 0 = 0
[PROOFSTEP]
erw [LocalizationMap.lift_spec f.toLocalizationMap hg 0 0]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationWithZeroMap S N
g : M →*₀ P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
src✝ : N →* P := LocalizationMap.lift f.toLocalizationMap hg
⊢ ↑↑g (LocalizationMap.sec f.toLocalizationMap 0).fst = ↑↑g ↑(LocalizationMap.sec f.toLocalizationMap 0).snd * 0
[PROOFSTEP]
rw [mul_zero, ← map_zero g, ← g.toMonoidHom_coe]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationWithZeroMap S N
g : M →*₀ P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
src✝ : N →* P := LocalizationMap.lift f.toLocalizationMap hg
⊢ ↑↑g (LocalizationMap.sec f.toLocalizationMap 0).fst = OneHom.toFun (↑↑g) 0
[PROOFSTEP]
refine f.toLocalizationMap.eq_of_eq hg ?_
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationWithZeroMap S N
g : M →*₀ P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
src✝ : N →* P := LocalizationMap.lift f.toLocalizationMap hg
⊢ ↑(LocalizationMap.toMap f.toLocalizationMap) (LocalizationMap.sec f.toLocalizationMap 0).fst =
    ↑(LocalizationMap.toMap f.toLocalizationMap) 0
[PROOFSTEP]
rw [LocalizationMap.sec_zero_fst]
[GOAL]
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : LocalizationWithZeroMap S N
g : M →*₀ P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
src✝ : N →* P := LocalizationMap.lift f.toLocalizationMap hg
⊢ 0 = ↑(LocalizationMap.toMap f.toLocalizationMap) 0
[PROOFSTEP]
exact f.toMonoidWithZeroHom.map_zero.symm
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b : { x // x ∈ s }
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
⊢ c = d
[PROOFSTEP]
have : Nonempty s := One.nonempty
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b : { x // x ∈ s }
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
this : Nonempty { x // x ∈ s }
⊢ c = d
[PROOFSTEP]
simpa [-mk_eq_monoidOf_mk', mk_eq_mk_iff, r_iff_exists] using h
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
[PROOFSTEP]
have : Nonempty s := One.nonempty
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
this : Nonempty { x // x ∈ s }
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
[PROOFSTEP]
simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
obtain ⟨e, he⟩ := r_iff_exists.1 hab
[GOAL]
case intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e : { x // x ∈ s }
he : ↑e * (↑(b₁, b₂).snd * (a₁, a₂).fst) = ↑e * (↑(a₁, a₂).snd * (b₁, b₂).fst)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e : { x // x ∈ s }
he : ↑e * (↑(b₁, b₂).snd * (a₁, a₂).fst) = ↑e * (↑(a₁, a₂).snd * (b₁, b₂).fst)
f : { x // x ∈ s }
hf : ↑f * (↑(d₁, d₂).snd * (c₁, c₂).fst) = ↑f * (↑(c₁, c₂).snd * (d₁, d₂).fst)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
simp only [mul_right_inj] at he hf 
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e f : { x // x ∈ s }
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e f : { x // x ∈ s }
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁
[PROOFSTEP]
rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α), mul_le_mul_iff_right, ←
  mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm, mul_left_comm (b₂ : α), mul_le_mul_iff_left]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
obtain ⟨e, he⟩ := r_iff_exists.1 hab
[GOAL]
case intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e : { x // x ∈ s }
he : ↑e * (↑(b₁, b₂).snd * (a₁, a₂).fst) = ↑e * (↑(a₁, a₂).snd * (b₁, b₂).fst)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e : { x // x ∈ s }
he : ↑e * (↑(b₁, b₂).snd * (a₁, a₂).fst) = ↑e * (↑(a₁, a₂).snd * (b₁, b₂).fst)
f : { x // x ∈ s }
hf : ↑f * (↑(d₁, d₂).snd * (c₁, c₂).fst) = ↑f * (↑(c₁, c₂).snd * (d₁, d₂).fst)
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
simp only [mul_right_inj] at he hf 
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e f : { x // x ∈ s }
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) a₁ a₂ c₁ c₂ ↔ (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) b₁ b₂ d₁ d₂
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a b : Localization s
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
c₁ d₁ : α
c₂ d₂ : { x // x ∈ s }
hab : ↑(r s) (a₁, a₂) (b₁, b₂)
hcd : ↑(r s) (c₁, c₂) (d₁, d₂)
e f : { x // x ∈ s }
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁
[PROOFSTEP]
rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α), mul_lt_mul_iff_right, ←
  mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm, mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : mk a.fst a.snd ≤ mk b.fst b.snd
hbc : mk b.fst b.snd ≤ mk c.fst c.snd
⊢ mk a.fst a.snd ≤ mk c.fst c.snd
[PROOFSTEP]
simp only [mk_le_mk] at hab hbc ⊢
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
hbc : ↑c.snd * b.fst ≤ ↑b.snd * c.fst
⊢ ↑c.snd * a.fst ≤ ↑a.snd * c.fst
[PROOFSTEP]
refine' le_of_mul_le_mul_left' _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
hbc : ↑c.snd * b.fst ≤ ↑b.snd * c.fst
⊢ α
[PROOFSTEP]
exact ↑b.2
[GOAL]
case refine'_2
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
hbc : ↑c.snd * b.fst ≤ ↑b.snd * c.fst
⊢ ↑b.snd * (↑c.snd * a.fst) ≤ ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
rw [mul_left_comm]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
hbc : ↑c.snd * b.fst ≤ ↑b.snd * c.fst
⊢ ↑c.snd * (↑b.snd * a.fst) ≤ ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
refine' (mul_le_mul_left' hab _).trans _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
hbc : ↑c.snd * b.fst ≤ ↑b.snd * c.fst
⊢ ↑c.snd * (↑a.snd * b.fst) ≤ ↑b.snd * (↑a.snd * c.fst)
[PROOFSTEP]
rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
⊢ a ≤ b → b ≤ a → a = b
[PROOFSTEP]
induction' a using Localization.rec with a₁ a₂
[GOAL]
case f
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
⊢ mk a₁ a₂ ≤ b → b ≤ mk a₁ a₂ → mk a₁ a₂ = b
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
induction' b using Localization.rec with b₁ b₂
[GOAL]
case f.f
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a₁ : α
a₂ : { x // x ∈ s }
b₁ : α
b₂ : { x // x ∈ s }
⊢ mk a₁ a₂ ≤ mk b₁ b₂ → mk b₁ b₂ ≤ mk a₁ a₂ → mk a₁ a₂ = mk b₁ b₂
case f.H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝) =
    (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝)
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
[GOAL]
case f.f
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a₁ : α
a₂ : { x // x ∈ s }
b₁ : α
b₂ : { x // x ∈ s }
⊢ ↑b₂ * a₁ ≤ ↑a₂ * b₁ → ↑a₂ * b₁ ≤ ↑b₂ * a₁ → ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
case f.H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝) =
    (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝)
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : { x // x ∈ s }
a₁ : α
a₂ : { x // x ∈ s }
b₁ : α
b₂ : { x // x ∈ s }
hab : ↑b₂ * a₁ ≤ ↑a₂ * b₁
hba : ↑a₂ * b₁ ≤ ↑b₂ * a₁
⊢ ↑1 * (↑b₂ * a₁) = ↑1 * (↑a₂ * b₁)
[PROOFSTEP]
rw [hab.antisymm hba]
[GOAL]
case f.H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝) =
    (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝)
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
all_goals intros; rfl
[GOAL]
case f.H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝) =
    (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝)
[PROOFSTEP]
intros
[GOAL]
case f.H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁✝ b₁ : α
a₂✝ b₂ : { x // x ∈ s }
b : Localization s
a₁ : α
a₂ : { x // x ∈ s }
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝) =
    (_ : mk a₁ a₂ ≤ mk c✝ d✝ → mk c✝ d✝ ≤ mk a₁ a₂ → mk a₁ a₂ = mk c✝ d✝)
[PROOFSTEP]
rfl
[GOAL]
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
intros
[GOAL]
case H
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
a b : Localization s
a✝ c✝ : α
b✝ d✝ : { x // x ∈ s }
h✝ : ↑(r s) (a✝, b✝) (c✝, d✝)
⊢ (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b) = (_ : mk c✝ d✝ ≤ b → b ≤ mk c✝ d✝ → mk c✝ d✝ = b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
src✝¹ : CommMonoid (Localization s) := commMonoid s
src✝ : PartialOrder (Localization s) := partialOrder
a✝ b✝ : Localization s
a b : α × { x // x ∈ s }
hab : mk a.fst a.snd ≤ mk b.fst b.snd
c✝ : Localization s
c : α × { x // x ∈ s }
⊢ mk c.fst c.snd * mk a.fst a.snd ≤ mk c.fst c.snd * mk b.fst b.snd
[PROOFSTEP]
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ c.1] at hab ⊢
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
src✝¹ : CommMonoid (Localization s) := commMonoid s
src✝ : PartialOrder (Localization s) := partialOrder
a✝ b✝ : Localization s
a b : α × { x // x ∈ s }
c✝ : Localization s
c : α × { x // x ∈ s }
hab : ↑b.snd * a.fst ≤ ↑a.snd * b.fst
⊢ ↑c.snd * c.fst * (↑b.snd * a.fst) ≤ ↑c.snd * c.fst * (↑a.snd * b.fst)
[PROOFSTEP]
exact mul_le_mul_left' hab _
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
src✝¹ : CommMonoid (Localization s) := commMonoid s
src✝ : PartialOrder (Localization s) := partialOrder
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : mk a.fst a.snd * mk b.fst b.snd ≤ mk a.fst a.snd * mk c.fst c.snd
⊢ mk b.fst b.snd ≤ mk c.fst c.snd
[PROOFSTEP]
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : { x // x ∈ s }
src✝¹ : CommMonoid (Localization s) := commMonoid s
src✝ : PartialOrder (Localization s) := partialOrder
a✝ b✝ c✝ : Localization s
a b c : α × { x // x ∈ s }
hab : ↑a.snd * a.fst * (↑c.snd * b.fst) ≤ ↑a.snd * a.fst * (↑b.snd * c.fst)
⊢ ↑c.snd * b.fst ≤ ↑b.snd * c.fst
[PROOFSTEP]
exact le_of_mul_le_mul_left' hab
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b✝ : { x // x ∈ s }
a b : α
⊢ ↑{ toFun := fun a => mk a b✝, inj' := (_ : Injective fun a => mk a b✝) } a ≤
      ↑{ toFun := fun a => mk a b✝, inj' := (_ : Injective fun a => mk a b✝) } b ↔
    a ≤ b
[PROOFSTEP]
simp [-mk_eq_monoidOf_mk', mk_le_mk]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCancelCommMonoid α
s : Submonoid α
src✝ : OrderedCancelCommMonoid (Localization s) := orderedCancelCommMonoid
a b : Localization s
x✝¹ x✝ : α × { x // x ∈ s }
⊢ mk x✝¹.fst x✝¹.snd ≤ mk x✝.fst x✝.snd ∨ mk x✝.fst x✝.snd ≤ mk x✝¹.fst x✝¹.snd
[PROOFSTEP]
simp_rw [mk_le_mk]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCancelCommMonoid α
s : Submonoid α
src✝ : OrderedCancelCommMonoid (Localization s) := orderedCancelCommMonoid
a b : Localization s
x✝¹ x✝ : α × { x // x ∈ s }
⊢ ↑x✝.snd * x✝¹.fst ≤ ↑x✝¹.snd * x✝.fst ∨ ↑x✝¹.snd * x✝.fst ≤ ↑x✝.snd * x✝¹.fst
[PROOFSTEP]
exact le_total _ _
