awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ s ⊆ (↑N : Set M)
have refine_3 : span R s ≤ N
Tactic: rw [← span_le, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ s ⊆ (↑N : Set M)
have refine_3₁ : N ≤ N
Tactic: rw [← span_le, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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 ∈ N, r • n = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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)
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
have 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
Tactic: rcases H with ⟨r, hr1, hrn, _⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
have empty : ∀ (n : M) (hn : n ∈ N), r • n = 0
Tactic: refine ⟨r, hr1, fun n hn => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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
⊢ r • n = 0
have 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
Tactic: specialize hrn hn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ r • n = 0
have 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
Tactic: rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ r • n = 0
have 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
Tactic: rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ r • n = 0
have 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
Tactic: rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
⊢ r • n = 0
have 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
Tactic: rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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 i s))) ∧
        insert i s ⊆ (↑N : Set M)
⊢ ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
have 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)
Tactic: apply ih
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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 i s))) ∧
        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)
have 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 i s))))
  (hs : 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)
Tactic: rcases H with ⟨r, hr1, hrn, hs⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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)
⊢ ∃ (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)
have hrn₁ : 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
Cleared hypotheses: hrn, hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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 (R ∙ i) ⊔ HSMul.hSMul (β := Submodule R M) I (span R s))
hs : 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)
have hs₁ : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
Tactic: rw [Set.insert_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
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 (R ∙ i) ⊔ HSMul.hSMul (β := Submodule R M) I (span R s)))
    i
⊢ ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have hrn₁ : ∃ y ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ i),
  ∃ z ∈ HSMul.hSMul (β := Submodule R M) I (span R s),
    y + z = (((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) i
Tactic: rw [mem_comap, mem_sup] at hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
hrn :
  ∃ y ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ i),
    ∃ z ∈ HSMul.hSMul (β := Submodule R M) I (span R s),
      y + z = (((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) i
⊢ ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have rcases : ∀ (y : M) (hy : y ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ i)) (z : M)
  (hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s))
  (hyz : y + z = (((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M) i),
  ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: rcases hrn with ⟨y, hy, z, hz, hyz⟩
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
y : M
hy : y ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ i)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
hyz : y + z = r • i
⊢ ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have rw : ∀ (hy : ∃ y_1 ∈ I, y_1 • i = y) (z : M) (hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)) (hyz : y + z = r • i),
  ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: rw [mem_smul_span_singleton] at hy
Cleared hypotheses: hy, z, hz, hyz
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
y : M
hy : ∃ y_1 ∈ I, y_1 • i = y
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
hyz : y + z = r • i
⊢ ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have rcases : ∀ (c : R) (hci : c ∈ I) (hyz : c • i + z = r • i),
  ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: rcases hy with ⟨c, hci, rfl⟩
Cleared hypotheses: y, hy, hyz
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have h : r - c - 1 ∈ I ∧ (r - c) • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: use r - c
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I ∧ (r - c) • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have h : r - c - 1 ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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_1 : 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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
c : R
hci : c ∈ I
hyz : c • i + z = r • i
h : r - c - 1 ∈ I
⊢ r - c - 1 ∈ I ∧ (r - c) • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
have h₁ : (r - c) • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I
have h : r - 1 - c ∈ I
Tactic: rw [sub_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (hypothesis)
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 (R ∙ i) ⊔ HSMul.hSMul (β := Submodule R M) I (span R s))
hs : i ∈ (↑N : Set M) ∧ 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)
have this : ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
Tactic: have : ∃ c : R, c - 1 ∈ I ∧ c • i ∈ I • span R s := by
    specialize hrn hs.1
    rw [mem_comap, mem_sup] at hrn
    rcases hrn with ⟨y, hy, z, hz, hyz⟩
    dsimp at hyz
    rw [mem_smul_span_singleton] at hy
    rcases hy with ⟨c, hci, rfl⟩
    use r - c
    constructor
    · rw [sub_right_comm]
      exact I.sub_mem hr1 hci
    · rw [sub_smul, ← hyz, add_sub_cancel_left]
      exact hz
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nakayama (goal)
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 (R ∙ i) ⊔ HSMul.hSMul (β := Submodule R M) I (span R s))
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
this : ∃ (c : R), c - 1 ∈ I ∧ c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
⊢ ∃ (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)
have insert : ∀ (c : R) (hc1 : c - 1 ∈ I) (hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)),
  ∃ (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 this with ⟨c, hc1, hci⟩
Cleared hypotheses: this