Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case neg
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
R'' : Type u
inst✝¹⁰ : CommRing R''
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R R''
inst✝⁷ : IsScalarTower R R' R''
inst✝⁶ : Etale R' R''
Q : Ideal R''
inst✝⁵ : Q.IsPrime
inst✝⁴ : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝³ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝² : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝² : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝¹ : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
⊢ e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin (n + 1)), e' i.castSucc ∉ P'' → P'' = Fin.cons (↑P'φ) Q' i

Tactic:
have : ∀ i ≠ 0, e' i ∈ P'' := by
        intro j hj
        rw [← Ideal.IsPrime.mul_mem_left_iff (I := P'') heP'']
        simp [φ, ← he'0, he'.ortho hj.symm]

Goal state after:
case neg
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
R'' : Type u
inst✝¹⁰ : CommRing R''
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R R''
inst✝⁷ : IsScalarTower R R' R''
inst✝⁶ : Etale R' R''
Q : Ideal R''
inst✝⁵ : Q.IsPrime
inst✝⁴ : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝³ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝² : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝³ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝² : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝¹ : (↑P'φ).LiesOver P
this✝ : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
this : ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''
⊢ e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin (n + 1)), e' i.castSucc ∉ P'' → P'' = Fin.cons (↑P'φ) Q' i