[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ↑f
hg : Function.Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.map f (Submodule.comap f a) = a ⊓ LinearMap.range f
[PROOFSTEP]
simp [Submodule.map_comap_eq, inf_comm]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ↑f
hg : Function.Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.comap g (Submodule.map g a) = a ⊔ LinearMap.range f
[PROOFSTEP]
simp [Submodule.comap_map_eq, h]
[GOAL]
R✝ : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R✝
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ M
inst✝² : Module R✝ P
inst✝¹ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Type u_7} [inst : Ring R] [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)]
    [inst_3 : ∀ (i : ι), IsArtinian R (M i)], IsArtinian R ((i : ι) → M i)
[PROOFSTEP]
apply Finite.induction_empty_option _ _ _ ι
[GOAL]
R✝ : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R✝
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ M
inst✝² : Module R✝ P
inst✝¹ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6},
    α ≃ β →
      (∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
          [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)) →
        ∀ {M : β → Type u_7} [inst : Ring R] [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)]
          [inst_3 : ∀ (i : β), IsArtinian R (M i)], IsArtinian R ((i : β) → M i)
[PROOFSTEP]
intro α β e hα M _ _ _ _
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
N : Type u_4
inst✝¹¹ : Ring R✝
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R✝ M✝
inst✝⁶ : Module R✝ P
inst✝⁵ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝⁴ : Finite ι
α β : Type u_6
e : α ≃ β
hα :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
M : β → Type u_7
inst✝³ : Ring R
inst✝² : (i : β) → AddCommGroup (M i)
inst✝¹ : (i : β) → Module R (M i)
inst✝ : ∀ (i : β), IsArtinian R (M i)
⊢ IsArtinian R ((i : β) → M i)
[PROOFSTEP]
have := @hα
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
N : Type u_4
inst✝¹¹ : Ring R✝
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R✝ M✝
inst✝⁶ : Module R✝ P
inst✝⁵ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝⁴ : Finite ι
α β : Type u_6
e : α ≃ β
hα :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
M : β → Type u_7
inst✝³ : Ring R
inst✝² : (i : β) → AddCommGroup (M i)
inst✝¹ : (i : β) → Module R (M i)
inst✝ : ∀ (i : β), IsArtinian R (M i)
this :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
⊢ IsArtinian R ((i : β) → M i)
[PROOFSTEP]
exact isArtinian_of_linearEquiv (LinearEquiv.piCongrLeft R M e)
[GOAL]
R✝ : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R✝
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ M
inst✝² : Module R✝ P
inst✝¹ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty → Type u_7} [inst : Ring R] [inst_1 : (i : PEmpty) → AddCommGroup (M i)]
    [inst_2 : (i : PEmpty) → Module R (M i)] [inst_3 : ∀ (i : PEmpty), IsArtinian R (M i)],
    IsArtinian R ((i : PEmpty) → M i)
[PROOFSTEP]
intro M _ _ _ _
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
N : Type u_4
inst✝¹¹ : Ring R✝
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R✝ M✝
inst✝⁶ : Module R✝ P
inst✝⁵ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝⁴ : Finite ι
M : PEmpty → Type u_7
inst✝³ : Ring R
inst✝² : (i : PEmpty) → AddCommGroup (M i)
inst✝¹ : (i : PEmpty) → Module R (M i)
inst✝ : ∀ (i : PEmpty), IsArtinian R (M i)
⊢ IsArtinian R ((i : PEmpty) → M i)
[PROOFSTEP]
infer_instance
[GOAL]
R✝ : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R✝
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ M
inst✝² : Module R✝ P
inst✝¹ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [inst : Fintype α],
    (∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
        [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : Option α → Type u_7} [inst : Ring R] [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)] [inst_3 : ∀ (i : Option α), IsArtinian R (M i)],
        IsArtinian R ((i : Option α) → M i)
