awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (finrank K V - k)))

Tactic:
ker_pow_constant hk (finrank K V - k)

Premises used: HSub.hSub, Module.End.ker_pow_constant, 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 ^ finrank K V) = LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)

Tactic:
rw [add_tsub_cancel_of_le h_k_le]

Premises used: 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 ^ m) = LinearMap.ker (f ^ (k + (m - k)))
rw₁ : LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)
rw₂ : LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ m) = 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]

Premises used: LinearMap.ker, HSub.hSub, HPow.hPow, HAdd.hAdd, Module.End.ker_pow_constant, 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 : ℕ
pos : ∀ (h_cases : m < finrank K V), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
neg : ∀ (h_cases : finrank K V ≤ m), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
by_cases! h_cases : m < finrank K V

Premises used: 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 : ℕ
h_cases : m < finrank K V
pos : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
rw [← add_tsub_cancel_of_le h_cases.le, add_comm, pow_add]

Premises used: pow_add, LT.lt.le, add_comm, 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 : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)

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
m : ℕ
h_cases : finrank K V ≤ m
neg neg₁ : LinearMap.ker (f ^ finrank K V) ≤ LinearMap.ker (f ^ finrank K V)
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
rw [ker_pow_eq_ker_pow_finrank_of_le h_cases]

Premises used: Module.End.ker_pow_eq_ker_pow_finrank_of_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
grw : lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
⊢ FiniteDimensional.{u, v} K ↥(comap f p)

Tactic:
grw [FiniteDimensional, ← rank_lt_aleph0_iff, ← lift_lt, f.lift_rank_comap_le p, lift_aleph0]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.lift_lt, FiniteDimensional, LinearMap.lift_rank_comap_le, Cardinal.lift_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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) < ℵ₀
hb : lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
apply add_lt_aleph0

Premises used: Cardinal.add_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 < ℵ₀
ha₁ ha₂ ha₃ ha₄ : Module.Finite.{u, v'} K ↥p
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 < ℵ₀
hb₁ hb₂ hb₃ hb₄ : Module.Finite.{u, v} K ↥f.ker
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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)
grw : lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
⊢ FiniteDimensional.{u, v'} K (W ⧸ map f p)

Tactic:
grw [FiniteDimensional, ← rank_lt_aleph0_iff, ← lift_lt, f.lift_rank_quot_map_le p, lift_aleph0]

Premises used: Module.rank_lt_aleph0_iff, LinearMap.lift_rank_quot_map_le, Cardinal.lift_lt, FiniteDimensional, Cardinal.lift_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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)) < ℵ₀
hb : lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
apply add_lt_aleph0

Premises used: Cardinal.add_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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) < ℵ₀
ha₁ ha₂ ha₃ ha₄ : Module.Finite.{u, v'} K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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) < ℵ₀
hb₁ hb₂ hb₃ hb₄ : Module.Finite.{u, v} K (V ⧸ p)
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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) Φ Φ
⊢ BijOn (⇑e : (a : M) → M) Φ Φ

Tactic:
replace he : BijOn e Φ Φ := (hΦ₁.injOn_iff_bijOn_of_mapsTo he).mp e.injective.injOn
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
⊢ Finite.{u_2 + 1} (↑Φ : Type u_2)

Tactic:
have : Finite Φ := finite_coe_iff.mpr hΦ₁
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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)
obtain :
  ∀ (k : ℕ) (hk₀ : k > 0) (hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1), IsOfFinOrder e
⊢ IsOfFinOrder e

Tactic:
obtain ⟨k, hk₀, hk⟩ := isOfFinOrder_of_finite e'

Premises used: isOfFinOrder_of_finite
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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

Tactic:
⟨k, hk₀, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Function.periodicPts, Exists.intro, IsOfFinOrder
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
refine : IsPeriodicPt (fun (x : M ≃ₗ[R] M) ↦ e * x) k 1
⊢ IsOfFinOrder e

Tactic:
refine ⟨k, hk₀, ?_⟩
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
h : ∀ (m : M), Eq (α := M) (((fun (x : M ≃ₗ[R] M) ↦ e * x)^[k] 1 : (a : M) → M) m : M) ((1 : (a : M) → M) m : M)
⊢ IsPeriodicPt (fun (x : M ≃ₗ[R] M) ↦ e * x) k 1

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
⊢ Membership.mem (γ := Submodule R M) (span R Φ) m

Tactic:
have hm : m ∈ span R Φ := hΦ₂ ▸ Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
h : (e ^ k : (a : M) → M) m = m
⊢ Eq (α := M) (((fun (x : M ≃ₗ[R] M) ↦ e * x)^[k] 1 : (a : M) → M) m : M) ((1 : (a : M) → M) m : M)

Tactic:
simp only [mul_left_iterate, mul_one, LinearEquiv.coe_one, id_eq]

