case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateKer 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.iterateKer 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
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
obtain ⟨n, w⟩ :=
  monotone_stabilizes_iff_noetherian.mpr I
    (f.iterateKer.comp ⟨fun n => n + 1, fun n m w => by linarith⟩)
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ↑(OrderHom.comp (LinearMap.iterateKer 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.iterateKer f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      (2 * n + 1)
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateKer 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.iterateKer 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 (2 * n + 1) (by linarith only)
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ↑(OrderHom.comp (LinearMap.iterateKer 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.iterateKer f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      (2 * n + 1)
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
dsimp at w
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) = ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 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
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) ≤ ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) = ⊥
rw [eq_bot_iff]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ ↑(f ^ (n + 1)) y ∈ ⊥
case intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) ≤ ⊥
rintro - ⟨h, ⟨y, rfl⟩⟩
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ y ∈ LinearMap.ker (f ^ (2 * n + 1 + 1))
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ ↑(f ^ (n + 1)) y ∈ ⊥
rw [mem_bot, ← LinearMap.mem_ker, w]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) (↑(f ^ (n + 1)) y) = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ y ∈ LinearMap.ker (f ^ (2 * n + 1 + 1))
erw [LinearMap.mem_ker] at h⊢
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1) * f ^ (n + 1)) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) (↑(f ^ (n + 1)) y) = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
change (f ^ (n + 1) * f ^ (n + 1)) y = 0 at h
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1) * f ^ (n + 1)) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
rw [← pow_add] at h
case h.e'_2.h.e'_5.h.e'_6
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ 2 * n + 1 + 1 = n + 1 + (n + 1)
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
convert h using 3
no goals
case h.e'_2.h.e'_5.h.e'_6
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ 2 * n + 1 + 1 = n + 1 + (n + 1)
ring
no goals
R : Type u_1
M : Type u_2
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian 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
P : Type ?u.247455
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateKer 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.iterateKer f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          m
⊢ n ≤ 2 * n + 1
linarith only