-- Mathlib/RingTheory/MvPolynomial/Localization.lean
private lemma auxInv_auxHom : (auxInv S r).comp (auxHom (S := S) r).toRingHom = RingHom.id _

Proof state:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ (IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom =
    RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})

Tactic:
rw [← RingHom.cancel_right (Ideal.Quotient.mk_surjective)]

Result:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) =
    (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))

Proof state:
case hC.a
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ ((((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
            (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp
        C)
      x =
    (((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
            (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp
        C)
      x

Tactic:
simp [auxInv]

Result:
no goals

Proof state:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x) =
    ((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x)

Tactic:
simp only [auxInv, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
  Function.comp_apply, auxHom_mk, aeval_X, RingHomCompTriple.comp_eq]

Result:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (lift r ⋯) (invSelf r) = (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Proof state:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C) 1 =
    ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C) ↑⟨r, ⋯⟩ *
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Tactic:
simp only [map_one, RingHom.coe_comp, Function.comp_apply]

Result:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ 1 = (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Proof state:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ 1 = (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Tactic:
rw [← map_one (Ideal.Quotient.mk _), ← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem,
  ← Ideal.neg_mem_iff, neg_sub]

Result:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ C r * X x - 1 ∈ Ideal.span {C r * X () - 1}

Proof state:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) =
    (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))

Tactic:
ext x

Result:
case hC.a
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ ((((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
            (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp
        C)
      x =
    (((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
            (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp
        C)
      x

case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x) =
    ((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x)

Proof state:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (lift r ⋯) (invSelf r) = (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Tactic:
erw [IsLocalization.lift_mk'_spec]

Result:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C) 1 =
    ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C) ↑⟨r, ⋯⟩ *
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Proof state:
case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ C r * X x - 1 ∈ Ideal.span {C r * X () - 1}

Tactic:
exact Ideal.mem_span_singleton_self (C r * X x - 1)

Result:
no goals