awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
t : Localization.AtPrime p
hrt :
  HSMul.hSMul (β := p.ResidueField) r
      ((IsLocalRing.residue (Localization.AtPrime p) :
            (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
          t :
        IsLocalRing.ResidueField (Localization.AtPrime p)) ∉
    ⊥
e :
  1 ⊗ₜ[R]
        HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
                (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
              t :
            IsLocalRing.ResidueField (Localization.AtPrime p)) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        t
obtain :
  ∀ (y : R) (t : ↥p.primeCompl)
    (hrt :
      HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))) ∉
        ⊥)
    (e :
      1 ⊗ₜ[R]
            HSMul.hSMul (β := p.ResidueField) r
              ((IsLocalRing.residue (Localization.AtPrime p) :
                  (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
                ((fun (x : R × ↥p.primeCompl) ↦
                    (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                      | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                      Localization.AtPrime p))
                  (y, t))) *
          x =
        a ⊗ₜ[R]
          (IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))),
    ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

Tactic:
obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl t

Premises used: IsLocalization.mk'_surjective, Ideal.primeCompl, rfl
-- 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 : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
hrt :
  HSMul.hSMul (β := p.ResidueField) r
      ((IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        ((fun (x : R × ↥p.primeCompl) ↦
            (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
              | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
              Localization.AtPrime p))
          (y, t))) ∉
    ⊥
e :
  1 ⊗ₜ[R]
        HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        ((fun (x : R × ↥p.primeCompl) ↦
            (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
              | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
              Localization.AtPrime p))
          (y, t))
⊢ r ∉ p ∧ y ∉ p

Tactic:
simp only [smul_def, Submodule.mem_bot, mul_eq_zero, algebraMap_residueField_eq_zero,
    IsLocalRing.residue_eq_zero_iff, not_or, IsLocalization.AtPrime.mk'_mem_maximal_iff] at hrt

Premises used: IsLocalRing.residue_eq_zero_iff, Submodule.mem_bot, mul_eq_zero, not_or, Algebra.smul_def, Ideal.algebraMap_residueField_eq_zero
-- 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 : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        ((fun (x : R × ↥p.primeCompl) ↦
            (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
              | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
              Localization.AtPrime p))
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

Tactic:
⟨r * y, p.primeCompl.mul_mem hrt.1 hrt.2, y • a, ?_⟩

Premises used: HMul.hMul, Submonoid.mul_mem, And.right, And.left, And.intro, Exists.intro, HSMul.hSMul, Ideal.primeCompl
-- 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 : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        ((fun (x : R × ↥p.primeCompl) ↦
            (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
              | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
              Localization.AtPrime p))
          (y, t))
hrt : r ∉ p ∧ y ∉ p
refine : (r * y) • x = (y • a) ⊗ₜ[R] 1
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

Tactic:
refine ⟨r * y, p.primeCompl.mul_mem hrt.1 hrt.2, y • a, ?_⟩
-- 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 : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            ((fun (x : R × ↥p.primeCompl) ↦
                (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
                  | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
                  Localization.AtPrime p))
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p) :
          (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
        ((fun (x : R × ↥p.primeCompl) ↦
            (match (motive := R × ↥p.primeCompl → Localization.AtPrime p) x with
              | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m :
              Localization.AtPrime p))
          (y, t))
hrt : r ∉ p ∧ y ∉ p
rw : (r * y) • x = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) a ⊗ₜ[R] 1
⊢ (r * y) • x = (y • a) ⊗ₜ[R] 1

Tactic:
rw [Algebra.smul_def, ← Algebra.TensorProduct.includeRight.commutes, smul_tmul,
    ← Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.includeRight_apply]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.includeRight_apply, Algebra.algebraMap_eq_smul_one, AlgHom.commutes, Algebra.smul_def, Algebra.TensorProduct.includeRight
-- 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 : Ideal R
inst_4 : p.IsPrime
q : Ideal (p.Fiber S)
inst_5 : q.IsPrime
⊢ q.LiesOver p

Tactic:
.trans _ (⊥ : Ideal p.ResidueField) _

Premises used: Bot.bot, Ideal.LiesOver.trans
-- 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 : Ideal R
inst_3 : p.IsPrime
x : p.Fiber S
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
⊢ ∃ 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)

Premises used: Ideal.ResidueField.exists_smul_eq_tmul_one, Algebra.TensorProduct.comm, DFunLike.coe
-- 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 : Ideal R
inst_3 : p.IsPrime
x : p.Fiber S
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 • x = 1 ⊗ₜ[R] s

Tactic:
simpa using congr((Algebra.TensorProduct.comm _ _ _).symm $e)
-- 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 : Ideal R
inst_3 : p.IsPrime
x : p.Fiber S
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:
refine ⟨r, hr, s, by simpa using congr((Algebra.TensorProduct.comm _ _ _).symm $e)⟩
-- 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 : Ideal R
inst_3 : p.IsPrime
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)))
⊢ 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))))

