Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case h.succ
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝² : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
n✝ : ℕ
IH :
  ∀ m < n✝ + 1,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = n✝ + 1
q : Ideal S
hq : q.IsPrime
hq' : q.LiesOver p
R' : Type u
w✝¹³ : CommRing R'
w✝¹² : Algebra R R'
w✝¹¹ : Etale R R'
P : Ideal R'
w✝¹⁰ : P.IsPrime
w✝⁹ : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
P' : Ideal (R' ⊗[R] S)
w✝⁸ : P'.IsPrime
w✝⁷ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
left✝ : Module.Finite R' (Localization.Away e)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
this✝¹ : (P.primesOver (R' ⊗[R] S ⧸ Ideal.span {e})).ncard < n✝ + 1
R'' : Type u
w✝⁶ : CommRing R''
w✝⁵ : Algebra R' R''
w✝⁴ : Etale R' R''
Q : Ideal R''
w✝³ : Q.IsPrime
w✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1) → R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})
he' : CompleteOrthogonalIdempotents e'
Q' : Fin n → Ideal (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))
w✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
w✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))),
    P''.IsPrime → P''.LiesOver Q → e' (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e' i.castSucc ∉ P'' → P'' = Q' i
this✝ : Algebra R R'' := compHom R'' (algebraMap R R')
this : IsScalarTower R R' R''
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
e₁ : R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[R''] R'' ⊗[R] S ⧸ Ideal.span {φ e} := tensorQuotientTensorEquiv R'' e
e'' : Fin (n + 1) → R'' ⊗[R] S
he'' : CompleteOrthogonalIdempotents fun t ↦ Option.rec (φ e) e'' t
he''e' : ⇑e₁ ∘ e' = ⇑(Ideal.Quotient.mk (Ideal.span {φ e})) ∘ e''
he''e'' : ∀ (i : Fin (n + 1)), e₁ (e' i) = (Ideal.Quotient.mk (Ideal.span {φ e})) (e'' i)
hψe'' : ∀ (i : Fin (n + 1)), e' i = e₁.symm ((Ideal.Quotient.mk (Ideal.span {φ e})) (e'' i))
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (R' ⊗[R] S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

Tactic:
refine exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq_aux p q R' P e P'
      hP'q heP' hpP (fun P'' h₁ h₂ heP'' ↦ H P'' h₁ h₂ heP'') R'' Q n _
      ((CompleteOrthogonalIdempotents.equiv (finSuccEquiv _)).mpr he'') rfl
      (Q' · |>.comap (e₁.symm.toAlgHom.comp (Ideal.Quotient.mkₐ _ _))) hPQ
      (fun i ↦ by rw [Function.comp_def]; simpa [← hψe''] using hQ' i) ?_

Goal state after:
case h.succ
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝² : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
n✝ : ℕ
IH :
  ∀ m < n✝ + 1,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = n✝ + 1
q : Ideal S
hq : q.IsPrime
hq' : q.LiesOver p
R' : Type u
w✝¹³ : CommRing R'
w✝¹² : Algebra R R'
w✝¹¹ : Etale R R'
P : Ideal R'
w✝¹⁰ : P.IsPrime
w✝⁹ : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
P' : Ideal (R' ⊗[R] S)
w✝⁸ : P'.IsPrime
w✝⁷ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
left✝ : Module.Finite R' (Localization.Away e)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
this✝¹ : (P.primesOver (R' ⊗[R] S ⧸ Ideal.span {e})).ncard < n✝ + 1
R'' : Type u
w✝⁶ : CommRing R''
w✝⁵ : Algebra R' R''
w✝⁴ : Etale R' R''
Q : Ideal R''
w✝³ : Q.IsPrime
w✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1) → R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})
he' : CompleteOrthogonalIdempotents e'
Q' : Fin n → Ideal (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))
w✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
w✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))),
    P''.IsPrime → P''.LiesOver Q → e' (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e' i.castSucc ∉ P'' → P'' = Q' i
this✝ : Algebra R R'' := compHom R'' (algebraMap R R')
this : IsScalarTower R R' R''
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
e₁ : R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[R''] R'' ⊗[R] S ⧸ Ideal.span {φ e} := tensorQuotientTensorEquiv R'' e
e'' : Fin (n + 1) → R'' ⊗[R] S
he'' : CompleteOrthogonalIdempotents fun t ↦ Option.rec (φ e) e'' t
he''e' : ⇑e₁ ∘ e' = ⇑(Ideal.Quotient.mk (Ideal.span {φ e})) ∘ e''
he''e'' : ∀ (i : Fin (n + 1)), e₁ (e' i) = (Ideal.Quotient.mk (Ideal.span {φ e})) (e'' i)
hψe'' : ∀ (i : Fin (n + 1)), e' i = e₁.symm ((Ideal.Quotient.mk (Ideal.span {φ e})) (e'' i))
⊢ ∀ (P'' : Ideal (R'' ⊗[R] S)),
    ((fun t ↦ Option.rec (φ e) e'' t) ∘ ⇑(finSuccEquiv (n + 1))) 0 ∈ P'' →
      P''.IsPrime →
        P''.LiesOver Q →
          ((fun t ↦ Option.rec (φ e) e'' t) ∘ ⇑(finSuccEquiv (n + 1))) (Fin.last (n + 1)) ∈ P'' ∧
            ∀ (i : Fin n),
              ((fun t ↦ Option.rec (φ e) e'' t) ∘ ⇑(finSuccEquiv (n + 1))) i.succ.castSucc ∉ P'' →
                P'' = Ideal.comap ((↑e₁.symm).comp (Ideal.Quotient.mkₐ R'' (Ideal.span {φ e}))) (Q' i)