[PROOFSTEP]
intro α _ ih M _ _ _ _
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
N : Type u_4
inst✝¹² : Ring R✝
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ P
inst✝⁶ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝⁵ : Finite ι
α : Type u_6
inst✝⁴ : Fintype α
ih :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
M : Option α → Type u_7
inst✝³ : Ring R
inst✝² : (i : Option α) → AddCommGroup (M i)
inst✝¹ : (i : Option α) → Module R (M i)
inst✝ : ∀ (i : Option α), IsArtinian R (M i)
⊢ IsArtinian R ((i : Option α) → M i)
[PROOFSTEP]
have := @ih
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
N : Type u_4
inst✝¹² : Ring R✝
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ P
inst✝⁶ : Module R✝ N
R : Type u_5
ι : Type u_6
inst✝⁵ : Finite ι
α : Type u_6
inst✝⁴ : Fintype α
ih :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
M : Option α → Type u_7
inst✝³ : Ring R
inst✝² : (i : Option α) → AddCommGroup (M i)
inst✝¹ : (i : Option α) → Module R (M i)
inst✝ : ∀ (i : Option α), IsArtinian R (M i)
this :
  ∀ {M : α → Type u_7} [inst : Ring R] [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)]
    [inst_3 : ∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)
⊢ IsArtinian R ((i : Option α) → M i)
[PROOFSTEP]
exact isArtinian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
⊢ Set.Finite s
[PROOFSTEP]
refine'
  by_contradiction fun hf =>
    (RelEmbedding.wellFounded_iff_no_descending_seq.1 (wellFounded_submodule_lt (R := R) (M := M))).elim' _
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
[PROOFSTEP]
have f : ℕ ↪ s := Set.Infinite.natEmbedding s hf
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
[PROOFSTEP]
have : ∀ n, (↑) ∘ f '' {m | n ≤ m} ⊆ s := by
  rintro n x ⟨y, _, rfl⟩
  exact (f y).2
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
⊢ ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
[PROOFSTEP]
rintro n x ⟨y, _, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
n y : ℕ
left✝ : y ∈ {m | n ≤ m}
⊢ (Subtype.val ∘ ↑f) y ∈ s
[PROOFSTEP]
exact (f y).2
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
[PROOFSTEP]
have : ∀ a b : ℕ, a ≤ b ↔ span R (Subtype.val ∘ f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ f '' {m | a ≤ m}) :=
  by
  intro a b
  rw [span_le_span_iff hs (this b) (this a), Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective),
    Set.subset_def]
  simp only [Set.mem_setOf_eq]
  exact ⟨fun hab x => le_trans hab, fun h => h _ le_rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
⊢ ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
[PROOFSTEP]
rw [span_le_span_iff hs (this b) (this a), Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective),
  Set.subset_def]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ ∀ (x : ℕ), x ∈ {m | b ≤ m} → x ∈ {m | a ≤ m}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ ∀ (x : ℕ), b ≤ x → a ≤ x
[PROOFSTEP]
exact ⟨fun hab x => le_trans hab, fun h => h _ le_rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
[PROOFSTEP]
exact
  ⟨⟨fun n => span R (Subtype.val ∘ f '' {m | n ≤ m}), fun x y =>
      by
      rw [le_antisymm_iff, ← this y x, ← this x y]
      exact fun ⟨h₁, h₂⟩ => le_antisymm_iff.2 ⟨h₂, h₁⟩⟩,
    by
    intro a b
    conv_rhs => rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
x y : ℕ
⊢ (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) x = (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) y → x = y
[PROOFSTEP]
rw [le_antisymm_iff, ← this y x, ← this x y]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
x y : ℕ
⊢ y ≤ x ∧ x ≤ y → x = y
[PROOFSTEP]
exact fun ⟨h₁, h₂⟩ => le_antisymm_iff.2 ⟨h₂, h₁⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
⊢ ∀ {a b : ℕ},
    ↑{ toFun := fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m}),
              inj' :=
                (_ :
                  ∀ (x y : ℕ),
                    (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) x =
                        (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) y →
                      x = y) }
          a <
        ↑{ toFun := fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m}),
              inj' :=
                (_ :
                  ∀ (x y : ℕ),
                    (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) x =
                        (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) y →
                      x = y) }
          b ↔
      a > b
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
a b : ℕ
⊢ ↑{ toFun := fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m}),
            inj' :=
              (_ :
                ∀ (x y : ℕ),
                  (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) x =
                      (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) y →
                    x = y) }
        a <
      ↑{ toFun := fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m}),
            inj' :=
              (_ :
                ∀ (x y : ℕ),
                  (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) x =
                      (fun n => span R (Subtype.val ∘ ↑f '' {m | n ≤ m})) y →
                    x = y) }
        b ↔
    a > b
