Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ x ∈ q.asIdeal ↔
    (algebraMap R (p.asIdeal.Fiber S)) r * x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

Tactic:
← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r),

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r * x ∈ q.asIdeal ↔
    (algebraMap R (p.asIdeal.Fiber S)) r * x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal