awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
obtain :
  ∀ (S' : Type u) (w : CommRing S') (w_1 : Algebra R S'),
    Module.Finite R S' →
      Module.Free R S' →
        FinitePresentation R S' →
          ∀ (f : S' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)),
            FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
obtain ⟨S', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S

Premises used: Module.Finite.exists_free_surjective
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ FinitePresentation R S

Tactic:
.of_surjective hf ?_

Premises used: Algebra.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
refine : Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R S

Tactic:
refine .of_surjective hf ?_
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
apply : Submodule.FG (Submodule.restrictScalars R (RingHom.ker f.toRingHom))
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
apply Submodule.FG.of_restrictScalars R

Premises used: Submodule.FG.of_restrictScalars
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ Submodule.FG (Submodule.restrictScalars R (RingHom.ker f.toRingHom))

Tactic:
Module.FinitePresentation.fg_ker f.toLinearMap hf

Premises used: Module.FinitePresentation.fg_ker, AlgHom.toLinearMap, Set.Mem, Submodule.restrictScalars, LinearMap.ker, setOf, Submodule.comap, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FinitePresentation R S
S' : Type u
w : CommRing S'
w_1 : Algebra R S'
w_2 : Module.Finite R S'
w_3 : Module.Free R S'
w_4 : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := S') (β := S) (⇑f : (a : S') → S)
⊢ Submodule.FG (Submodule.restrictScalars R (RingHom.ker f.toRingHom))

Tactic:
exact Module.FinitePresentation.fg_ker f.toLinearMap hf

Premises used: Module.FinitePresentation.fg_ker, AlgHom.toLinearMap
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
obtain :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S

Premises used: Module.Finite.exists_free_surjective
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this : Algebra R' S := f.toAlgebra
⊢ IsScalarTower R R' S

Tactic:
have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this : IsScalarTower R R' S
⊢ FinitePresentation R R'

Tactic:
have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this_2 : IsScalarTower R R' S
this : FinitePresentation R R'
⊢ FinitePresentation R' S

Tactic:
have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this_2 : IsScalarTower R R' S
this_3 : FinitePresentation R R'
this : FinitePresentation R' S
⊢ FinitePresentation R S

Tactic:
.trans R S R'

Premises used: Module.FinitePresentation.trans
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Module.Finite R R'
w_3 : Free R R'
w_4 : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)
this_1 : Algebra R' S := f.toAlgebra
this_2 : IsScalarTower R R' S
this_3 : FinitePresentation R R'
this : FinitePresentation R' S
⊢ FinitePresentation R S

Tactic:
exact .trans R S R'
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Algebra.FinitePresentation R S
obtain :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₁ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            FinitePresentation R S
obtain₂ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this : IsScalarTower R R' S), FinitePresentation R S
obtain₃ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this : IsScalarTower R R' S) (this : FinitePresentation R R'), FinitePresentation R S
obtain₄ :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Module.Finite R R' →
      Free R R' →
        Algebra.FinitePresentation R R' →
          ∀ (f : R' →ₐ[R] S) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R') (β := S) (⇑f : (a : R') → S)),
            let this := f.toAlgebra;
            ∀ (this_1 : IsScalarTower R R' S) (this_2 : FinitePresentation R R') (this : FinitePresentation R' S),
              FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
classical
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  letI := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'

Premises used: Module.Finite.exists_free_surjective
-- Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
⊢ FinitePresentation R S ↔ Algebra.FinitePresentation R S

Tactic:
⟨fun _ ↦ .of_finitePresentation R S, fun _ ↦ .of_finite_of_finitePresentation R S⟩

Premises used: Iff.intro, Algebra.FinitePresentation.of_finitePresentation, Module.FinitePresentation.of_finite_of_finitePresentation
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
⊢ ∃ (S : Set M), S.Finite ∧ span R S = N

Tactic:
rw [fg_def] at hn

Premises used: Submodule.fg_def
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
hn₁ : ∃ (S : Set M), S.Finite ∧ span R S = N
⊢ N ≤ I • N

Tactic:
rw [fg_def] at hn

Premises used: Submodule.fg_def
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ (S : Set M), S.Finite ∧ span R S = N
hin : N ≤ I • N
rcases : ∀ (s : Set M) (hfs : s.Finite) (hs : span R s = N), ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
rcases hn with ⟨s, hfs, hs⟩
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)

Tactic:
⟨1, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_1 : HSub.hSub (α := R) 1 1 ∈ I
refine_2 :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1)
      (HSMul.hSMul (β := Submodule R M) I (span R s))
refine_3 : s ⊆ (↑N : Set M)
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)

Tactic:
refine ⟨1, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_1 : 0 ∈ I
⊢ HSub.hSub (α := R) 1 1 ∈ I

