case intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
obtain ⟨k, h_k_le, hk⟩ :
  ∃ k, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) :=
  exists_ker_pow_eq_ker_pow_succ f
no goals
case intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
calc
  LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k))) := by
    rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
  _ = LinearMap.ker (f ^ k) := by rw [ker_pow_constant hk _]
  _ = LinearMap.ker (f ^ (k + (finrank K V - k))) := (ker_pow_constant hk (finrank K V - k))
  _ = LinearMap.ker (f ^ finrank K V) := by rw [add_tsub_cancel_of_le h_k_le]
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
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k)))
rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
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
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)
rw [ker_pow_constant hk _]
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
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)
rw [add_tsub_cancel_of_le h_k_le]