-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem exists_ker_pow_eq_ker_pow_succ [FiniteDimensional K V] (f : End K V) :
    ∃ k : ℕ, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)

Tactic:
refine lt_of_le_of_ne ?_ (h_contra n (Nat.le_of_succ_le_succ hn))

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ n.succ)

Proof state:
case succ
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)
h_finrank_lt_finrank : finrank K ↥(LinearMap.ker (f ^ n)) < finrank K ↥(LinearMap.ker (f ^ n.succ))
⊢ n + 1 ≤ finrank K ↥(LinearMap.ker (f ^ (n + 1)))

Tactic:
calc
  n.succ ≤ (finrank K ↑(LinearMap.ker (f ^ n))).succ :=
    Nat.succ_le_succ (ih (Nat.le_of_succ_le hn))
  _ ≤ finrank K ↑(LinearMap.ker (f ^ n.succ)) := Nat.succ_le_of_lt h_finrank_lt_finrank

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
hn : n ≤ (finrank K V).succ
⊢ n ≤ finrank K ↥(LinearMap.ker (f ^ n))

Tactic:
induction n with
| zero => exact zero_le (finrank _ _)
| succ n ih =>
  have h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ) := by
    refine lt_of_le_of_ne ?_ (h_contra n (Nat.le_of_succ_le_succ hn))
    rw [pow_succ']
    apply LinearMap.ker_le_ker_comp
  have h_finrank_lt_finrank :
      finrank K (LinearMap.ker (f ^ n)) < finrank K (LinearMap.ker (f ^ n.succ)) := by
    apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker
  calc
    n.succ ≤ (finrank K ↑(LinearMap.ker (f ^ n))).succ :=
      Nat.succ_le_succ (ih (Nat.le_of_succ_le hn))
    _ ≤ finrank K ↑(LinearMap.ker (f ^ n.succ)) := Nat.succ_le_of_lt h_finrank_lt_finrank

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ n.succ)

Tactic:
rw [pow_succ']

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
⊢ ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))

Tactic:
intro n hn

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
hn : n ≤ (finrank K V).succ
⊢ n ≤ finrank K ↥(LinearMap.ker (f ^ n))

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)

Tactic:
apply LinearMap.ker_le_ker_comp

Result:
no goals

Proof state:
case succ
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ n + 1 ≤ finrank K ↥(LinearMap.ker (f ^ (n + 1)))

Tactic:
have h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ) := by
  refine lt_of_le_of_ne ?_ (h_contra n (Nat.le_of_succ_le_succ hn))
  rw [pow_succ']
  apply LinearMap.ker_le_ker_comp

Result:
case succ
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)
⊢ n + 1 ≤ finrank K ↥(LinearMap.ker (f ^ (n + 1)))