-- 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)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V
⊢ False

Tactic:
exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)

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)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
⊢ False

Tactic:
have h_any_n_lt : ∀ n, n ≤ (finrank K V).succ → n ≤ finrank K V := fun n hn =>
  (h_le_ker_pow n hn).trans (Submodule.finrank_le _)

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)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V
⊢ False

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
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)
⊢ finrank K ↥(LinearMap.ker (f ^ n)) < finrank K ↥(LinearMap.ker (f ^ n.succ))

Tactic:
apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker

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
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Tactic:
by_contra h_contra

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 : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ False

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)
⊢ False

Tactic:
have h_le_ker_pow : ∀ n : ℕ, n ≤ (finrank K V).succ →
    n ≤ finrank K (LinearMap.ker (f ^ n)) := by
  intro n hn
  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:
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)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
⊢ False

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)
⊢ n + 1 ≤ finrank K ↥(LinearMap.ker (f ^ (n + 1)))

Tactic:
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

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)
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)))

Proof state:
case zero
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)
hn : 0 ≤ (finrank K V).succ
⊢ 0 ≤ finrank K ↥(LinearMap.ker (f ^ 0))

Tactic:
exact zero_le (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
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Tactic:
classical
  by_contra h_contra
  simp_rw [not_exists, not_and] at h_contra
  have h_le_ker_pow : ∀ n : ℕ, n ≤ (finrank K V).succ →
      n ≤ finrank K (LinearMap.ker (f ^ n)) := by
    intro n hn
    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
  have h_any_n_lt : ∀ n, n ≤ (finrank K V).succ → n ≤ finrank K V := fun n hn =>
    (h_le_ker_pow n hn).trans (Submodule.finrank_le _)
  show False
  exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)

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 : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ False

Tactic:
simp_rw [not_exists, not_and] at h_contra

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)
⊢ False