awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ideal R
inst_3 : p.IsPrime
x : p.Fiber S
⊢ ∃ r ∉ p, ∃ (s : S), r • x = 1 ⊗ₜ[R] s
have obtain : ∀ (r : R) (hr : r ∉ p) (s : S)
  (e :
    HSMul.hSMul (β := S ⊗[R] p.ResidueField) r
        ((Algebra.TensorProduct.comm R p.ResidueField S : (a : p.ResidueField ⊗[R] S) → S ⊗[R] p.ResidueField) x :
          S ⊗[R] p.ResidueField) =
      s ⊗ₜ[R] 1),
  ∃ r ∉ p, ∃ (s : S), r • x = 1 ⊗ₜ[R] s
Tactic: obtain ⟨r, hr, s, e⟩ := Ideal.ResidueField.exists_smul_eq_tmul_one _
    (Algebra.TensorProduct.comm _ _ _ x)
-- 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 : Ideal R
inst_3 : p.IsPrime
⊢ Eq.{u_2 + 1} (α := Ideal (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (Ideal.map (R := Localization (M := R) p.primeCompl) (F :=
      RingHom.{u_1, u_2} (Localization (M := R) p.primeCompl)
        (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
      (algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl)))
    (Ideal.map (R := S ⊗[R] Localization.AtPrime p) (F :=
      S ⊗[R] Localization.AtPrime p →+* Localization (M := S) (algebraMapSubmonoid S p.primeCompl))
      (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
        S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
      (Ideal.map (R := Localization.AtPrime p) (F := Localization.AtPrime p →ₐ[R] S ⊗[R] Localization.AtPrime p)
        includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p))))
have rw : Eq.{u_2 + 1} (α := Ideal (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
  (Ideal.map (R := Localization (M := R) p.primeCompl) (F :=
    RingHom.{u_1, u_2} (Localization (M := R) p.primeCompl)
      (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl)))
  (Ideal.map (R := Localization.AtPrime p) (F :=
    RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
        S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
      (↑includeRight : Localization.AtPrime p →+* S ⊗[R] Localization.AtPrime p))
    (IsLocalRing.maximalIdeal (Localization.AtPrime p)))
Tactic: rw [← Ideal.map_coe includeRight, Ideal.map_map]
-- 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 : Ideal R
inst_3 : p.IsPrime
⊢ Eq.{u_2 + 1} (α := Ideal (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (Ideal.map (R := Localization (M := R) p.primeCompl) (F :=
      RingHom.{u_1, u_2} (Localization (M := R) p.primeCompl)
        (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
      (algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl)))
    (Ideal.map (R := Localization.AtPrime p) (F :=
      RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
          S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
        (↑includeRight : Localization.AtPrime p →+* S ⊗[R] Localization.AtPrime p))
      (IsLocalRing.maximalIdeal (Localization.AtPrime p)))
have e_f : Eq (α :=
  RingHom.{u_1, u_2} (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
  (algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
      S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
    (↑includeRight : Localization.AtPrime p →+* S ⊗[R] Localization.AtPrime p))
Tactic: congr
-- 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 : Ideal R
inst_3 : p.IsPrime
⊢ Eq (α :=
    RingHom.{u_1, u_2} (Localization (M := R) p.primeCompl)
      (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
        S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
      (↑includeRight : Localization.AtPrime p →+* S ⊗[R] Localization.AtPrime p))
have e_f : ∀ (x : Localization (M := R) p.primeCompl),
  Eq.{u_2 + 1} (α := Localization (M := S) (algebraMapSubmonoid S p.primeCompl))
    ((algebraMap (Localization (M := R) p.primeCompl) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)) :
          (a : Localization p.primeCompl) → Localization (algebraMapSubmonoid S p.primeCompl))
        x :
      Localization (M := S) (algebraMapSubmonoid S p.primeCompl))
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) :
                S ⊗[R] Localization.AtPrime p →+* Localization (algebraMapSubmonoid S p.primeCompl))
              (↑includeRight : Localization.AtPrime p →+* S ⊗[R] Localization.AtPrime p) :
            RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization (M := S) (algebraMapSubmonoid S p.primeCompl))) :
          (a : Localization p.primeCompl) → Localization (algebraMapSubmonoid S p.primeCompl))
        x :
      Localization (M := S) (algebraMapSubmonoid S p.primeCompl))
Tactic: ext
-- 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)
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
    (comap (AlgHom.toRingHom includeRight) q)
have simp : Membership.mem (γ := Set (PrimeSpectrum R)) {p} (comap (algebraMap R (p.asIdeal.Fiber S)) q)
Tactic: simp only [AlgHom.toRingHom_eq_coe, Set.mem_preimage, ← comap_comp_apply,
      AlgHom.comp_algebraMap_of_tower]
-- 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 : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
⊢ (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) ⋯)
      ((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) })
        q) =
    q
have a : ∀ (x : S),
  Membership.mem (γ := Ideal S)
      (asIdeal
        (↑((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)
              ((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) })
                q)) :
          PrimeSpectrum S))
      x ↔
    x ∈ (↑q : PrimeSpectrum S).asIdeal
Tactic: ext x
-- 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)
⊢ (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) =
    q
have asIdeal : ∀ (x : p.asIdeal.Fiber S),
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (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)))
      x ↔
    x ∈ q.asIdeal
Tactic: ext x
-- 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
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (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 : ∀ (r : R) (hr : r ∉ p.asIdeal) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (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)))
      x ↔
    x ∈ q.asIdeal
Tactic: obtain ⟨r, hr, s, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (hypothesis)
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
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (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 this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
Tactic: have := @PrimeSpectrum.isPrime
-- 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
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (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 : 1 ⊗ₜ[R] s ∈ q.asIdeal ↔
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
    (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)))
    (1 ⊗ₜ[R] s)
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]
-- 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)
⊢ 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) ∉ 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]
-- 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
⊢ ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉ q.asIdeal
have asIdeal : r ∉ asIdeal (comap (algebraMap R (p.asIdeal.Fiber S)) q)
Tactic: rw [← Ideal.mem_comap, ← PrimeSpectrum.comap_asIdeal]
-- 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
⊢ r ∉ asIdeal (comap (algebraMap R (p.asIdeal.Fiber S)) q)
have h : comap (algebraMap R (p.asIdeal.Fiber S)) q = p
Tactic: convert! hr