awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
rw :
  (∀ x ∈ (↑p.support : Set (σ →₀ ℕ)),
      Membership.mem (γ := Set (σ →₀ ℕ)) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n} x) ↔
    ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n
⊢ (truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.totalDegree < n

Tactic:
rw [truncTotal, truncFinset_coe_eq_self_iff, Set.Finite.subset_toFinset,
    MvPolynomial.totalDegree, Finset.sup_lt_iff (bot_lt_iff_ne_bot.mpr h), Set.subset_def]

Premises used: MvPowerSeries.truncTotal, Iff.mpr, Set.subset_def, bot_lt_iff_ne_bot, Finset.sup_lt_iff, Set.Finite.subset_toFinset, MvPolynomial.totalDegree, MvPowerSeries.truncFinset_coe_eq_self_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ (∀ x ∈ (↑p.support : Set (σ →₀ ℕ)),
      Membership.mem (γ := Set (σ →₀ ℕ)) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n} x) ↔
    ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n

Tactic:
simp [degree, sum]

Premises used: Finsupp.sum, Finsupp.degree
-- Module: Mathlib.RingTheory.Nakayama
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 = J • N

Tactic:
le_antisymm ?_ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)

Premises used: Iff.mpr, le_antisymm, Submodule.smul_le, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Nakayama
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
refine : N ≤ J • N
⊢ N = J • N

Tactic:
refine le_antisymm ?_ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)

Premises used: Iff.mpr, le_antisymm, Submodule.smul_le, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Nakayama
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
obtain : ∀ (r : R) (hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0), n ∈ J • N
⊢ n ∈ J • N

Tactic:
obtain ⟨r, hr⟩ := Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN

Premises used: Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
-- Module: Mathlib.RingTheory.Nakayama
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
obtain : ∀ (s : R) (hs : s * r - 1 ∈ J), n ∈ J • N
⊢ n ∈ J • N

Tactic:
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1)

Premises used: And.left, Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson
-- Module: Mathlib.RingTheory.Nakayama
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
rw₆ rw₇ : n = n
⊢ n = -(s * r - 1) • n

Tactic:
rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]

Premises used: neg_sub, sub_zero, sub_smul, smul_zero, one_smul, And.right, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Nakayama
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

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]
-- Module: Mathlib.RingTheory.Nakayama
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
rw : -(s * r - 1) • n ∈ J • N
⊢ n ∈ J • N

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Nakayama
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
⊢ -(s * r - 1) • n ∈ J • N

Tactic:
Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn

Premises used: Set.Mem, Submodule.neg_mem, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Nakayama
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 ≤ N.annihilator.jacobson
⊢ N = ⊥

Tactic:
(eq_smul_of_le_smul_of_le_jacobson hN hIN.le hIjac).trans N.annihilator_smul

Premises used: Submodule.eq_smul_of_le_smul_of_le_jacobson, Submodule.annihilator_smul, Eq.le, Eq.trans
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
N : Submodule R M
hN : N.FG
hrN : N = r • N
hrJac : r ∈ N.annihilator.jacobson
⊢ N = ⊥

Tactic:
eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator hN
    (Eq.trans hrN (ideal_span_singleton_smul r N).symm)
    ((span_singleton_le_iff_mem r _).mpr hrJac)

Premises used: Iff.mpr, Submodule.ideal_span_singleton_smul, Submodule.span_singleton_le_iff_mem, Eq.symm, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator, Eq.trans
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
N : Submodule R M
hN : N.FG
hsN : N = s • N
hsJac : s ⊆ (↑N.annihilator.jacobson : Set R)
⊢ N = ⊥

Tactic:
eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator hN
    (Eq.trans hsN (span_smul_eq s N).symm) (span_le.mpr hsJac)

Premises used: Iff.mpr, Submodule.span_smul_eq, Eq.symm, Submodule.span_le, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator, Eq.trans
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Module.Finite R M
I : Ideal R
h : I ≤ jacobson (Module.annihilator R M)
⊢ ⊤ ≠ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
fun H => top_ne_bot <|
  eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator Module.Finite.fg_top H <|
    (congrArg (I ≤ Ideal.jacobson ·) annihilator_top).mpr h

