awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = -(s * r - 1) • n
have rw : n = (1 - s * r) • n
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
⊢ n = -(s * r - 1) • n
have rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
⊢ n = -(s * r - 1) • n
have rw₂ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - s • r • n
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
rw₂ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - s • r • n
⊢ n = -(s * r - 1) • n
have rw₃ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - HSMul.hSMul (β := M) s 0
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
rw₂ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - s • r • n
rw₃ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - HSMul.hSMul (β := M) s 0
⊢ n = -(s * r - 1) • n
have rw₄ : n = n - HSMul.hSMul (β := M) s 0
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
rw₂ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - s • r • n
rw₃ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - HSMul.hSMul (β := M) s 0
rw₄ : n = n - HSMul.hSMul (β := M) s 0
⊢ n = -(s * r - 1) • n
have rw₅ : n = n - 0
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
rw : n = (1 - s * r) • n
rw₁ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - (s * r) • n
rw₂ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - s • r • n
rw₃ : n = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 n - HSMul.hSMul (β := M) s 0
rw₄ : n = n - HSMul.hSMul (β := M) s 0
rw₅ : n = n - 0
⊢ n = -(s * r - 1) • n
have rw₆ : n = n
Tactic: rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n ∈ J • N
have this : n = -(s * r - 1) • n
Tactic: have : n = -(s * r - 1) • n := by
    rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ n ∈ J • N
