awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x_2 : LocalizedModule.AtPrime p M
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x_2})
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
r : Rₚ
x : Nₚ'
⊢ g.toFun (r • x) = HSMul.hSMul (α := Rₚ) ((RingHom.id Rₚ : (a : Rₚ) → Rₚ) r : Rₚ) (g.toFun x)
have simp : (g : (a : Nₚ') → p.ResidueField) (r • x) =
  HSMul.hSMul (β := p.ResidueField) r ((g : (a : Nₚ') → p.ResidueField) x : p.ResidueField)
Tactic: simp only [AddHom.toFun_eq_coe, coe_toAddHom, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
⊢ False
have hx₁ : Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
  (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
Tactic: replace hx : maximalIdeal (Localization.AtPrime p) = (toSpanSingleton _ _ x).ker :=
      hx.trans (by simp [SetLike.ext_iff])
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
⊢ False
have inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
Tactic: have inj1 : Function.Injective i :=
      LinearMap.ker_eq_bot.mp (Submodule.ker_liftQ_eq_bot _ _ _ (le_of_eq hx.symm))
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
⊢ False
have absurd : g = 0
Tactic: absurd hg
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
⊢ g = 0
have h₁ : ∀ (x : Nₚ'),
  Eq.{u_1 + 1} (α := p.ResidueField) ((g : (a : Nₚ') → p.ResidueField) x : p.ResidueField)
    ((0 : (a : Nₚ') → p.ResidueField) x : p.ResidueField)
Tactic: apply LinearMap.ext
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np' : Nₚ'
⊢ Eq.{u_1 + 1} (α := p.ResidueField) ((g : (a : Nₚ') → p.ResidueField) np' : p.ResidueField)
    ((0 : (a : Nₚ') → p.ResidueField) np' : p.ResidueField)
have h₁ : ∀ (np : Nₚ),
  Eq.{u_1 + 1} (α := p.ResidueField) ((g : (a : Nₚ') → p.ResidueField) (Submodule.Quotient.mk np) : p.ResidueField)
    ((0 : (a : Nₚ') → p.ResidueField) (Submodule.Quotient.mk np) : p.ResidueField)
Tactic: induction np' using Submodule.Quotient.induction_on with | _ np
Cleared hypotheses: np'
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np : Nₚ
⊢ Eq.{u_1 + 1} (α := p.ResidueField) ((g : (a : Nₚ') → p.ResidueField) (Submodule.Quotient.mk np) : p.ResidueField)
    ((0 : (a : Nₚ') → p.ResidueField) (Submodule.Quotient.mk np) : p.ResidueField)
have h₁ : Eq.{u_1 + 1} (α := p.ResidueField) ((to_res : (a : Nₚ) → p.ResidueField) np : p.ResidueField) (0 : p.ResidueField)
Tactic: change to_res np = 0
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np : Nₚ
⊢ Eq.{u_1 + 1} (α := p.ResidueField) ((to_res : (a : Nₚ) → p.ResidueField) np : p.ResidueField) (0 : p.ResidueField)
have h₁ : Eq (α := Mₚ) ((i : (a : p.ResidueField) → Mₚ) ((to_res : (a : Nₚ) → p.ResidueField) np) : Mₚ)
  ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)
Tactic: apply inj1
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np : Nₚ
⊢ Eq (α := Mₚ) ((i : (a : p.ResidueField) → Mₚ) ((to_res : (a : Nₚ) → p.ResidueField) np) : Mₚ)
    ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)
have h₁ : Eq (α := Mₚ) ((f : (a : Nₚ) → Mₚ) np : Mₚ) ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)
Tactic: change f np = _