case mk.intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
n : ℕ
⊢ IsUnit
    (↑(algebraMap R S)
      ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) })
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
⊢ ∀ (y : { x // x ∈ Submonoid.powers r }), IsUnit (↑(algebraMap R S) ↑y)
rintro ⟨_, n, rfl⟩
no goals
case mk.intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
n : ℕ
⊢ IsUnit
    (↑(algebraMap R S)
      ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) })
exact (algebraMap R S).isUnit_map (hr.pow _)
case intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z' : R
⊢ ∃ x, ↑(algebraMap R S) z' * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z : S
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
obtain ⟨z', rfl⟩ := H.2 z
no goals
case intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z' : R
⊢ ∃ x, ↑(algebraMap R S) z' * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
exact ⟨⟨z', 1⟩, by simp⟩
no goals
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z' : R
⊢ ↑(algebraMap R S) z' * ↑(algebraMap R S) ↑(z', 1).snd = ↑(algebraMap R S) (z', 1).fst
simp
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y ↔ ∃ c, ↑c * x = ↑c * y
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y ↔ ∃ c, ↑c * x = ↑c * y
erw [H.1.eq_iff]
case mp
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y → ∃ c, ↑c * x = ↑c * y

case mpr
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → x = y
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y ↔ ∃ c, ↑c * x = ↑c * y
constructor
case mp
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x : R
⊢ ∃ c, ↑c * x = ↑c * x
case mp
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y → ∃ c, ↑c * x = ↑c * y
rintro rfl
no goals
case mp
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x : R
⊢ ∃ c, ↑c * x = ↑c * x
exact ⟨1, rfl⟩
case mpr.intro.mk.intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      y
⊢ x = y
case mpr
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → x = y
rintro ⟨⟨_, n, rfl⟩, e⟩
no goals
case mpr.intro.mk.intro
R✝ : Type ?u.305976
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type ?u.306165
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type ?u.306345
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      y
⊢ x = y
exact (hr.pow _).mul_right_inj.mp e