-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
a b : R' ⊗[R] S
xa : R' ⊗[R] R''
ma : ℕ
ea :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      xa =
    HPow.hPow (α := R' ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              (a : R' ⊗[R] R'') → R' ⊗[R] S)
            (e₀ * 1 ⊗ₜ[R] g) :
          R' ⊗[R] S)
        ma *
      a
xb : R' ⊗[R] R''
mb : ℕ
eb :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      xb =
    HPow.hPow (α := R' ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              (a : R' ⊗[R] R'') → R' ⊗[R] S)
            (e₀ * 1 ⊗ₜ[R] g) :
          R' ⊗[R] S)
        mb *
      b
H₁ :
  HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
            (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                e₀ :
              R' ⊗[R] S)
            (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
          mb *
        (HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
              (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                    (a : R' ⊗[R] R'') → R' ⊗[R] S)
                  e₀ :
                R' ⊗[R] S)
              (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
            ma *
          a) +
      HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
            (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                e₀ :
              R' ⊗[R] S)
            (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
          ma *
        (HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
              (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                    (a : R' ⊗[R] R'') → R' ⊗[R] S)
                  e₀ :
                R' ⊗[R] S)
              (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
            mb *
          b) =
    HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
            (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                e₀ :
              R' ⊗[R] S)
            (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
          ma *
        HMul.hMul (α := R' ⊗[R] S) (β := R' ⊗[R] S)
            (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                e₀ :
              R' ⊗[R] S)
            (1 ⊗ₜ[R] (IsScalarTower.toAlgHom R R'' S : (a : R'') → S) g : R' ⊗[R] S) ^
          mb *
      (a + b)
⊢ ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      ((e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb) =
    HPow.hPow (α := R' ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              (a : R' ⊗[R] R'') → R' ⊗[R] S)
            (e₀ * 1 ⊗ₜ[R] g) :
          R' ⊗[R] S)
        (ma + mb) *
      (a + b)

Tactic:
simp only [map_add, map_mul, map_pow, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        ea, eb, pow_add]

Premises used: AlgHom.coe_id, Algebra.TensorProduct.map_tmul, pow_add, map_add, map_pow, map_mul, id_eq