[PROOFSTEP]
conv_rhs => rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
a b : ℕ
| a > b
[PROOFSTEP]
rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
a b : ℕ
| a > b
[PROOFSTEP]
rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ↑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ↑f '' {m | a ≤ m})
a b : ℕ
| a > b
[PROOFSTEP]
rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), Set.Nonempty a → ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), I ∈ a → ¬I < M') ↔ IsArtinian R M
[PROOFSTEP]
rw [isArtinian_iff_wellFounded, WellFounded.wellFounded_iff_has_min]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ IsArtinian R M
[PROOFSTEP]
rw [isArtinian_iff_wellFounded]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
exact WellFounded.monotone_chain_condition.symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
[PROOFSTEP]
obtain ⟨n, w⟩ := monotone_stabilizes (f.iterateRange.comp ⟨fun n => n + 1, fun n m w => by linarith⟩)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n m : ℕ
w : n ≤ m
⊢ (fun n => n + 1) n ≤ (fun n => n + 1) m
[PROOFSTEP]
linarith
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateRange f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          n =
        ↑(OrderHom.comp (LinearMap.iterateRange f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          m
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
[PROOFSTEP]
specialize w (n + 1 + n) (by linarith)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateRange f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          n =
        ↑(OrderHom.comp (LinearMap.iterateRange f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          m
⊢ n ≤ n + 1 + n
[PROOFSTEP]
linarith
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w :
  ↑(OrderHom.comp (LinearMap.iterateRange f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      n =
    ↑(OrderHom.comp (LinearMap.iterateRange f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      (n + 1 + n)
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
[PROOFSTEP]
dsimp at w
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
[PROOFSTEP]
refine' ⟨n + 1, Nat.succ_ne_zero _, _⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊔ LinearMap.range (f ^ (n + 1)) = ⊤
[PROOFSTEP]
simp_rw [eq_top_iff', mem_sup]
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
⊢ ∀ (x : M), ∃ y, y ∈ LinearMap.ker (f ^ (n + 1)) ∧ ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ y + z = x
[PROOFSTEP]
intro x
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x : M
⊢ ∃ y, y ∈ LinearMap.ker (f ^ (n + 1)) ∧ ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ y + z = x
[PROOFSTEP]
have : (f ^ (n + 1)) x ∈ LinearMap.range (f ^ (n + 1 + n + 1)) :=
  by
  rw [← w]
  exact mem_range_self _
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x : M
⊢ ↑(f ^ (n + 1)) x ∈ LinearMap.range (f ^ (n + 1 + n + 1))
[PROOFSTEP]
rw [← w]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x : M
⊢ ↑(f ^ (n + 1)) x ∈ LinearMap.range (f ^ (n + 1))
[PROOFSTEP]
exact mem_range_self _
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x : M
this : ↑(f ^ (n + 1)) x ∈ LinearMap.range (f ^ (n + 1 + n + 1))
⊢ ∃ y, y ∈ LinearMap.ker (f ^ (n + 1)) ∧ ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ y + z = x
[PROOFSTEP]
rcases this with ⟨y, hy⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ ∃ y, y ∈ LinearMap.ker (f ^ (n + 1)) ∧ ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ y + z = x
[PROOFSTEP]
use x - (f ^ (n + 1)) y
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ x - ↑(f ^ (n + 1)) y ∈ LinearMap.ker (f ^ (n + 1)) ∧
    ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + z = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ x - ↑(f ^ (n + 1)) y ∈ LinearMap.ker (f ^ (n + 1))
[PROOFSTEP]
rw [LinearMap.mem_ker, LinearMap.map_sub, ← hy, sub_eq_zero, pow_add]
[GOAL]
case h.left
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ n * f ^ 1) (↑(f ^ n * f ^ 1) y)
[PROOFSTEP]
simp [pow_add]
[GOAL]
case h.right
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + z = x
[PROOFSTEP]
use(f ^ (n + 1)) y
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.range (f ^ (n + 1)) = LinearMap.range (f ^ (n + 1 + n + 1))
x y : M
hy : ↑(f ^ (n + 1 + n + 1)) y = ↑(f ^ (n + 1)) x
⊢ ↑(f ^ (n + 1)) y ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + ↑(f ^ (n + 1)) y = x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
⊢ Surjective ↑f
[PROOFSTEP]
obtain ⟨n, ne, w⟩ := exists_endomorphism_iterate_ker_sup_range_eq_top f
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
⊢ Surjective ↑f
[PROOFSTEP]
rw [LinearMap.ker_eq_bot.mpr (LinearMap.iterate_injective s n), bot_sup_eq, LinearMap.range_eq_top] at w
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : Surjective ↑(f ^ n)
⊢ Surjective ↑f
[PROOFSTEP]
exact LinearMap.surjective_of_iterate_surjective ne w
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
[PROOFSTEP]
rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
[PROOFSTEP]
use n + 1
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
⊢ ∀ (m : ℕ), n + 1 ≤ m → f m = ⊤
[PROOFSTEP]
rintro (_ | m) p
[GOAL]
case h.zero
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
p : n + 1 ≤ Nat.zero
⊢ f Nat.zero = ⊤
[PROOFSTEP]
cases p
[GOAL]
case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ f (Nat.succ m) = ⊤
[PROOFSTEP]
apply w
[GOAL]
case h.succ.a
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
[PROOFSTEP]
exact Nat.succ_le_succ_iff.mp p
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
[PROOFSTEP]
obtain ⟨n, w⟩ := monotone_stabilizes (partialSups (OrderDual.toDual ∘ f))
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ↑OrderDual.toDual f (m + 1) = ⊤
[PROOFSTEP]
refine' ⟨n, fun m p => _⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups (↑OrderDual.toDual ∘ f)) n) (↑OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups (↑OrderDual.toDual ∘ f)) n = ↑(partialSups (↑OrderDual.toDual ∘ f)) m
m : ℕ
p : n ≤ m
⊢ ↑OrderDual.toDual f (m + 1) = ⊤
[PROOFSTEP]
exact (h m).eq_bot_of_ge (sup_eq_left.1 <| (w (m + 1) <| le_add_right p).symm.trans <| w m p)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : ↑(r ^ m • LinearMap.id) y = x
⊢ ↑(r ^ n • LinearMap.id) (r ^ (m - n) • y) = x
[PROOFSTEP]
dsimp at hy ⊢
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x
[PROOFSTEP]
rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
[PROOFSTEP]
obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
[PROOFSTEP]
simp_rw [SetLike.ext_iff] at hn
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
[PROOFSTEP]
exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ y, r ^ Nat.succ n • y = r ^ n • x
[PROOFSTEP]
simpa using hn n.succ n.le_succ (r ^ n • x)
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : IsArtinian R M
⊢ IsArtinian S M
[PROOFSTEP]
rw [isArtinian_iff_wellFounded] at h ⊢
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : WellFounded fun x x_1 => x < x_1
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
refine' (Submodule.restrictScalarsEmbedding R S M).wellFounded h
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
⊢ IsArtinian R { x // x ∈ N }
[PROOFSTEP]
let ⟨s, hs⟩ := hN
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
⊢ IsArtinian R { x // x ∈ N }
[PROOFSTEP]
haveI := Classical.decEq M
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this : DecidableEq M
⊢ IsArtinian R { x // x ∈ N }
[PROOFSTEP]
haveI := Classical.decEq R
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝ : DecidableEq M
this : DecidableEq R
⊢ IsArtinian R { x // x ∈ N }
[PROOFSTEP]
have : ∀ x ∈ s, x ∈ N := fun x hx => hs ▸ Submodule.subset_span hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ IsArtinian R { x // x ∈ N }
[PROOFSTEP]
refine' @isArtinian_of_surjective _ ((↑s : Set M) →₀ R) N _ _ _ _ _ _ _ isArtinian_finsupp
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ (↑↑s →₀ R) →ₗ[R] { x // x ∈ N }
[PROOFSTEP]
exact Finsupp.total (↑s : Set M) N R (fun i => ⟨i, hs ▸ subset_span i.2⟩)
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑(Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) })
[PROOFSTEP]
rw [← LinearMap.range_eq_top, eq_top_iff, ←
  map_le_map_iff_of_injective (show Injective (Submodule.subtype N) from Subtype.val_injective), Submodule.map_top,
  range_subtype, ← Submodule.map_top, ← Submodule.map_comp, Submodule.map_top]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ N ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype N)
        (Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) }))
[PROOFSTEP]
subst N
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
⊢ span R ↑s ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype (span R ↑s))
        (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
[PROOFSTEP]
refine span_le.2 (fun i hi => ?_)
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ i ∈
    ↑(LinearMap.range
        (LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) })))
[PROOFSTEP]
use Finsupp.single ⟨i, hi⟩ 1
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ ↑(LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
      (Finsupp.single { val := i, property := hi } 1) =
    i
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : Ring R
S : Type u_2
inst✝¹ : Ring S
F : Type u_3
inst✝ : RingHomClass F R S
f : F
hf : Surjective ↑f
H : IsArtinianRing R
⊢ IsArtinianRing S
[PROOFSTEP]
rw [isArtinianRing_iff, isArtinian_iff_wellFounded] at H ⊢
[GOAL]
R : Type u_1
inst✝² : Ring R
S : Type u_2
inst✝¹ : Ring S
F : Type u_3
inst✝ : RingHomClass F R S
f : F
hf : Surjective ↑f
H : WellFounded fun x x_1 => x < x_1
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
exact (Ideal.orderEmbeddingOfSurjective f hf).wellFounded H
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson ⊥)
[PROOFSTEP]
let Jac := Ideal.jacobson (⊥ : Ideal R)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
⊢ IsNilpotent (Ideal.jacobson ⊥)
[PROOFSTEP]
let f : ℕ →o (Ideal R)ᵒᵈ := ⟨fun n => Jac ^ n, fun _ _ h => Ideal.pow_le_pow h⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
⊢ IsNilpotent (Ideal.jacobson ⊥)
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → Jac ^ n = Jac ^ m := IsArtinian.monotone_stabilizes f
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ IsNilpotent (Ideal.jacobson ⊥)
[PROOFSTEP]
refine' ⟨n, _⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ Ideal.jacobson ⊥ ^ n = 0
[PROOFSTEP]
let J : Ideal R := annihilator (Jac ^ n)
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ Ideal.jacobson ⊥ ^ n = 0
[PROOFSTEP]
suffices J = ⊤ by
  have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n)
  simpa only [this, top_smul, Ideal.zero_eq_bot] using hJ
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
this : J = ⊤
⊢ Ideal.jacobson ⊥ ^ n = 0
[PROOFSTEP]
have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
this : J = ⊤
hJ : J • Jac ^ n = ⊥
⊢ Ideal.jacobson ⊥ ^ n = 0
[PROOFSTEP]
simpa only [this, top_smul, Ideal.zero_eq_bot] using hJ
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ J = ⊤
[PROOFSTEP]
by_contra hJ
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : ¬J = ⊤
⊢ False
[PROOFSTEP]
change J ≠ ⊤ at hJ
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
⊢ False
[PROOFSTEP]
rcases IsArtinian.set_has_minimal {J' : Ideal R | J < J'} ⟨⊤, hJ.lt_top⟩ with
  ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → ¬I < J'⟩
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
⊢ False
[PROOFSTEP]
rcases SetLike.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ False
[PROOFSTEP]
obtain rfl : J ⊔ Ideal.span { x } = J' :=
  by
  apply eq_of_le_of_not_lt _ (hJ' (J ⊔ Ideal.span { x }) _)
  · exact sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))
  · rw [SetLike.lt_iff_le_and_exists]
    exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ⊔ Ideal.span {x} = J'
[PROOFSTEP]
apply eq_of_le_of_not_lt _ (hJ' (J ⊔ Ideal.span { x }) _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ⊔ Ideal.span {x} ≤ J'
[PROOFSTEP]
exact sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J < J ⊔ Ideal.span {x}
[PROOFSTEP]
rw [SetLike.lt_iff_le_and_exists]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ≤ J ⊔ Ideal.span {x} ∧ ∃ x_1, x_1 ∈ J ⊔ Ideal.span {x} ∧ ¬x_1 ∈ J
[PROOFSTEP]
exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
⊢ False
[PROOFSTEP]
have : J ⊔ Jac • Ideal.span { x } ≤ J ⊔ Ideal.span { x } :=
  sup_le_sup_left (smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
⊢ False
[PROOFSTEP]
have : Jac * Ideal.span { x } ≤ J := by
  -- Need version 4 of Nakayama's lemma on Stacks
  by_contra H
  refine' H (smul_sup_le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl (this.eq_of_not_lt (hJ' _ _)).ge)
  exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
⊢ Jac * Ideal.span {x} ≤ J
[PROOFSTEP]
by_contra H
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ False
[PROOFSTEP]
refine' H (smul_sup_le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl (this.eq_of_not_lt (hJ' _ _)).ge)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ J < J ⊔ Jac • Ideal.span {x}
[PROOFSTEP]
exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ False
[PROOFSTEP]
have : Ideal.span { x } * Jac ^ (n + 1) ≤ ⊥
[GOAL]
case this
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
[PROOFSTEP]
calc
  Ideal.span { x } * Jac ^ (n + 1) = Ideal.span { x } * Jac * Jac ^ n := by rw [pow_succ, ← mul_assoc]
  _ ≤ J * Jac ^ n := (mul_le_mul (by rwa [mul_comm]) le_rfl)
  _ = ⊥ := by simp
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ^ (n + 1) = Ideal.span {x} * Jac * Jac ^ n
[PROOFSTEP]
rw [pow_succ, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ≤ J
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ J * Jac ^ n = ⊥
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
[PROOFSTEP]
refine' hxJ (mem_annihilator.2 fun y hy => (mem_bot R).1 _)
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ x • y ∈ ⊥
[PROOFSTEP]
refine' this (mul_mem_mul (mem_span_singleton_self x) _)
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ y ∈ Jac ^ (n + 1)
[PROOFSTEP]
rwa [← hn (n + 1) (Nat.le_succ _)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
⊢ ∃ b, x * b = 1
[PROOFSTEP]
have : IsArtinianRing (R ⧸ p) := (@Ideal.Quotient.mk_surjective R _ p).isArtinianRing
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
⊢ ∃ b, x * b = 1
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ (n : ℕ), Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
⊢ ∃ n, Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
[PROOFSTEP]
obtain ⟨n, h⟩ :=
  IsArtinian.monotone_stabilizes (R := R ⧸ p) (M := R ⧸ p)
    ⟨fun m => OrderDual.toDual (Ideal.span {x ^ m}), fun m n h y hy =>
      by
      dsimp [OrderDual.toDual] at *
      rw [Ideal.mem_span_singleton] at hy ⊢
      obtain ⟨z, rfl⟩ := hy
      exact dvd_mul_of_dvd_left (pow_dvd_pow _ h) _⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
m n : ℕ
h : m ≤ n
y : R ⧸ p
hy : y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) n
⊢ y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) m
[PROOFSTEP]
dsimp [OrderDual.toDual] at *
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : ¬x = 0
this : IsArtinianRing (R ⧸ p)
m n : ℕ
h : m ≤ n
y : R ⧸ p
hy : y ∈ Ideal.span {x ^ n}
⊢ y ∈ Ideal.span {x ^ m}
[PROOFSTEP]
rw [Ideal.mem_span_singleton] at hy ⊢
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : ¬x = 0
this : IsArtinianRing (R ⧸ p)
m n : ℕ
h : m ≤ n
y : R ⧸ p
hy : x ^ n ∣ y
⊢ x ^ m ∣ y
[PROOFSTEP]
obtain ⟨z, rfl⟩ := hy
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : ¬x = 0
this : IsArtinianRing (R ⧸ p)
m n : ℕ
h : m ≤ n
z : R ⧸ p
⊢ x ^ m ∣ x ^ n * z
[PROOFSTEP]
exact dvd_mul_of_dvd_left (pow_dvd_pow _ h) _
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
h :
  ∀ (m : ℕ),
    n ≤ m →
      ↑{ toFun := fun m => ↑OrderDual.toDual (Ideal.span {x ^ m}),
              monotone' :=
                (_ :
                  ∀ (m n : ℕ),
                    m ≤ n →
                      ∀ (y : R ⧸ p),
                        y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) n →
                          y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) m) }
          n =
        ↑{ toFun := fun m => ↑OrderDual.toDual (Ideal.span {x ^ m}),
              monotone' :=
                (_ :
                  ∀ (m n : ℕ),
                    m ≤ n →
                      ∀ (y : R ⧸ p),
                        y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) n →
                          y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) m) }
          m