Premises used: Eq.mpr, Module.Finite.fg_top, congrArg, top_ne_bot, Ideal.jacobson, LE.le, Submodule.annihilator_top, Not, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Module.Finite R M
s : Set R
h : s ⊆ (↑(jacobson (Module.annihilator R M)) : Set R)
⊢ ⊤ ≠ HSMul.hSMul (β := Submodule R M) s ⊤

Tactic:
ne_of_ne_of_eq (top_ne_ideal_smul_of_le_jacobson_annihilator (span_le.mpr h))
    (span_smul_eq _ _)

Premises used: Iff.mpr, Submodule.span_smul_eq, Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator, ne_of_ne_of_eq, Submodule.span_le
-- Module: Mathlib.RingTheory.Nakayama
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Module.Finite R M
r : R
h : Membership.mem (γ := Ideal R) (jacobson (Module.annihilator R M)) r
⊢ ⊤ ≠ HSMul.hSMul (β := Submodule R M) r ⊤

Tactic:
ne_of_ne_of_eq (top_ne_set_smul_of_subset_jacobson_annihilator <|
                    Set.singleton_subset_iff.mpr h) (singleton_set_smul ⊤ r)

Premises used: Iff.mpr, Set.singleton_subset_iff, Submodule.top_ne_set_smul_of_subset_jacobson_annihilator, Submodule.singleton_set_smul, Top.top, ne_of_ne_of_eq
-- Module: Mathlib.RingTheory.Nakayama
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 = ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
⊢ N = ⊥

Tactic:
rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]

Premises used: Submodule.eq_smul_of_le_smul_of_le_jacobson, Submodule.bot_smul
-- Module: Mathlib.RingTheory.Nakayama
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 ⊔ 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 _ _) _)
-- Module: Mathlib.RingTheory.Nakayama
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'
⊢ Function.Injective (comap N.mkQ)

Tactic:
have h_comap :=
    comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
-- Module: Mathlib.RingTheory.Nakayama
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)
⊢ map N.mkQ (I • N') = map N.mkQ N'

Tactic:
simpa only [← h_comap.eq_iff, comap_map_mkQ, sup_comm, eq_comm] using hNN'

Premises used: Function.Injective.eq_iff, eq_comm, Submodule.comap_map_mkQ, sup_comm
-- Module: Mathlib.RingTheory.Nakayama
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)
⊢ 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'
-- Module: Mathlib.RingTheory.Nakayama
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')
rw₁ rw₂ : map N.mkQ N' ≤ map N.mkQ N'
⊢ map N.mkQ N' ≤ I • map N.mkQ N'

Tactic:
rw [← map_smul'', this]

Premises used: Submodule.map_smul''
-- Module: Mathlib.RingTheory.Nakayama
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' = 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
-- Module: Mathlib.RingTheory.Nakayama
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'
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (this : N ⊔ N' = N ⊔ J • N'), 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

Premises used: Submodule.map_smul'', Function.Injective.eq_iff, sup_comm, Submodule.ker_mkQ, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Nakayama
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 ⊔ I • N' = N ⊔ J • N'

Tactic:
((sup_le_sup_left smul_le_right _).antisymm (sup_le le_sup_left hNN)).trans
    (sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN)

Premises used: sup_le_sup_left, Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson, le_sup_left, LE.le.antisymm, sup_le, Eq.trans
-- Module: Mathlib.RingTheory.Nakayama
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
rw₃ rw₄ : N = 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]

Premises used: Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson, Submodule.bot_smul, sup_eq_left, sup_bot_eq
-- Module: Mathlib.RingTheory.Nakayama
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' : Submodule R M
hN' : N'.FG
hIJ : I ≤ jacobson ⊥
hNN : N' ≤ N ⊔ I • N'
⊢ I • N' ≤ N

