-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePair R
refine_2 :
  IsUnit (M :=
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
            Localization.Away P.g))))
    ((algebraMap (Localization.Away P.g)
            (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
              (Ideal.span
                (singleton (α := Localization.Away P.g)
                  ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                    Localization.Away P.g)))) :
          (a : Localization.Away P.g) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.g) :
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))
⊢ IsUnit (M :=
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
            Localization.Away P.g))))
    (((aeval
              ((algebraMap R[X]
                    (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                      (Ideal.span
                        (singleton (α := Localization.Away P.g)
                          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                            Localization.Away P.g)))) :
                  (a : R[X]) →
                    Localization.Away P.g ⧸
                      Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
                X) :
            R[X] →ₐ[R]
              HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                (Ideal.span
                  (singleton (α := Localization.Away P.g)
                    ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                      Localization.Away P.g)))) :
          (a : R[X]) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        P.g :
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))

Tactic:
rw [aeval_algebraMap_apply, IsScalarTower.algebraMap_apply _ (Localization.Away P.g) (_ ⧸ _),
      aeval_X_left_apply]

Premises used: Polynomial.aeval_X_left_apply, Localization.Away, HasQuotient.Quotient, StandardEtalePair.g, IsScalarTower.algebraMap_apply, Polynomial.aeval_algebraMap_apply