Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver p Q'
hsQ'' : (algebraMap R Q'.ResidueField) s ≠ 0
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q'.ResidueField) (IsScalarTower.toAlgHom R S Q'.ResidueField) ⋯
⊢ t ∈ Q'

Tactic:
have H : φ' r = 0 := (hr (α ⟨Q', ⟨‹_›, ‹_›⟩⟩).asIdeal inferInstance (by
        rwa [ne_eq, ← PrimeSpectrum.ext_iff, EmbeddingLike.apply_eq_iff_eq, Subtype.mk.injEq]) :)

Goal state after:
case refine_2
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H✝ : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver p Q'
hsQ'' : (algebraMap R Q'.ResidueField) s ≠ 0
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q'.ResidueField) (IsScalarTower.toAlgHom R S Q'.ResidueField) ⋯
H : φ' r = 0
⊢ t ∈ Q'