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) = ⊤
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) = ⊤
obtain ⟨n, w⟩ :=
  monotone_stabilizes (f.iterateRange.comp ⟨fun n => n + 1, fun n m w => by linarith⟩)
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) = ⊤
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) = ⊤
specialize w (n + 1 + n) (by linarith)
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) = ⊤
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) = ⊤
dsimp at w
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)) = ⊤
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) = ⊤
refine' ⟨n + 1, Nat.succ_ne_zero _, _⟩
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
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)) = ⊤
simp_rw [eq_top_iff', mem_sup]
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
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
intro x
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
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
have : (f ^ (n + 1)) x ∈ LinearMap.range (f ^ (n + 1 + n + 1)) := by
  rw [← w]
  exact mem_range_self _
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
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
rcases this with ⟨y, hy⟩
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
⊢ x - ↑(f ^ (n + 1)) y ∈ LinearMap.ker (f ^ (n + 1)) ∧
    ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + z = x
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
use x - (f ^ (n + 1)) y
case intro.intro.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))

case intro.intro.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
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
⊢ x - ↑(f ^ (n + 1)) y ∈ LinearMap.ker (f ^ (n + 1)) ∧
    ∃ z, z ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + z = x
constructor
no goals
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
linarith
no goals
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
linarith
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))
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))
rw [← w]
no goals
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))
exact mem_range_self _
case intro.intro.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)
case intro.intro.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))
rw [LinearMap.mem_ker, LinearMap.map_sub, ← hy, sub_eq_zero, pow_add]
no goals
case intro.intro.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)
simp [iterate_add_apply]
case intro.intro.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
⊢ ↑(f ^ (n + 1)) y ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + ↑(f ^ (n + 1)) y = x
case intro.intro.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
use (f ^ (n + 1)) y
no goals
case intro.intro.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
⊢ ↑(f ^ (n + 1)) y ∈ LinearMap.range (f ^ (n + 1)) ∧ x - ↑(f ^ (n + 1)) y + ↑(f ^ (n + 1)) y = x
simp