Tactic:
rw [sub_self]

Premises used: sub_self
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ 0 ∈ I

Tactic:
I.zero_mem

Premises used: Set.Mem, Ideal.zero_mem
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ 0 ∈ I

Tactic:
exact I.zero_mem

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_2 : N ≤ comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1) (I • N)
⊢ N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1)
      (HSMul.hSMul (β := Submodule R M) I (span R s))

Tactic:
rw [hs]
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n ∈ I • N
⊢ Membership.mem (α := M) (I • N) (((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) 1 : (a : M) → M) n : M)

Tactic:
change (1 : R) • n ∈ I • N

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
refine_2 : n ∈ I • N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n ∈ I • N

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ I • N

Tactic:
hin hn
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ I • N

Tactic:
exact hin hn
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
refine_3 : span R s ≤ N
refine_3₁ refine_3₂ : N ≤ N
⊢ s ⊆ (↑N : Set M)

Tactic:
rw [← span_le, hs]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)

Tactic:
have H : ∃ r : R, r - 1 ∈ I ∧ N ≤ (I • span R s).comap (LinearMap.lsmul R M r) ∧ s ⊆ N := by
    refine ⟨1, ?_, ?_, ?_⟩
    · rw [sub_self]
      exact I.zero_mem
    · rw [hs]
      intro n hn
      rw [mem_comap]
      change (1 : R) • n ∈ I • N
      rw [one_smul]
      exact hin hn
    · rw [← span_le, hs]
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set M
H :
  ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R ∅)) ∧
        ∅ ⊆ (↑N : Set M)
empty :
  ∀ (r : R) (hr1 : r - 1 ∈ I)
    (hrn :
      N ≤
        comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
          (HSMul.hSMul (β := Submodule R M) I (span R ∅))),
    ∅ ⊆ (↑N : Set M) → ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
rcases H with ⟨r, hr1, hrn, _⟩
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
hrn :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R ∅))
right : ∅ ⊆ (↑N : Set M)
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
⟨r, hr1, fun n hn => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
hrn :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R ∅))
right : ∅ ⊆ (↑N : Set M)
empty : ∀ (n : M) (hn : n ∈ N), r • n = 0
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
refine ⟨r, hr1, fun n hn => ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
hrn :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R ∅))
right : ∅ ⊆ (↑N : Set M)
n : M
hn : n ∈ N
⊢ Membership.mem (γ := Submodule R M)
    (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R ∅)))
    n

Tactic:
specialize hrn hn
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
right : ∅ ⊆ (↑N : Set M)
n : M
hn : n ∈ N
hrn :
  Membership.mem (γ := Submodule R M)
    (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R ∅)))
    n
empty :
  ∀
    (hrn :
      Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I (span R ∅))
        ((((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) n : M)),
    r • n = 0
empty₁ :
  ∀
    (hrn :
      Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊥)
        ((((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) n : M)),
    r • n = 0
empty₂ :
  ∀
    (hrn :
      Membership.mem (α := M) (γ := Submodule R M) ⊥
        ((((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) n : M)),
    r • n = 0
empty₃ empty₄ empty₅ empty₆ :
  ∀ (hrn : Eq (α := M) ((((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) n : M) (0 : M)),
    r • n = 0
⊢ r • n = 0

Tactic:
rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn

Premises used: Submodule.smul_bot, Submodule.mem_bot, Submodule.mem_comap, Submodule.span_empty
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
H :
  ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R (Insert.insert i s))) ∧
        Insert.insert i s ⊆ (↑N : Set M)
insert :
  ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
apply ih
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
H :
  ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R (Insert.insert i s))) ∧
        Insert.insert i s ⊆ (↑N : Set M)
insert :
  ∀ (r : R) (hr1 : r - 1 ∈ I)
    (hrn :
      N ≤
        comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
          (HSMul.hSMul (β := Submodule R M) I (span R (Insert.insert i s))))
    (hs : Insert.insert i s ⊆ (↑N : Set M)),
    ∃ (r : R),
      r - 1 ∈ I ∧
        N ≤
            comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
              (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
          s ⊆ (↑N : Set M)
⊢ ∃ (r : R),
    r - 1 ∈ I ∧
      N ≤
          comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
            (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
        s ⊆ (↑N : Set M)

Tactic:
rcases H with ⟨r, hr1, hrn, hs⟩
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn :
  N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (span R (insert i s)))
hs : insert i s ⊆ (↑N : Set M)
⊢ N ≤
    comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
      (HSMul.hSMul (β := Submodule R M) I (R ∙ i) ⊔ HSMul.hSMul (β := Submodule R M) I (span R s))

Tactic:
rw [← Set.singleton_union, span_union, smul_sup] at hrn

Premises used: Set.singleton_union, Submodule.smul_sup, Submodule.span_union