awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this : FiniteDimensional F E
⊢ FiniteDimensional.{u_1, u_2} F ↥S

Tactic:
haveI : FiniteDimensional F S :=
        FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this : FiniteDimensional.{u_1, u_2} F ↥S
⊢ finrank.{u_1, u_2} F ↥S ≤ 2

Tactic:
have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
this : finrank.{u_1, u_2} F ↥S ≤ 2
⊢ 0 < finrank.{u_1, u_2} F ↥S

Tactic:
have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
this_3 : finrank.{u_1, u_2} F ↥S ≤ 2
this : 0 < finrank.{u_1, u_2} F ↥S
1 : ∀ (h : finrank.{u_1, u_2} F ↥S = 1) (this : LE.le (α := ℕ) 1 2) (this : LT.lt (α := ℕ) 0 1), S = ⊥ ∨ S = ⊤
2 : ∀ (h : finrank.{u_1, u_2} F ↥S = 2) (this : LE.le (α := ℕ) 2 2) (this : LT.lt (α := ℕ) 0 2), S = ⊥ ∨ S = ⊤
⊢ S = ⊥ ∨ S = ⊤

Tactic:
interval_cases h : finrank F { x // x ∈ S }

Premises used: Membership.mem, Subtype, Module.finrank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 1
this_3 : LE.le (α := ℕ) 1 2
this : LT.lt (α := ℕ) 0 1
1 : S = ⊥
⊢ S = ⊥ ∨ S = ⊤

Tactic:
left
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 1
this_3 : LE.le (α := ℕ) 1 2
this : LT.lt (α := ℕ) 0 1
⊢ S = ⊥

Tactic:
Subalgebra.eq_bot_of_finrank_one h

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 1
this_3 : LE.le (α := ℕ) 1 2
this : LT.lt (α := ℕ) 0 1
⊢ S = ⊥

Tactic:
exact Subalgebra.eq_bot_of_finrank_one h

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 2
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
2 : S = ⊤
⊢ S = ⊥ ∨ S = ⊤

Tactic:
right
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 2
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
⊢ finrank.{u_1, u_2} F ↥S = finrank F E

Tactic:
rw [← hr] at h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 2
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
h₁ : finrank.{u_1, u_2} F ↥S = finrank F E
⊢ LE.le (α := ℕ) 2 2

Tactic:
rw [← hr] at h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = 2
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
h₁ : finrank.{u_1, u_2} F ↥S = finrank F E
this₁ : LE.le (α := ℕ) 2 2
⊢ LT.lt (α := ℕ) 0 2

Tactic:
rw [← hr] at h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = finrank F E
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
2 : Eq (α := Submodule F E) ((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) (⊤ : Submodule F E)
⊢ S = ⊤

Tactic:
rw [← Algebra.toSubmodule_eq_top]

Premises used: Algebra.toSubmodule_eq_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = finrank F E
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
⊢ Eq (α := Submodule F E) ((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) (⊤ : Submodule F E)

Tactic:
eq_top_of_finrank_eq h

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
this_1 : FiniteDimensional F E
this_2 : FiniteDimensional.{u_1, u_2} F ↥S
h : finrank.{u_1, u_2} F ↥S = finrank F E
this_3 : LE.le (α := ℕ) 2 2
this : LT.lt (α := ℕ) 0 2
⊢ Eq (α := Submodule F E) ((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) (⊤ : Submodule F E)

Tactic:
exact eq_top_of_finrank_eq h

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
by_contra : ∀ (h_contra : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)), False
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Tactic:
by_contra h_contra
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)

Tactic:
simp_rw [not_exists, not_and] at h_contra

Premises used: not_exists, not_and
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} K ↥(LinearMap.ker (HPow.hPow (β := ℕ) f 0))

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} K ↥(LinearMap.ker (HPow.hPow (β := ℕ) f 0))

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)

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

Premises used: Nat.le_of_succ_le_succ, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
refine : LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ n.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))

Premises used: Nat.le_of_succ_le_succ, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
rw : LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)
⊢ LinearMap.ker (f ^ n) ≤ LinearMap.ker (f ^ n.succ)

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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