Tactic:
smul_le_right.trans (le_of_le_smul_of_le_jacobson_bot hN' hIJ hNN)

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, Submodule.smul_le_right, LE.le.trans
-- Module: Mathlib.RingTheory.Nakayama
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'
⊢ N ⊔ I • N' ≤ N ⊔ N'

Tactic:
simpa using le_trans smul_le_right le_sup_right

Premises used: Submodule.smul_le_right, le_trans
-- Module: Mathlib.RingTheory.Nakayama
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'
⊢ P ≤ N ⊔ N'

Tactic:
have hNN'' : P ≤ N ⊔ N' := le_trans hNN' (by simpa using le_trans smul_le_right le_sup_right)
-- Module: Mathlib.RingTheory.Nakayama
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'

Tactic:
le_antisymm ?_ (map_mono hN'le)

Premises used: le_antisymm, Submodule.map_mono
-- Module: Mathlib.RingTheory.Nakayama
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'
refine : map N.mkQ P ≤ map N.mkQ N'
⊢ map N.mkQ P = map N.mkQ N'

Tactic:
refine le_antisymm ?_ (map_mono hN'le)

Premises used: le_antisymm, Submodule.map_mono
-- Module: Mathlib.RingTheory.Nakayama
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'

Tactic:
simpa using map_mono (f := N.mkQ) hNN''

Premises used: Submodule.map_mono
-- Module: Mathlib.RingTheory.Nakayama
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'

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''
-- Module: Mathlib.RingTheory.Nakayama
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')
a₁ : map N.mkQ (I • N') ≤ map N.mkQ P
⊢ map N.mkQ P = map N.mkQ (I • N')

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Nakayama
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')

Tactic:
simpa using map_mono (f := N.mkQ) hNN'

Premises used: Submodule.map_mono
-- Module: Mathlib.RingTheory.Nakayama
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 (I • N') ≤ map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P

Tactic:
rw [h1]
-- Module: Mathlib.RingTheory.Nakayama
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 N'

Tactic:
simp [smul_le_right]

Premises used: Submodule.smul_le_right
-- Module: Mathlib.RingTheory.Nakayama
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')

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]
-- Module: Mathlib.RingTheory.Nakayama
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')
rw : map N.mkQ (I • N')
| map N.mkQ P

Tactic:
rw [h2]
-- Module: Mathlib.RingTheory.Nakayama
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')
conv_lhs : map N.mkQ (I • N') ≤ I • map N.mkQ P
⊢ map N.mkQ P ≤ I • map N.mkQ P

Tactic:
conv_lhs => rw [h2]
-- Module: Mathlib.RingTheory.Nakayama
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 (I • N') ≤ I • map N.mkQ P

Tactic:
simp [← h1]
-- Module: Mathlib.RingTheory.Nakayama
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

Tactic:
have hle : (P.map N.mkQ) ≤ I • P.map N.mkQ := by
    conv_lhs => rw [h2]
    simp [← h1]
-- Module: Mathlib.RingTheory.Nakayama
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
obtain : ∀ (r : R) (hmem : r - 1 ∈ I) (hr : ∀ n ∈ map N.mkQ P, r • n = 0), ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N
⊢ ∃ (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

Premises used: Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
-- Module: Mathlib.RingTheory.Nakayama
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

Tactic:
⟨r, hmem, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Nakayama
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
refine : ∀ (x : M) (hx : x ∈ r • P), x ∈ N
⊢ ∃ (r : R), r - 1 ∈ I ∧ r • P ≤ N

Tactic:
refine ⟨r, hmem, fun x hx ↦ ?_⟩
-- Module: Mathlib.RingTheory.Nakayama
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
smul₀ : HSMul.hSMul (β := M ⧸ N) r (Quotient.mk p) = 0
⊢ r • p ∈ N

Tactic:
rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]

Premises used: Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Nakayama
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
⊢ HSMul.hSMul (β := M ⧸ N) r (Quotient.mk p) = 0

Tactic:
hr _ ⟨p, hp, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Nakayama
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
⊢ HSMul.hSMul (β := M ⧸ N) r (Quotient.mk p) = 0

Tactic:
exact hr _ ⟨p, hp, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Nakayama
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
r_1 : R
m : M
mem : m ∈ r • P
h : m ∈ N
⊢ r_1 • m ∈ N

Tactic:
N.smul_mem _ h

Premises used: Submodule.smul_mem