awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
a :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
        (∑ x_1 : ι,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ x_1 : ι,
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a₁ : Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [← map_sum, Basis.sum_repr b x]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have pos : ∀ (hI : I = ⊤), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
Tactic: by_cases hI : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
pos : ∀ (hI : I = ⊤), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have neg : ∀ (hI : ¬I = ⊤), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
Tactic: by_cases hI : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have this : Nontrivial.{u_1} (R ⧸ I)
Tactic: have : Nontrivial (R ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr hI
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this : Nontrivial.{u_1} (R ⧸ I)
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have this₁ : IsLocalRing.{u_1} (R ⧸ I)
Tactic: have := IsLocalRing.of_surjective' (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this : IsLocalRing.{u_1} (R ⧸ I)
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have this₁ : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
Tactic: have := IsLocalHom.of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have neg : ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
Tactic: obtain ⟨n, hn⟩ := IsArtinianRing.isNilpotent_jacobson_bot (R := R ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
⊢ Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
have h : ∀ (x : R ⧸ I),
  Membership.mem (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
x : R ⧸ I
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I)) x
have h : ∀ (x : R),
  Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I))
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have this₁ : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
Tactic: have : (maximalIdeal R).map (Ideal.Quotient.mk I) = maximalIdeal (R ⧸ I) := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp [sup_eq_left.mpr (le_maximalIdeal hI)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this_3 : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
this : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have hn₁ : HPow.hPow (α := Ideal R) p n ≤ I
Tactic: rw [jacobson_eq_maximalIdeal _ bot_ne_top, ← this, ← Ideal.map_pow, Ideal.zero_eq_bot,
    Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at hn
Cleared hypotheses: hn, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
⊢ Finite.{u_1 + 1} (R ⧸ I) ↔ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
have refine : (∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I) → Finite.{u_1 + 1} (R ⧸ I)
Tactic: refine ⟨fun _ ↦ exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
⊢ Finite.{u_1 + 1} (R ⧸ I)
have this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)
Tactic: have : Finite (R ⧸ maximalIdeal R) := ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)
⊢ Finite.{u_1 + 1} (R ⧸ I)
have this₁ : Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) p n)
Tactic: have := (Ideal.finite_quotient_pow (IsNoetherian.noetherian (maximalIdeal R)) n)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : R
⊢ Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) x : ResidueField R) (0 : ResidueField R) ↔
    Membership.mem (γ := Ideal R) (maximalIdeal R) x
have rw : Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* ResidueField R) (residue R)) x ↔
  Membership.mem (γ := Ideal R) (maximalIdeal R) x
Tactic: rw [← RingHom.mem_ker, ker_residue]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : R
rw :
  Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* ResidueField R) (residue R)) x ↔
    Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) x : ResidueField R) (0 : ResidueField R) ↔
    Membership.mem (γ := Ideal R) (maximalIdeal R) x
have rw₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x
Tactic: rw [← RingHom.mem_ker, ker_residue]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R →+* S
inst_6 : IsLocalHom (R := R) (S := S) f
a : R
ha : Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) a
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))
    (((RingHom.comp (Ideal.Quotient.mk (maximalIdeal S)) f :
            RingHom.{u_1, u_2} R (HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))) :
          (a : R) → S ⧸ maximalIdeal S)
        a :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))
    (0 : HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))
have rw : Membership.mem (α := S) (γ := Ideal S) (maximalIdeal S : Ideal S) ((f : (a : R) → S) a : S)
Tactic: rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
⊢ IsScalarTower.{u_4, u_1, u_2} (ResidueField R₀) (ResidueField R) (ResidueField S)
have refine : ∀ (x : ResidueField R₀),
  Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S) x : ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R) x) :
      ResidueField S)
Tactic: refine .of_algebraMap_eq fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
x : ResidueField R₀
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S) x : ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R) x) :
      ResidueField S)
have obtain : ∀ (x : R₀),
  Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S)
        ((residue R₀ : (a : R₀) → ResidueField R₀) x) :
      ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R)
          ((residue R₀ : (a : R₀) → ResidueField R₀) x)) :
      ResidueField S)
Tactic: obtain ⟨x, rfl⟩ := residue_surjective x
Cleared hypotheses: 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
inst_4 : IsLocalRing R
inst_5 : IsLocalRing S
inst_6 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans (Algebra.TensorProduct.comm R (ResidueField R) S)
    (AlgEquiv.restrictScalars R (AlgEquiv.symm (quotIdealMapEquivTensorQuot S (maximalIdeal R))))
⊢ Nontrivial (ResidueField R ⊗[R] S)
have rw : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ⊤
Tactic: rw [eSp.nontrivial_congr, Ideal.Quotient.nontrivial_iff]
-- 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 : S ⊗[R] p.ResidueField
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
have obtain : ∀ (t : p.ResidueField) (r : R) (a : S) (hrt : r • t ∉ ⊥) (e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t),
  ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
Tactic: obtain ⟨t, r, a, hrt, e⟩ := RingHom.SurjectiveOnStalks.exists_mul_eq_tmul
    p.surjectiveOnStalks_residueField x ⊥ isPrime_bot
-- 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 : S ⊗[R] p.ResidueField
t : p.ResidueField
r : R
a : S
hrt : r • t ∉ ⊥
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
have obtain : ∀ (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),
  ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
Tactic: obtain ⟨t, rfl⟩ := IsLocalRing.residue_surjective t
Cleared hypotheses: t, hrt, 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 : 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
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
have 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
Tactic: obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl t
Cleared hypotheses: t, hrt, e
-- 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 : 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, ∃ (s : S), r • x = s ⊗ₜ[R] 1
have hrt₁ : 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
Cleared hypotheses: hrt
-- 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 : 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
have refine : (r * y) • x = (y • a) ⊗ₜ[R] 1
Tactic: refine ⟨r * y, p.primeCompl.mul_mem hrt.1 hrt.2, y • a, ?_⟩
-- 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 : 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 * y) • x = (y • a) ⊗ₜ[R] 1
have rw : (r * y) • x = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) a ⊗ₜ[R] 1
Tactic: rw [Algebra.smul_def, ← Algebra.TensorProduct.includeRight.commutes, smul_tmul,
    ← Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.includeRight_apply]