case intro.mk.mk
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
s : S
x y : R
hy : y ∈ M
H :
  s * ↑(algebraMap R S) ↑(x, { val := y, property := hy }).snd = ↑(algebraMap R S) (x, { val := y, property := hy }).fst
⊢ ∃ x, s * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
s : S
⊢ ∃ x, s * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
obtain ⟨⟨x, y, hy⟩, H⟩ := IsLocalization.surj M s
no goals
case intro.mk.mk
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
s : S
x y : R
hy : y ∈ M
H :
  s * ↑(algebraMap R S) ↑(x, { val := y, property := hy }).snd = ↑(algebraMap R S) (x, { val := y, property := hy }).fst
⊢ ∃ x, s * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
exact ⟨⟨x, y, h₁ hy⟩, H⟩
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ↑(algebraMap R S) x = ↑(algebraMap R S) y
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y ↔ ∃ c, ↑c * x = ↑c * y
constructor
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
rw [IsLocalization.eq_iff_exists M]
case mp.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
c : { x // x ∈ M }
hc : ↑c * x = ↑c * y
⊢ ∃ c, ↑c * x = ↑c * y
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
rintro ⟨c, hc⟩
no goals
case mp.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
c : { x // x ∈ M }
hc : ↑c * x = ↑c * y
⊢ ∃ c, ↑c * x = ↑c * y
exact ⟨⟨c, h₁ c.2⟩, hc⟩
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
c : { x // x ∈ N }
h : ↑c * x = ↑c * y
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y
case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ↑(algebraMap R S) x = ↑(algebraMap R S) y
rintro ⟨c, h⟩
no goals
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.125264
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ (r : R), r ∈ N → IsUnit (↑(algebraMap R S) r)
x y : R
c : { x // x ∈ N }
h : ↑c * x = ↑c * y
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y
simpa only [map_mul, (h₂ c c.2).mul_right_inj] using
  congr_arg (algebraMap R S) h