-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem isNoetherian_iff_fg_wellFounded :
    IsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG }

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M

Proof state:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ span R {x} ⊔ N₀

Tactic:
exact (le_sup_left : (R ∙ x) ≤ _) (Submodule.mem_span_singleton_self _)

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun N => N.FG
⊢ WellFoundedGT { N // N.FG }

Tactic:
exact OrderEmbedding.wellFoundedLT f.dual

Result:
no goals

Proof state:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N ≤ N₀

Tactic:
by_contra h₃

Result:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
⊢ False

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M

Tactic:
intro H

Result:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ IsNoetherian R M

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

Tactic:
intro H

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
⊢ WellFoundedGT { N // N.FG }

Proof state:
case mpr.noetherian
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ ∀ (s : Submodule R M), s.FG

Tactic:
intro N

Result:
case mpr.noetherian
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N : Submodule R M
⊢ N.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Tactic:
let α := { N : Submodule R M // N.FG }

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Proof state:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N = N₀

Tactic:
refine (e.antisymm ?_).symm

Result:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N ≤ N₀

Proof state:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ N₀

Tactic:
rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
  ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
  sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]

Result:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ span R {x} ⊔ N₀

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
⊢ WellFoundedGT { N // N.FG }

Tactic:
let f : α ↪o Submodule R M := OrderEmbedding.subtype _

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun N => N.FG
⊢ WellFoundedGT { N // N.FG }

Proof state:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
⊢ False

Tactic:
obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃

Result:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ False

Proof state:
case mpr.noetherian.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N.FG

Tactic:
convert h₁

Result:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N = N₀

Proof state:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ False

Tactic:
apply hx₂

Result:
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ N₀