-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem isNoetherian_submodule {N : Submodule R M} :
    IsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
⊢ s.FG

Tactic:
have f := (Submodule.equivMapOfInjective N.subtype Subtype.val_injective s).symm

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
⊢ s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
h₂ : Submodule.map f ⊤ = ⊤
⊢ s.FG

Tactic:
have h₃ := ((Submodule.fg_top _).2 h₁).map (↑f : _ →ₗ[R] s)

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
h₂ : Submodule.map f ⊤ = ⊤
h₃ : (Submodule.map ↑f ⊤).FG
⊢ s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
⊢ s.FG

Tactic:
have h₂ : (⊤ : Submodule R (s.map N.subtype)).map f = ⊤ := by simp

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
h₂ : Submodule.map f ⊤ = ⊤
⊢ s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
⊢ Submodule.map f ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG

Tactic:
refine ⟨fun ⟨hn⟩ => fun s hs =>
  have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
  Submodule.map_comap_eq_self this ▸ (hn _).map _,
  fun h => ⟨fun s => ?_⟩⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
⊢ s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
h₂ : Submodule.map f ⊤ = ⊤
h₃ : (Submodule.map ↑f ⊤).FG
⊢ s.FG

Tactic:
exact (Submodule.fg_top _).1 (h₂ ▸ h₃)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
⊢ s.FG

Tactic:
have h₁ := h (s.map N.subtype) (Submodule.map_subtype_le N s)

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s
h₁ : (Submodule.map N.subtype s).FG
⊢ s.FG