Premises used: mul_left_iterate, LinearEquiv.coe_one, mul_one, id_eq
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
⊢ Eq (α := M) ((e ^ k : (a : M) → M) 0 : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x y : M
h : Membership.mem (γ := Submodule R M) (span R Φ) x
h_1 : Membership.mem (γ := Submodule R M) (span R Φ) y
hx : (e ^ k : (a : M) → M) x = x
hy : (e ^ k : (a : M) → M) y = y
⊢ (e ^ k : (a : M) → M) (x + y) = x + y

Tactic:
simp [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
t : R
x : M
h : Membership.mem (γ := Submodule R M) (span R Φ) x
hx : (e ^ k : (a : M) → M) x = x
⊢ (e ^ k : (a : M) → M) (t • x) = t • x

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
h : ∀ (x : M) (hx : x ∈ Φ), (e ^ k : (a : M) → M) x = x
⊢ (e ^ k : (a : M) → M) m = m

Tactic:
refine Submodule.span_induction (fun x hx ↦ ?_) (by simp)
    (fun x y _ _ hx hy ↦ by simp [map_add, hx, hy]) (fun t x _ hx ↦ by simp [hx]) hm
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
h : (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
⊢ (e ^ k : (a : M) → M) x = x

Tactic:
rw [LinearEquiv.pow_apply, ← he.1.coe_iterate_restrict ⟨x, hx⟩ k]

Premises used: Set.MapsTo.coe_iterate_restrict, Subtype.mk, And.left, LinearEquiv.pow_apply
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
⊢ e' ^ k = 1

Tactic:
simpa [IsPeriodicPt, IsFixedPt] using hk

Premises used: Function.IsPeriodicPt, Function.IsFixedPt
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
⊢ e' ^ k = 1

Tactic:
replace hk : (e') ^ k = 1 := by simpa [IsPeriodicPt, IsFixedPt] using hk
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk : e' ^ k = 1
⊢ Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))

Tactic:
replace hk := Equiv.congr_fun hk ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.FiniteSpan
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
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk :
  Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
h :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        id (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₁ :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₂ :
  ∀
    (hk :
      (↑((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) =
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : M)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₃ h₄ h₅ h₆ :
  ∀
    (hk :
      (↑((⇑e' : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2))^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) =
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : M)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x

Tactic:
rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk

Premises used: Equiv.Perm.coe_one, Subtype.ext_iff, Equiv.Perm.coe_pow, id_eq
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R : Type u_9
M : Type u_11
α : Type u_12
inst : Finite α
inst_1 : AddCommMonoid M
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : DecidableEq α
x : α
m : M
⊢ Eq (α := α → M) ((linearEquivFunOnFinite R M α : (a : α →₀ M) → α → M) (single x m) : α → M)
    (Pi.single (M := fun (j : α) ↦ M) x m : (j : α) → M)

Tactic:
equivFunOnFinite_single x m

Premises used: Finsupp.equivFunOnFinite_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R : Type u_9
M : Type u_11
α : Type u_12
inst : Finite α
inst_1 : AddCommMonoid M
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : DecidableEq α
x : α
m : M
⊢ Eq (α := α →₀ M)
    ((LinearEquiv.symm (linearEquivFunOnFinite R M α) : (a : α → M) → α →₀ M) (Pi.single (M := fun (a : α) ↦ M) x m) :
      α →₀ M)
    (single x m : α →₀ M)

Tactic:
equivFunOnFinite_symm_single x m

Premises used: Finsupp.equivFunOnFinite_symm_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R : Type u_9
M : Type u_11
α : Type u_12
inst : Finite α
inst_1 : AddCommMonoid M
inst_2 : Semiring R
inst_3 : Module R M
f : α →₀ M
⊢ (LinearEquiv.symm (linearEquivFunOnFinite R M α) : (a : α → M) → α →₀ M) (⇑f : (a : α) → M) = f

Tactic:
(linearEquivFunOnFinite R M α).symm_apply_apply f

Premises used: Finsupp.linearEquivFunOnFinite, LinearEquiv.symm_apply_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R : Type u_9
M : Type u_11
α : Type u_12
inst : Finite α
inst_1 : AddCommMonoid M
inst_2 : Semiring R
inst_3 : Module R M
f : α → M
⊢ (⇑((LinearEquiv.symm (linearEquivFunOnFinite R M α) : (a : α → M) → α →₀ M) f : α →₀ M) : (a : α) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N
h :
  ∀ (a : α) (b : M),
    Eq.{u_3 + 1} (α := N) ((φ : (a : α →₀ M) → N) (single a b) : N) ((ψ : (a : α →₀ M) → N) (single a b) : N)
⊢ φ = ψ

Tactic:
LinearMap.toAddMonoidHom_injective <| addHom_ext h

Premises used: LinearMap.toAddMonoidHom_injective, Finsupp.addHom_ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N
h : ∀ (a : α), φ ∘ₛₗ lsingle a = ψ ∘ₛₗ lsingle a
⊢ φ = ψ

Tactic:
lhom_ext fun a => LinearMap.congr_fun (h a)

Premises used: LinearMap.congr_fun, Finsupp.lhom_ext