-- Mathlib/RingTheory/Presentation.lean
lemma _root_.Algebra.Generators.ker_localizationAway :
    (Generators.localizationAway (S := S) r).ker = Ideal.span { C r * X () - 1 }

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) =
    Ideal.span {C r * X () - 1}

Tactic:
erw [← RingHom.comap_ker]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})))
      (RingHom.ker (↑(mvPolynomialQuotientEquiv S r)).toRingHom) =
    Ideal.span {C r * X () - 1}

Proof state:
case hf
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : (Generators.localizationAway r).vars
⊢ invSelf r = (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x))

Tactic:
rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))

Tactic:
ext x

Result:
case hf
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : (Generators.localizationAway r).vars
⊢ (aeval (Generators.localizationAway r).val) (X x) =
    ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (X x)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})))
      (RingHom.ker (↑(mvPolynomialQuotientEquiv S r)).toRingHom) =
    Ideal.span {C r * X () - 1}

Tactic:
simp only [Generators.localizationAway_vars, AlgEquiv.toAlgHom_eq_coe, AlgHom.toRingHom_eq_coe,
  AlgEquiv.toAlgHom_toRingHom]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker ↑(mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}

Proof state:
case hf
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : (Generators.localizationAway r).vars
⊢ (aeval (Generators.localizationAway r).val) (X x) =
    ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (X x)

Tactic:
simp only [Generators.localizationAway_vars, aeval_X, Generators.localizationAway_val,
  AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, Ideal.Quotient.mkₐ_eq_mk,
  Function.comp_apply]

Result:
case hf
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : (Generators.localizationAway r).vars
⊢ invSelf r = (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker (mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}

Tactic:
simp [RingHom.ker_equiv, ← RingHom.ker_eq_comap_bot]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker ↑(mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}

Tactic:
show Ideal.comap _ (RingHom.ker (mvPolynomialQuotientEquiv S r)) = Ideal.span {C r * X () - 1}

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker (mvPolynomialQuotientEquiv S r)) =
    Ideal.span {C r * X () - 1}

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (Generators.localizationAway r).ker = Ideal.span {C r * X () - 1}

Tactic:
have : aeval (S₁ := S) (Generators.localizationAway r).val =
    (mvPolynomialQuotientEquiv S r).toAlgHom.comp
      (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})) := by
  ext x
  simp only [Generators.localizationAway_vars, aeval_X, Generators.localizationAway_val,
    AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, Ideal.Quotient.mkₐ_eq_mk,
    Function.comp_apply]
  rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ (Generators.localizationAway r).ker = Ideal.span {C r * X () - 1}

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ (Generators.localizationAway r).ker = Ideal.span {C r * X () - 1}

Tactic:
rw [Generators.ker_eq_ker_aeval_val, this]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) =
    Ideal.span {C r * X () - 1}