have rw : -(s * r - 1) • n ∈ J • N
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ jacobson ⊥
⊢ N = ⊥
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) ⊥ N = ⊥
Tactic: rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ jacobson ⊥
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) ⊥ N = ⊥
⊢ N = ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'
have hNN' : N ⊔ N' = N ⊔ I • N'
Tactic: have hNN' : N ⊔ N' = N ⊔ I • N' :=
    le_antisymm (sup_le le_sup_left hNN)
    (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'
have h_comap : Function.Injective (comap N.mkQ)
Tactic: have h_comap :=
    comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
⊢ N ⊔ N' = N ⊔ J • N'
have this : map N.mkQ (I • N') = map N.mkQ N'
Tactic: have : (I • N').map N.mkQ = N'.map N.mkQ := by
    simpa only [← h_comap.eq_iff, comap_map_mkQ, sup_comm, eq_comm] using hNN'
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ I • map N.mkQ N'
have rw : map N.mkQ N' ≤ map N.mkQ (I • N')
Tactic: rw [← map_smul'', this]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
rw : map N.mkQ N' ≤ map N.mkQ (I • N')
⊢ map N.mkQ N' ≤ I • map N.mkQ N'
have rw₁ : map N.mkQ N' ≤ map N.mkQ N'
Tactic: rw [← map_smul'', this]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'
have this₁ : map N.mkQ N' = J • map N.mkQ N'
Tactic: have :=
    @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _)
      (by rw [← map_smul'', this]) hIJ
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₂ : ∀ (this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₂ : ∀ (this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₃ : ∀ (this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₂ : ∀ (this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₃ : ∀ (this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₄ : ∀ (this : N' ⊔ N = J • N' ⊔ N), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₂ : ∀ (this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₃ : ∀ (this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker), N ⊔ N' = N ⊔ J • N'
rwa₄ : ∀ (this : N' ⊔ N = J • N' ⊔ N), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₅ : ∀ (this : N ⊔ N' = J • N' ⊔ N), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this_1 : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
rwa : ∀ (this : map N.mkQ N' = map N.mkQ (J • N')), N ⊔ N' = N ⊔ J • N'
rwa₁ : ∀ (this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₂ : ∀ (this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))), N ⊔ N' = N ⊔ J • N'
rwa₃ : ∀ (this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker), N ⊔ N' = N ⊔ J • N'
rwa₄ : ∀ (this : N' ⊔ N = J • N' ⊔ N), N ⊔ N' = N ⊔ J • N'
rwa₅ : ∀ (this : N ⊔ N' = J • N' ⊔ N), N ⊔ N' = N ⊔ J • N'
⊢ N ⊔ N' = N ⊔ J • N'
have rwa₆ : ∀ (this : N ⊔ N' = N ⊔ J • N'), N ⊔ N' = N ⊔ J • N'
Tactic: rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ jacobson ⊥
hNN : N' ≤ N ⊔ I • N'
⊢ N' ≤ N
have rw : N ⊔ N' = N
Tactic: rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ jacobson ⊥
hNN : N' ≤ N ⊔ I • N'
rw : N ⊔ N' = N
⊢ N' ≤ N
have rw₁ : N ⊔ HSMul.hSMul.{u_3, u_4, u_4} (α := Ideal R) ⊥ N' = N
Tactic: rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ jacobson ⊥
hNN : N' ≤ N ⊔ I • N'
rw : N ⊔ N' = N
rw₁ : N ⊔ HSMul.hSMul.{u_3, u_4, u_4} (α := Ideal R) ⊥ N' = N
⊢ N' ≤ N
have rw₂ : N ⊔ ⊥ = N
Tactic: rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ jacobson ⊥
hNN : N' ≤ N ⊔ I • N'
rw : N ⊔ N' = N
rw₁ : N ⊔ HSMul.hSMul.{u_3, u_4, u_4} (α := Ideal R) ⊥ N' = N
rw₂ : N ⊔ ⊥ = N
⊢ N' ≤ N
have rw₃ : N = N
Tactic: rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have hNN'' : P ≤ N ⊔ N'
Tactic: have hNN'' : P ≤ N ⊔ N' := le_trans hNN' (by simpa using le_trans smul_le_right le_sup_right)
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
⊢ map N.mkQ P = map N.mkQ N'
have refine : map N.mkQ P ≤ map N.mkQ N'
Tactic: refine le_antisymm ?_ (map_mono hN'le)
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have h1 : map N.mkQ P = map N.mkQ N'
Tactic: have h1 : P.map N.mkQ = N'.map N.mkQ := by
    refine le_antisymm ?_ (map_mono hN'le)
    simpa using map_mono (f := N.mkQ) hNN''
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ P = map N.mkQ (I • N')
have a : map N.mkQ P ≤ map N.mkQ (I • N')
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
a : map N.mkQ P ≤ map N.mkQ (I • N')
⊢ map N.mkQ P = map N.mkQ (I • N')
have a₁ : map N.mkQ (I • N') ≤ map N.mkQ P
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P
have a : map N.mkQ (I • N') ≤ map N.mkQ N'
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have h2 : map N.mkQ P = map N.mkQ (I • N')
Tactic: have h2 : P.map N.mkQ = (I • N').map N.mkQ := by
    apply le_antisymm
    · simpa using map_mono (f := N.mkQ) hNN'
    · rw [h1]
      simp [smul_le_right]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
| map N.mkQ P
have rw : map N.mkQ (I • N')
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
⊢ map N.mkQ P ≤ I • map N.mkQ P
have conv_lhs : map N.mkQ (I • N') ≤ I • map N.mkQ P
Tactic: conv_lhs => rw [h2]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have hle : map N.mkQ P ≤ I • map N.mkQ P
Tactic: have hle : (P.map N.mkQ) ≤ I • P.map N.mkQ := by
    conv_lhs => rw [h2]
    simp [← h1]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have obtain : ∀ (r : R) (hmem : r - 1 ∈ I) (hr : ∀ n ∈ map N.mkQ P, r • n = 0), ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
Tactic: obtain ⟨r, hmem, hr⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I _
    (h1 ▸ hN'.map _) hle
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
have refine : ∀ (x : M) (hx : x ∈ r • P), x ∈ N
Tactic: refine ⟨r, hmem, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x p : M
hp : p ∈ P
⊢ r • p ∈ N
have smul₀ : HSMul.hSMul (β := M ⧸ N) r (Quotient.mk p) = 0
Tactic: rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
⊢ x ∈ N
have smul₀ : ∀ (p : M) (hp : p ∈ P), r • p ∈ N
Tactic: induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem
Cleared hypotheses: hx