Tactic:
rw [← Ideal.map_coe includeRight, Ideal.map_map]

Premises used: Ideal.map_map, Ideal.map_coe, Algebra.TensorProduct.includeRight
-- 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 : Ideal R
inst_3 : p.IsPrime
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))
⊢ 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:
congr
-- 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 : Ideal R
inst_3 : p.IsPrime
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))
⊢ 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:
ext
-- 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 : Ideal R
inst_3 : p.IsPrime
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:
simp [Localization.tensorLeftAlgEquiv_apply_one_tmul p.primeCompl]

Premises used: Ideal.primeCompl, Localization.tensorLeftAlgEquiv_apply_one_tmul
-- 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 : Ideal R
inst_3 : p.IsPrime
⊢ ∀ (r : S),
    Eq (α :=
      HasQuotient.Quotient (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)) (B :=
        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))))
      (Equiv.toFun
        (RingEquiv.toEquiv
          (Ideal.quotientEquiv
            (Ideal.map (R := Localization.AtPrime p) (F := Localization.AtPrime p →ₐ[R] S ⊗[R] Localization.AtPrime p)
              includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p)))
            (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)))
            (AlgEquiv.toRingEquiv (Localization.tensorLeftAlgEquiv p.primeCompl S)) ⋯))
        ((algebraMap S
              (HasQuotient.Quotient (S ⊗[R] Localization.AtPrime p) (B := Ideal (S ⊗[R] Localization.AtPrime p))
                (Ideal.map (R := Localization.AtPrime p) (F :=
                  Localization.AtPrime p →ₐ[R] S ⊗[R] Localization.AtPrime p) includeRight
                  (IsLocalRing.maximalIdeal (Localization.AtPrime p)))) :
            (a : S) →
              S ⊗[R] Localization.AtPrime p ⧸
                Ideal.map includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p)))
          r))
      ((algebraMap S
            (HasQuotient.Quotient (Localization (M := S) (algebraMapSubmonoid S p.primeCompl)) (B :=
              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)))) :
          (a : S) →
            Localization (algebraMapSubmonoid S p.primeCompl) ⧸
              Ideal.map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
                (IsLocalRing.maximalIdeal (Localization p.primeCompl)))
        r)

Tactic:
simp
-- 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)
simp : Membership.mem (γ := Set (PrimeSpectrum R)) {p} (comap (algebraMap R (p.asIdeal.Fiber S)) q)
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
    (comap (AlgHom.toRingHom includeRight) q)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Set.mem_preimage, ← comap_comp_apply,
      AlgHom.comp_algebraMap_of_tower]

Premises used: PrimeSpectrum.comap_comp_apply, AlgHom.comp_algebraMap_of_tower, AlgHom.toRingHom_eq_coe, Set.mem_preimage
-- 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)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {p} (comap (algebraMap R (p.asIdeal.Fiber S)) q)

Tactic:
(residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

Premises used: Algebra.algebraMap, Eq.le, PrimeSpectrum.residueField_comap, Exists.intro, PrimeSpectrum.comap, rfl
-- 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)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {p} (comap (algebraMap R (p.asIdeal.Fiber S)) q)

Tactic:
exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

Premises used: Algebra.algebraMap, Eq.le, PrimeSpectrum.residueField_comap, Exists.intro, PrimeSpectrum.comap, rfl