Premises used: LinearMap.ker_le_ker_comp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
hn : n + 1 ≤ (finrank K V).succ
⊢ LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ)

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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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.{u, v} K ↥(LinearMap.ker (f ^ n)) < finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))

Tactic:
apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker

Premises used: Submodule.finrank_lt_finrank_of_lt
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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.{u, v} K ↥(LinearMap.ker (f ^ n)) < finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))

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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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.{u, v} K ↥(LinearMap.ker (f ^ n)) < finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))
⊢ n.succ ≤ (finrank.{u, v} K ↥(LinearMap.ker (f ^ n))).succ

Tactic:
Nat.succ_le_succ (ih (Nat.le_of_succ_le hn))

Premises used: Nat.le_of_succ_le, Nat.succ_le_succ
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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.{u, v} K ↥(LinearMap.ker (f ^ n)) < finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))
⊢ (finrank.{u, v} K ↥(LinearMap.ker (f ^ n))).succ ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))

Tactic:
Nat.succ_le_of_lt h_finrank_lt_finrank

Premises used: Nat.succ_le_of_lt
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} 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.{u, v} K ↥(LinearMap.ker (f ^ n)) < finrank.{u, v} K ↥(LinearMap.ker (f ^ n.succ))
⊢ n + 1 ≤ finrank.{u, v} 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

Premises used: Nat.succ_le_of_lt, Nat.le_of_succ_le, LinearMap.ker, Membership.mem, Subtype, HPow.hPow, Nat.succ, Module.finrank, Nat.succ_le_succ
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
zero : ∀ (hn : 0 ≤ (finrank K V).succ), 0 ≤ finrank.{u, v} K ↥(LinearMap.ker (HPow.hPow (β := ℕ) f 0))
succ :
  ∀ (n : ℕ) (ih : ∀ (hn : n ≤ (finrank K V).succ), n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n)))
    (hn : n + 1 ≤ (finrank K V).succ), n + 1 ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ (n + 1)))
⊢ n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))

Tactic:
induction n with
      | zero => exact zero_le
      | 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

Premises used: zero_le, LinearMap.ker, Membership.mem, Subtype, HPow.hPow, Submodule.zero, Nat.succ, Module.finrank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} K ↥(LinearMap.ker (f ^ n))

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
      | 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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} K ↥(LinearMap.ker (f ^ n))
⊢ ∀ n ≤ (finrank K V).succ, n ≤ finrank K V

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 _)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} K ↥(LinearMap.ker (f ^ n))
h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V
⊢ False

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

Premises used: Nat.le_refl, Nat.succ, Module.finrank, Nat.not_succ_le_self
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u, v} 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)

Premises used: Nat.le_refl, Nat.succ, Module.finrank, Nat.not_succ_le_self
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
by_contra by_contra₁ by_contra₂ :
  ∀ (h_contra : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)), False
by_contra₃ : ∀ (h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)), False
by_contra₄ :
  ∀ (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.{u, v} K ↥(LinearMap.ker (f ^ n))), False
by_contra₅ :
  ∀ (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.{u, v} K ↥(LinearMap.ker (f ^ n)))
    (h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V), False
⊢ ∃ 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
      | 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 _)
    exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)

Premises used: not_exists, not_and
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Tactic:
exists_ker_pow_eq_ker_pow_succ f

Premises used: Module.End.exists_ker_pow_eq_ker_pow_succ
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
obtain :
  ∀ (k : ℕ) (h_k_le : k ≤ finrank K V) (hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)),
    LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

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

Premises used: Module.End.exists_ker_pow_eq_ker_pow_succ, Module.finrank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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 ^ k.succ)
rw rw₁ : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ m)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k)))

Tactic:
rw [add_tsub_cancel_of_le (h_k_le.trans hm)]

Premises used: LE.le.trans, add_tsub_cancel_of_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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 ^ k.succ)
rw : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ (k + (m - k)))
rw₁ : ℕ
rw₂ : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ (k + (m - k)))
rw₃ : ℕ
⊢ LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)

Tactic:
rw [ker_pow_constant hk _]

Premises used: Module.End.ker_pow_constant