case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap R P) ↑y)

case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst

case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ {x y : R}, ↑(algebraMap R P) x = ↑(algebraMap R P) y ↔ ∃ c, ↑c * x = ↑c * y
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ IsLocalization M P
constructor
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap R P) ↑y)
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap R P) ↑y)
intro y
case h.e'_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : { x // x ∈ M }
⊢ ↑(algebraMap R P) ↑y = ↑↑↑↑h (↑(algebraMap R S) ↑y)
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap R P) ↑y)
convert (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom
no goals
case h.e'_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : { x // x ∈ M }
⊢ ↑(algebraMap R P) ↑y = ↑↑↑↑h (↑(algebraMap R S) ↑y)
exact (h.commutes y).symm
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
intro y
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e : ↑(AlgEquiv.symm h) y * ↑(algebraMap R ((fun x => S) y)) ↑(x, s).snd = ↑(algebraMap R ((fun x => S) y)) (x, s).fst
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e :
  (let_fun this := ↑h;
      this)
      (↑(AlgEquiv.symm h) y * ↑(algebraMap R ((fun x => S) y)) ↑(x, s).snd) =
    (let_fun this := ↑h;
      this)
      (↑(algebraMap R ((fun x => S) y)) (x, s).fst)
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e : ↑(AlgEquiv.symm h) y * ↑(algebraMap R ((fun x => S) y)) ↑(x, s).snd = ↑(algebraMap R ((fun x => S) y)) (x, s).fst
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
apply_fun (show S → P from h) at e
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e : y * ↑(algebraMap R P) ↑s = ↑(algebraMap R P) x
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e :
  (let_fun this := ↑h;
      this)
      (↑(AlgEquiv.symm h) y * ↑(algebraMap R ((fun x => S) y)) ↑(x, s).snd) =
    (let_fun this := ↑h;
      this)
      (↑(algebraMap R ((fun x => S) y)) (x, s).fst)
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
simp only [h.map_mul, h.apply_symm_apply, h.commutes] at e
no goals
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : { x // x ∈ M }
e : y * ↑(algebraMap R P) ↑s = ↑(algebraMap R P) x
⊢ ∃ x, y * ↑(algebraMap R P) ↑x.snd = ↑(algebraMap R P) x.fst
exact ⟨⟨x, s⟩, e⟩
case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ ↑(algebraMap R P) x = ↑(algebraMap R P) y ↔ ∃ c, ↑c * x = ↑c * y
case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ {x y : R}, ↑(algebraMap R P) x = ↑(algebraMap R P) y ↔ ∃ c, ↑c * x = ↑c * y
intro x y
case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ ↑(AlgEquiv.symm h).toEquiv (↑(algebraMap R P) x) = ↑(AlgEquiv.symm h).toEquiv (↑(algebraMap R P) y) ↔
    ↑(AlgEquiv.symm h) (↑(algebraMap R P) x) = ↑(AlgEquiv.symm h) (↑(algebraMap R P) y)
case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ ↑(algebraMap R P) x = ↑(algebraMap R P) y ↔ ∃ c, ↑c * x = ↑c * y
rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
  h.symm.commutes]
no goals
case eq_iff_exists'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ ↑(AlgEquiv.symm h).toEquiv (↑(algebraMap R P) x) = ↑(AlgEquiv.symm h).toEquiv (↑(algebraMap R P) y) ↔
    ↑(AlgEquiv.symm h) (↑(algebraMap R P) x) = ↑(AlgEquiv.symm h) (↑(algebraMap R P) y)
rfl