-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
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
⊢ 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
have 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) sorry)
                    (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) sorry :
                  p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
          isPrime := sorry : 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) sorry)
        q))
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]