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, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ False
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, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
by_contra h_contra
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
⊢ False
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, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ False
simp_rw [not_exists, not_and] at h_contra
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
h_le_ker_pow : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
h_any_n_lt : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K V
⊢ False
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
h_le_ker_pow : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
⊢ False
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 _)
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
h_le_ker_pow : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
h_any_n_lt : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K V
⊢ False
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
h_le_ker_pow : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
h_any_n_lt : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K V
⊢ False
show False
no goals
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
h_le_ker_pow : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
h_any_n_lt : ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K V
⊢ False
exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n : ℕ
hn : n ≤ Nat.succ (finrank K V)
⊢ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
⊢ ∀ (n : ℕ), n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
intro n hn
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n : ℕ
hn✝ : n ≤ Nat.succ (finrank K V)
hn : Nat.zero ≤ Nat.succ (finrank K V)
⊢ Nat.zero ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.zero) }

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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n : ℕ
hn : n ≤ Nat.succ (finrank K V)
⊢ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
induction' n with n ih
no goals
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n : ℕ
hn✝ : n ≤ Nat.succ (finrank K V)
hn : Nat.zero ≤ Nat.succ (finrank K V)
⊢ Nat.zero ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.zero) }
exact zero_le (finrank _ _)
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
h_finrank_lt_finrank :
  finrank K { x // x ∈ LinearMap.ker (f ^ n) } < finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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
no goals
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
h_finrank_lt_finrank :
  finrank K { x // x ∈ LinearMap.ker (f ^ n) } < finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
⊢ Nat.succ n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
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
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ Nat.succ n)
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
refine' lt_of_le_of_ne _ (h_contra n (Nat.le_of_succ_le_succ hn))
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ Nat.succ n)
rw [pow_succ]
no goals
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)
apply LinearMap.ker_le_ker_comp
no goals
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 : ℕ), x ≤ finrank K V → ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ Nat.succ x)
n✝ : ℕ
hn✝ : n✝ ≤ Nat.succ (finrank K V)
n : ℕ
ih : n ≤ Nat.succ (finrank K V) → n ≤ finrank K { x // x ∈ LinearMap.ker (f ^ n) }
hn : Nat.succ n ≤ Nat.succ (finrank K V)
h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ Nat.succ n)
⊢ finrank K { x // x ∈ LinearMap.ker (f ^ n) } < finrank K { x // x ∈ LinearMap.ker (f ^ Nat.succ n) }
apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker