case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
⊢ IsUnit (↑(algebraMap R S) ↑y)
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
⊢ IsUnit (↑(algebraMap R S) ↑y)
obtain ⟨m, hm⟩ := h' y
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) ↑{ val := m * ↑y, property := hm })
⊢ IsUnit (↑(algebraMap R S) ↑y)
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
⊢ IsUnit (↑(algebraMap R S) ↑y)
have := IsLocalization.map_units S ⟨_, hm⟩
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) m * ↑(algebraMap R S) ↑y)
⊢ IsUnit (↑(algebraMap R S) ↑y)
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) ↑{ val := m * ↑y, property := hm })
⊢ IsUnit (↑(algebraMap R S) ↑y)
erw [map_mul] at this
no goals
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) m * ↑(algebraMap R S) ↑y)
⊢ IsUnit (↑(algebraMap R S) ↑y)
exact (IsUnit.mul_iff.mp this).2
case intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
z : S
y : R
s : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
z : S
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
no goals
case intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
z : S
y : R
s : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
exact ⟨⟨y, _, h s.prop⟩, e⟩
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ ↑(algebraMap R S) x✝¹ = ↑(algebraMap R S) x✝ ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝
rw [IsLocalization.eq_iff_exists M]
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝
refine ⟨fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩, ?_⟩
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝
rintro ⟨x, h⟩
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
case intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
obtain ⟨m, hm⟩ := h' x
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ↑{ val := m * ↑x, property := hm } * x✝¹ = ↑{ val := m * ↑x, property := hm } * x✝
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
refine ⟨⟨_, hm⟩, ?_⟩
no goals
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.656657
inst✝³ : CommRing P
N✝ : Submonoid S
T : Type ?u.656821
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ↑{ val := m * ↑x, property := hm } * x✝¹ = ↑{ val := m * ↑x, property := hm } * x✝
simp [h, mul_assoc]