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
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))
⊢ False
have h_any_n_lt : ∀ 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 _)
-- 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 : (¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) → False
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)
-- 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
by_contra by_contra₁ 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)
have by_contra₃ : ∀ (h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)), False
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)
-- 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
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
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
have 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
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)
-- 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
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
⊢ ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
have 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
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)
-- 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
m : ℕ
hm : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
have 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)
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
-- 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
m : ℕ
hm : finrank K V ≤ m
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 ^ (k + (m - k)))
have rw : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ m)
Tactic: rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
-- 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
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)
have rw : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ (k + (m - k)))
Tactic: rw [ker_pow_constant hk _]
-- 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
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)
have rw : LinearMap.ker (f ^ finrank K V) = LinearMap.ker (f ^ finrank K V)
Tactic: rw [add_tsub_cancel_of_le h_k_le]
-- 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
m : ℕ
hm : finrank K V ≤ m
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)
have rw : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k)))
Tactic: 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]
-- 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
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 ^ m) = LinearMap.ker (f ^ (k + (m - k)))
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
have rw₁ : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)
Tactic: 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]
-- 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
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 ^ m) = LinearMap.ker (f ^ (k + (m - k)))
rw₁ : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
have rw₂ : LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)
Tactic: 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]
-- 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
m : ℕ
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
have pos : ∀ (h_cases : m < finrank K V), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
Tactic: by_cases! h_cases : m < finrank K V
-- 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
m : ℕ
pos : ∀ (h_cases : m < finrank K V), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
have neg : ∀ (h_cases : finrank K V ≤ m), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
Tactic: by_cases! h_cases : m < finrank K V
-- 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
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
have pos : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)
Tactic: rw [← add_tsub_cancel_of_le h_cases.le, add_comm, pow_add]
-- 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
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
have neg : LinearMap.ker (f ^ finrank K V) ≤ LinearMap.ker (f ^ finrank K V)
Tactic: rw [ker_pow_eq_ker_pow_finrank_of_le h_cases]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
⊢ FiniteDimensional.{u, v} K ↥(comap f p)
have grw : lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
Tactic: grw [FiniteDimensional, ← rank_lt_aleph0_iff, ← lift_lt, f.lift_rank_comap_le p, lift_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
have ha : lift.{v, v'} (Module.rank K ↥p) < ℵ₀
Tactic: apply add_lt_aleph0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
ha : lift.{v, v'} (Module.rank K ↥p) < ℵ₀
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
have hb : lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
Tactic: apply add_lt_aleph0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀
have ha : Module.rank K ↥p < ℵ₀
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
ha : Module.rank K ↥p < ℵ₀
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀
have ha₁ : Module.Finite.{u, v'} K ↥p
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
have hb : Module.rank K ↥f.ker < ℵ₀
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst_5 : FiniteDimensional.{u, v'} K ↥p
inst_6 : FiniteDimensional.{u, v} K ↥f.ker
hb : Module.rank K ↥f.ker < ℵ₀
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
have hb₁ : Module.Finite.{u, v} K ↥f.ker
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
⊢ FiniteDimensional.{u, v'} K (W ⧸ map f p)
have grw : lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
Tactic: grw [FiniteDimensional, ← rank_lt_aleph0_iff, ← lift_lt, f.lift_rank_quot_map_le p, lift_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
have ha : lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀
Tactic: apply add_lt_aleph0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
ha : lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
have hb : lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
Tactic: apply add_lt_aleph0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀
have ha : Module.rank K (W ⧸ f.range) < ℵ₀
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
ha : Module.rank K (W ⧸ f.range) < ℵ₀
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀
have ha₁ : Module.Finite.{u, v'} K (W ⧸ f.range)
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
have hb : Module.rank K (V ⧸ p) < ℵ₀
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
W : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup W
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K (V ⧸ p)
inst_6 : FiniteDimensional.{u, v'} K (W ⧸ f.range)
hb : Module.rank K (V ⧸ p) < ℵ₀
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
have hb₁ : Module.Finite.{u, v} K (V ⧸ p)
Tactic: rwa [lift_lt_aleph0, rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : MapsTo (⇑e : (a : M) → M) Φ Φ
⊢ IsOfFinOrder e
have he₁ : BijOn (⇑e : (a : M) → M) Φ Φ
Tactic: replace he : BijOn e Φ Φ := (hΦ₁.injOn_iff_bijOn_of_mapsTo he).mp e.injective.injOn
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
⊢ IsOfFinOrder e
have this : Finite.{u_2 + 1} (↑Φ : Type u_2)
Tactic: have : Finite Φ := finite_coe_iff.mpr hΦ₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
⊢ IsOfFinOrder e
have obtain : ∀ (k : ℕ) (hk₀ : k > 0) (hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1), IsOfFinOrder e
Tactic: obtain ⟨k, hk₀, hk⟩ := isOfFinOrder_of_finite e'
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
⊢ IsOfFinOrder e
have refine : IsPeriodicPt (fun (x : M ≃ₗ[R] M) ↦ e * x) k 1
Tactic: refine ⟨k, hk₀, ?_⟩