⊢ ∃ n, Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
[PROOFSTEP]
exact ⟨n, h (n + 1) <| by norm_num⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
h :
  ∀ (m : ℕ),
    n ≤ m →
      ↑{ toFun := fun m => ↑OrderDual.toDual (Ideal.span {x ^ m}),
              monotone' :=
                (_ :
                  ∀ (m n : ℕ),
                    m ≤ n →
                      ∀ (y : R ⧸ p),
                        y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) n →
                          y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) m) }
          n =
        ↑{ toFun := fun m => ↑OrderDual.toDual (Ideal.span {x ^ m}),
              monotone' :=
                (_ :
                  ∀ (m n : ℕ),
                    m ≤ n →
                      ∀ (y : R ⧸ p),
                        y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) n →
                          y ∈ (fun m => ↑OrderDual.toDual (Ideal.span {x ^ m})) m) }
          m
⊢ n ≤ n + 1
[PROOFSTEP]
norm_num
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
⊢ ∃ b, x * b = 1
[PROOFSTEP]
have H : x ^ n ∈ Ideal.span {x ^ (n + 1)}
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
⊢ x ^ n ∈ Ideal.span {x ^ (n + 1)}
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
H : x ^ n ∈ Ideal.span {x ^ (n + 1)}
⊢ ∃ b, x * b = 1
[PROOFSTEP]
{rw [← hn]; refine Submodule.subset_span (Set.mem_singleton _)
}
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
⊢ x ^ n ∈ Ideal.span {x ^ (n + 1)}
[PROOFSTEP]
rw [← hn]
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
⊢ x ^ n ∈ Ideal.span {x ^ n}
[PROOFSTEP]
refine Submodule.subset_span (Set.mem_singleton _)
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
H : x ^ n ∈ Ideal.span {x ^ (n + 1)}
⊢ ∃ b, x * b = 1
[PROOFSTEP]
rw [Ideal.mem_span_singleton] at H
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
H : x ^ (n + 1) ∣ x ^ n
⊢ ∃ b, x * b = 1
[PROOFSTEP]
obtain ⟨y, hy⟩ := H
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n = x ^ (n + 1) * y
⊢ ∃ b, x * b = 1
[PROOFSTEP]
rw [pow_add, mul_assoc, pow_one] at hy
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n = x ^ n * (x * y)
⊢ ∃ b, x * b = 1
[PROOFSTEP]
conv_lhs at hy => rw [← mul_one (x ^ n)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n = x ^ n * (x * y)
| x ^ n
[PROOFSTEP]
rw [← mul_one (x ^ n)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n = x ^ n * (x * y)
| x ^ n
[PROOFSTEP]
rw [← mul_one (x ^ n)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n = x ^ n * (x * y)
| x ^ n
[PROOFSTEP]
rw [← mul_one (x ^ n)]
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : Ideal.IsPrime p
x : R ⧸ p
hx : x ≠ 0
this : IsArtinianRing (R ⧸ p)
n : ℕ
hn : Ideal.span {x ^ n} = Ideal.span {x ^ (n + 1)}
y : R ⧸ p
hy : x ^ n * 1 = x ^ n * (x * y)
⊢ ∃ b, x * b = 1
[PROOFSTEP]
exact ⟨y, mul_left_cancel₀ (pow_ne_zero _ hx) hy.symm⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ Surjective ↑(algebraMap R L)
[PROOFSTEP]
intro r'
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, ↑(algebraMap R L) a = r'
[PROOFSTEP]
obtain ⟨r₁, s, rfl⟩ := IsLocalization.mk'_surjective S r'
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
[PROOFSTEP]
obtain ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
[PROOFSTEP]
swap
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
[PROOFSTEP]
exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ↑(algebraMap R L) (r₁ * r₂) = IsLocalization.mk' L r₁ s
[PROOFSTEP]
rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
use r
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
rw [smul_eq_mul, smul_eq_mul, pow_succ', mul_assoc] at hr
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
apply_fun algebraMap R L at hr
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑(algebraMap R L) (↑s ^ n * (↑s * r)) = ↑(algebraMap R L) (↑s ^ n * 1)
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
simp only [map_mul] at hr
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr :
  ↑(algebraMap R L) (↑s ^ n) * (↑(algebraMap R L) ↑s * ↑(algebraMap R L) r) =
    ↑(algebraMap R L) (↑s ^ n) * ↑(algebraMap R L) 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
[PROOFSTEP]
rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one, Submonoid.coe_one, ←
  (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul]