awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.LinearMap
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ₚ'
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)
⊢ Eq.{u_1 + 1} (α := p.ResidueField) ((g : (a : Nₚ') → p.ResidueField) np' : p.ResidueField)
    ((0 : (a : Nₚ') → p.ResidueField) np' : p.ResidueField)

Tactic:
induction np' using Submodule.Quotient.induction_on with | _ np
-- Module: Mathlib.RingTheory.Regular.LinearMap
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ₚ
h₁ : Eq.{u_1 + 1} (α := p.ResidueField) ((to_res : (a : Nₚ) → p.ResidueField) np : p.ResidueField) (0 : p.ResidueField)
⊢ 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:
change to_res np = 0

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Regular.LinearMap
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ₚ
h₁ :
  Eq (α := Mₚ) ((i : (a : p.ResidueField) → Mₚ) ((to_res : (a : Nₚ) → p.ResidueField) np) : Mₚ)
    ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)
⊢ Eq.{u_1 + 1} (α := p.ResidueField) ((to_res : (a : Nₚ) → p.ResidueField) np : p.ResidueField) (0 : p.ResidueField)

Tactic:
apply inj1
-- Module: Mathlib.RingTheory.Regular.LinearMap
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ₚ
h₁ : Eq (α := Mₚ) ((f : (a : Nₚ) → Mₚ) np : Mₚ) ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)
⊢ Eq (α := Mₚ) ((i : (a : p.ResidueField) → Mₚ) ((to_res : (a : Nₚ) → p.ResidueField) np) : Mₚ)
    ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)

Tactic:
change f np = _

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Regular.LinearMap
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ₚ) ((f : (a : Nₚ) → Mₚ) np : Mₚ) ((i : (a : p.ResidueField) → Mₚ) 0 : Mₚ)

Tactic:
simp [eq0]
-- Module: Mathlib.RingTheory.Regular.LinearMap
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
⊢ f ≠ 0

Tactic:
have f_ne0 : f ≠ 0 := by
      intro eq0
      absurd hg
      apply LinearMap.ext
      intro np'
      induction np' using Submodule.Quotient.induction_on with | _ np
      change to_res np = 0
      apply inj1
      change f np = _
      simp [eq0]
-- Module: Mathlib.RingTheory.Regular.LinearMap
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
f_ne0 : f ≠ 0
⊢ ¬?_mvar.59706

Tactic:
hom0
-- Module: Mathlib.RingTheory.Regular.LinearMap
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
f_ne0 : f ≠ 0
inr : ¬Subsingleton (N →ₗ[R] M)
⊢ False

Tactic:
absurd hom0
-- Module: Mathlib.RingTheory.Regular.LinearMap
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
f_ne0 : f ≠ 0
h_3 : FinitePresentation R N := ⋯
inr : ∀ (f_ne0 : Subsingleton (N →ₗ[R] M)), f = 0
⊢ ¬Subsingleton (N →ₗ[R] M)

Tactic:
contrapose f_ne0