Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
x✝ : R
⊢ ((((Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
                ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField)
                    ⋯)).comp
            TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝ =
    (((algebraMap (p.Fiber S) q'.ResidueField).comp TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝

pp: case h₂
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
x✝ : S
⊢ (((Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
            ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField)
                ⋯)).comp
        TensorProduct.includeRight.toRingHom)
      x✝ =
    ((algebraMap (p.Fiber S) q'.ResidueField).comp TensorProduct.includeRight.toRingHom) x✝

Tactic:
<;>

Goal state after:
case h₁
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
x✝ : R
⊢ ((((Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
                ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField)
                    ⋯)).comp
            TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝ =
    (((algebraMap (p.Fiber S) q'.ResidueField).comp TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝

case h₂
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
x✝ : S
⊢ (((Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
            ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField)
                ⋯)).comp
        TensorProduct.includeRight.toRingHom)
      x✝ =
    ((algebraMap (p.Fiber S) q'.ResidueField).comp TensorProduct.includeRight.toRingHom) x✝