-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.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
asIdeal :
  1 ⊗ₜ[R] s ∈ q.asIdeal ↔
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (PrimeSpectrum.asIdeal
        ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
            {
              asIdeal :=
                RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift
                        (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                        (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                      p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
              isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
          ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
              Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                Membership.mem (γ := Set (PrimeSpectrum S))
                  (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                (comap (AlgHom.toRingHom includeRight) q) ⋯)
            q)))
      (1 ⊗ₜ[R] s)
asIdeal₁ : ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉ q.asIdeal
asIdeal₂ :
  ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    PrimeSpectrum.asIdeal
      ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
          {
            asIdeal :=
              RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift
                      (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                    p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
            isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
        ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
            Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
              Membership.mem (γ := Set (PrimeSpectrum S))
                (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
              (comap (AlgHom.toRingHom includeRight) q) ⋯)
          q))
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (PrimeSpectrum.asIdeal
        ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
            {
              asIdeal :=
                RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift
                        (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                        (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                      p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
              isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
          ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
              Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                Membership.mem (γ := Set (PrimeSpectrum S))
                  (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                (comap (AlgHom.toRingHom includeRight) q) ⋯)
            q)))
      x ↔
    x ∈ q.asIdeal

Tactic:
rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), iff_comm,
      ← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e]

Premises used: iff_comm, Algebra.smul_def, Ideal.IsPrime.mul_mem_left_iff