Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case add
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : 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)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap 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)).toRingHom xa =
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ ma * a
xb : R' ⊗[R] R''
mb : ℕ
eb :
  (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom xb =
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ mb * b
⊢ ∃ b_1 m,
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom b_1 =
      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ m * (a + b)

Tactic:
refine ⟨(e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb, ma + mb, ?_⟩

Goal state after:
case add
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : 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)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap 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)).toRingHom xa =
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ ma * a
xb : R' ⊗[R] R''
mb : ℕ
eb :
  (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom xb =
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ mb * b
⊢ (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom
      ((e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb) =
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ (ma + mb) *
      (a + b)