awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
⊢ Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
have this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
Tactic: have := finrank_range_add_finrank_ker f
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
⊢ Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
have rw : f.ker = ⊥ ↔ f.range = ⊤
Tactic: rw [← ker_eq_bot, ← range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
⊢ f.ker = ⊥ ↔ f.range = ⊤
have refine_1 : ∀ (h : f.ker = ⊥), f.range = ⊤
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
refine_1 : ∀ (h : f.ker = ⊥), f.range = ⊤
⊢ f.ker = ⊥ ↔ f.range = ⊤
have refine_2 : ∀ (h : f.range = ⊤), f.ker = ⊥
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.ker = ⊥
⊢ f.range = ⊤
have this₁ : finrank.{u, v'} K ↥f.range = finrank K V₂
Tactic: rw [h, finrank_bot, add_zero, H] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥
have this₁ : finrank K V₂ + finrank.{u, v} K ↥f.ker = finrank K V₂
Tactic: rw [h, finrank_top, H] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw : f.ker = ⊥ ↔ Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
rw : f.ker = ⊥ ↔ Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw₁ : Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
  Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
rw : f.ker = ⊥ ↔ Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
rw₁ :
  Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw₂ : Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
  Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank.{u, v} K ↥U + finrank.{u, v} K ↥W = finrank K V
have rw : finrank.{u, v} K ↥⊤ = finrank K V
Tactic: rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
    add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ Eq (α := Submodule K V) (span K (Set.range b)) ⊤
have by_contra : ∀ (ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤), False
Tactic: by_contra ne_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤
⊢ False
have card_eq₁ : finrank.{u, v} K ↥(span K (Set.range b)) = finrank K V
Tactic: rw [← finrank_span_eq_card lin_ind] at card_eq
Cleared hypotheses: card_eq, ne_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ (⇑(basisOfPiSpaceOfLinearIndependent hb) : (a : ι) → ι → K) = b
have neg : (⇑(have this := sorry;
      Basis.empty (ι → K)) :
    (a : ι) → ι → K) =
  b
Tactic: rw [basisOfPiSpaceOfLinearIndependent, dif_neg hι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ (⇑(have this := ⋯;
        Basis.empty (ι → K)) :
      (a : ι) → ι → K) =
    b
have neg : ∀ (i x : ι),
  (have this := sorry;
        Basis.empty (ι → K) :
        (a : ι) → ι → K)
      i x =
    b i x
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent.{v, u, v} (ι := ↥s) K (Subtype.val (p := fun (x : V) ↦ x ∈ s))
card_eq : s.card = finrank K V
⊢ Eq.{v + 1} (α := (a : ↥s) → V) (⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) : (a : ↥s) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ s))
have this : Nonempty.{v + 1} ↥s
Tactic: haveI : Nonempty s := ⟨⟨hs.choose, hs.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
⊢ IsSimpleOrder.{v} (Submodule A V)
have this : Nontrivial V
Tactic: haveI := nontrivial_of_finrank_eq_succ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
⊢ IsSimpleOrder.{v} (Submodule A V)
have refine : ∀ (S : Submodule A V) (hn : ¬S = ⊥), S = ⊤
Tactic: refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
⊢ S = ⊤
have rw : ∀ (hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)),
  Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)
Tactic: rw [← restrictScalars_inj K] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
⊢ Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)
have this₁ : FiniteDimensional K V
Tactic: haveI : FiniteDimensional _ _ := .of_finrank_eq_succ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this_1 : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
this : FiniteDimensional K V
⊢ Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)
have refine : finrank K V ≤ finrank.{u, v} K ↥(restrictScalars K S)
Tactic: refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ S = ⊥ ∨ S = ⊤
have this : FiniteDimensional F E
Tactic: haveI : FiniteDimensional F E := .of_finrank_eq_succ hr
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ S = ⊥ ∨ S = ⊤
have this₁ : FiniteDimensional.{u_1, u_2} F ↥S
Tactic: haveI : FiniteDimensional F S :=
        FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ S = ⊥ ∨ S = ⊤
have this₁ : finrank.{u_1, u_2} F ↥S ≤ 2
Tactic: have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ S = ⊥ ∨ S = ⊤
have this₁ : 0 < finrank.{u_1, u_2} F ↥S
Tactic: have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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
⊢ S = ⊥ ∨ S = ⊤
have 1 : ∀ (h : finrank.{u_1, u_2} F ↥S = 1) (this : LE.le (α := ℕ) 1 2) (this : LT.lt (α := ℕ) 0 1), S = ⊥ ∨ S = ⊤
Tactic: interval_cases h : finrank F { x // x ∈ S }
Cleared hypotheses: this_3, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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 = ⊤
⊢ S = ⊥ ∨ S = ⊤
have 2 : ∀ (h : finrank.{u_1, u_2} F ↥S = 2) (this : LE.le (α := ℕ) 2 2) (this : LT.lt (α := ℕ) 0 2), S = ⊥ ∨ S = ⊤
Tactic: interval_cases h : finrank F { x // x ∈ S }
Cleared hypotheses: this_3, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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 = ⊥ ∨ S = ⊤
have 1 : S = ⊥
Tactic: left
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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
⊢ S = ⊥ ∨ S = ⊤
have 2 : S = ⊤
Tactic: right
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ S = ⊤
have h₁ : finrank.{u_1, u_2} F ↥S = finrank F E
Tactic: rw [← hr] at h
Cleared hypotheses: h, this_3, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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
⊢ S = ⊤
have 2 : Eq (α := Submodule F E) ((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) (⊤ : Submodule F E)
Tactic: rw [← Algebra.toSubmodule_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
have by_contra : ∀ (h_contra : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)), False
Tactic: by_contra h_contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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)
⊢ False
have h_contra₁ : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
Tactic: simp_rw [not_exists, not_and] at h_contra
Cleared hypotheses: h_contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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)
have refine : 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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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)
have rw : LinearMap.ker (f ^ n) ≤ LinearMap.ker (f * f ^ n)
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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
⊢ n + 1 ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ (n + 1)))
have h_ker_lt_ker : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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)
⊢ n + 1 ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ (n + 1)))
have h_finrank_lt_finrank : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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
⊢ n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
have zero : ∀ (hn : 0 ≤ (finrank K V).succ), 0 ≤ finrank.{u, v} K ↥(LinearMap.ker (HPow.hPow (β := ℕ) f 0))
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
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))
⊢ n ≤ finrank.{u, v} K ↥(LinearMap.ker (f ^ n))
have 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)))
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
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)
⊢ False
have h_le_ker_pow : ∀ 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