awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
simp :
  Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : ι,
      ∑ x_1 : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : ι) → R) i : R)
            ((Finsupp.single x_1 1 : (a : κ) → R) j : R))
          (b.coord x ⊗ₜ[R] c.coord x_1))
    (b.coord i ⊗ₜ[R] c.coord j)
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    ((dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R M ⊗[R] Dual R N)
        (((b.dualBasis.tensorProduct c.dualBasis : Basis (ι × κ) R (Dual R M ⊗[R] Dual R N)) :
            (a : ι × κ) → Dual R M ⊗[R] Dual R N)
          (i, j)) :
      Dual R M ⊗[R] Dual R N)
    ((LinearMap.id : (a : Dual R M ⊗[R] Dual R N) → Dual R M ⊗[R] Dual R N)
        (((b.dualBasis.tensorProduct c.dualBasis : Basis (ι × κ) R (Dual R M ⊗[R] Dual R N)) :
            (a : ι × κ) → Dual R M ⊗[R] Dual R N)
          (i, j)) :
      Dual R M ⊗[R] Dual R N)

Tactic:
simp only [Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
    dualDistribInvOfBasis_apply, dualDistrib_apply, Basis.coord_apply, Basis.repr_self,
    id_coe, id_eq]

Premises used: Module.Basis.tensorProduct_apply, Module.Basis.coe_dualBasis, LinearMap.id_coe, LinearMap.coe_comp, TensorProduct.dualDistribInvOfBasis_apply, Function.comp_apply, TensorProduct.dualDistrib_apply, Module.Basis.coord_apply, Module.Basis.repr_self, id_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
rw :
  HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
      (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
        ((Finsupp.single j 1 : (a : κ) → R) j : R))
      (b.coord i ⊗ₜ[R] c.coord j) =
    b.coord i ⊗ₜ[R] c.coord j
h₀ :
  ∀ (b_1 : κ),
    Membership.mem (γ := Finset κ) Finset.univ b_1 →
      b_1 ≠ j →
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
            (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
              ((Finsupp.single b_1 1 : (a : κ) → R) j : R))
            (b.coord i ⊗ₜ[R] c.coord b_1) =
          0
h₁ :
  j ∉ Finset.univ →
    HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
          ((Finsupp.single j 1 : (a : κ) → R) j : R))
        (b.coord i ⊗ₜ[R] c.coord j) =
      0
h₂ :
  ∀ (b_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ b_1 →
      b_1 ≠ i →
        Eq (α := Dual R M ⊗[R] Dual R N)
          (∑ x : κ,
            HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
              (HMul.hMul (α := R) (β := R) ((Finsupp.single b_1 1 : (a : ι) → R) i : R)
                ((Finsupp.single x 1 : (a : κ) → R) j : R))
              (b.coord b_1 ⊗ₜ[R] c.coord x))
          0
h₃ :
  i ∉ Finset.univ →
    Eq (α := Dual R M ⊗[R] Dual R N)
      (∑ x : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
            ((Finsupp.single x 1 : (a : κ) → R) j : R))
          (b.coord i ⊗ₜ[R] c.coord x))
      0
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : ι,
      ∑ x_1 : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : ι) → R) i : R)
            ((Finsupp.single x_1 1 : (a : κ) → R) j : R))
          (b.coord x ⊗ₜ[R] c.coord x_1))
    (b.coord i ⊗ₜ[R] c.coord j)

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
      (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
        ((Finsupp.single j 1 : (a : κ) → R) j : R))
      (b.coord i ⊗ₜ[R] c.coord j) =
    b.coord i ⊗ₜ[R] c.coord j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j b_1 : κ
h : Membership.mem (γ := Finset κ) Finset.univ b_1
h_1 : b_1 ≠ j
⊢ HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
      (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
        ((Finsupp.single b_1 1 : (a : κ) → R) j : R))
      (b.coord i ⊗ₜ[R] c.coord b_1) =
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h₀ h₁ :
  ∀ (b_1 : κ),
    Membership.mem (γ := Finset κ) Finset.univ b_1 →
      b_1 ≠ j →
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
            (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
              ((Finsupp.single b_1 1 : (a : κ) → R) j : R))
            (b.coord i ⊗ₜ[R] c.coord b_1) =
          0
⊢ ∀ (b_1 : κ),
    Membership.mem (γ := Finset κ) Finset.univ b_1 →
      b_1 ≠ j →
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
            (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
              ((Finsupp.single b_1 1 : (a : κ) → R) j : R))
            (b.coord i ⊗ₜ[R] c.coord b_1) =
          0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h : j ∉ Finset.univ
⊢ HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
      (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
        ((Finsupp.single j 1 : (a : κ) → R) j : R))
      (b.coord i ⊗ₜ[R] c.coord j) =
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h₁ h₂ :
  j ∉ Finset.univ →
    HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
          ((Finsupp.single j 1 : (a : κ) → R) j : R))
        (b.coord i ⊗ₜ[R] c.coord j) =
      0
⊢ j ∉ Finset.univ →
    HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
          ((Finsupp.single j 1 : (a : κ) → R) j : R))
        (b.coord i ⊗ₜ[R] c.coord j) =
      0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
b_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ b_1
h_1 : b_1 ≠ i
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : κ,
      HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single b_1 1 : (a : ι) → R) i : R)
          ((Finsupp.single x 1 : (a : κ) → R) j : R))
        (b.coord b_1 ⊗ₜ[R] c.coord x))
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h₀ h₁ :
  ∀ (b_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ b_1 →
      b_1 ≠ i →
        Eq (α := Dual R M ⊗[R] Dual R N)
          (∑ x : κ,
            HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
              (HMul.hMul (α := R) (β := R) ((Finsupp.single b_1 1 : (a : ι) → R) i : R)
                ((Finsupp.single x 1 : (a : κ) → R) j : R))
              (b.coord b_1 ⊗ₜ[R] c.coord x))
          0
⊢ ∀ (b_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ b_1 →
      b_1 ≠ i →
        Eq (α := Dual R M ⊗[R] Dual R N)
          (∑ x : κ,
            HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
              (HMul.hMul (α := R) (β := R) ((Finsupp.single b_1 1 : (a : ι) → R) i : R)
                ((Finsupp.single x 1 : (a : κ) → R) j : R))
              (b.coord b_1 ⊗ₜ[R] c.coord x))
          0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h : i ∉ Finset.univ
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : κ,
      HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
          ((Finsupp.single x 1 : (a : κ) → R) j : R))
        (b.coord i ⊗ₜ[R] c.coord x))
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
h₁ h₂ :
  i ∉ Finset.univ →
    Eq (α := Dual R M ⊗[R] Dual R N)
      (∑ x : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
            ((Finsupp.single x 1 : (a : κ) → R) j : R))
          (b.coord i ⊗ₜ[R] c.coord x))
      0
⊢ i ∉ Finset.univ →
    Eq (α := Dual R M ⊗[R] Dual R N)
      (∑ x : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
            ((Finsupp.single x 1 : (a : κ) → R) j : R))
          (b.coord i ⊗ₜ[R] c.coord x))
      0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
refine_1 : dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id
refine_2 : dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id
⊢ Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N)

Tactic:
refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_

Premises used: LinearEquiv.ofLinear, TensorProduct.dualDistrib, TensorProduct.dualDistribInvOfBasis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
dualDistrib_dualDistribInvOfBasis_left_inverse _ _

Premises used: TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
exact dualDistrib_dualDistribInvOfBasis_left_inverse _ _

Premises used: TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

Tactic:
dualDistrib_dualDistribInvOfBasis_right_inverse _ _

Premises used: TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

Tactic:
exact dualDistrib_dualDistribInvOfBasis_right_inverse _ _

Premises used: TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
⊢ Nonempty { l : ℕ // (↑l : ℕ∞) ≤ k }

Tactic:
have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le⟩⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l : ℕ // (↑l : ℕ∞) ≤ k }
m n : { i : ℕ // (↑i : ℕ∞) ≤ k }
h : m ≤ n
⊢ ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑m : ℕ)).ker ≤ ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑n : ℕ)).ker

Tactic:
simpa using (f - μ • 1).iterateKer.monotone h

Premises used: OrderHom.monotone, HSub.hSub, LinearMap.iterateKer, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l : ℕ // (↑l : ℕ∞) ≤ k }
⊢ Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) fun (i : { i : ℕ // (↑i : ℕ∞) ≤ k }) ↦
    ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑i : ℕ)).ker

Tactic:
have : Directed (ι := { i : ℕ // i ≤ k }) (· ≤ ·) fun i ↦ LinearMap.ker ((f - μ • 1) ^ (i : ℕ)) :=
    Monotone.directed_le fun m n h ↦ by simpa using (f - μ • 1).iterateKer.monotone h
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this_1 : Nonempty { l : ℕ // (↑l : ℕ∞) ≤ k }
this :
  Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) fun (i : { i : ℕ // (↑i : ℕ∞) ≤ k }) ↦
    ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑i : ℕ)).ker
simp_rw :
  Membership.mem (γ := Submodule R M)
      (({ toFun := fun (k : ℕ∞) ↦ ⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker,
              monotone' := ⋯ : ℕ∞ →o Submodule R M } :
            (a : ℕ∞) → Submodule R M)
          k :
        Submodule R M)
      x ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
simp_rw₁ :
  Membership.mem (γ := Submodule R M) (⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
      x ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
simp_rw₂ :
  Membership.mem (γ := Submodule R M) (⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
      x ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
simp_rw₃ :
  Membership.mem (γ := Submodule R M)
      (⨆ (x : { i : ℕ // (↑i : ℕ∞) ≤ k }), ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑x : ℕ)).ker) x ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
simp_rw₄ :
  (∃ (i : { i : ℕ // (↑i : ℕ∞) ≤ k }), x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑i : ℕ)).ker) ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
simp_rw₅ :
  (∃ (i : { i : ℕ // (↑i : ℕ∞) ≤ k }),
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑i : ℕ) : (a : M) → M) x : M) (0 : M)) ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
simp_rw₆ :
  (∃ (a : ℕ) (_ : (↑a : ℕ∞) ≤ k),
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ a : (a : M) → M) x : M) (0 : M)) ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ↔
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker

Tactic:
simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype',
    Submodule.mem_iSup_of_directed _ this, LinearMap.mem_ker, Subtype.exists, exists_prop]

Premises used: iSup_subtype', Subtype.exists, exists_prop, OrderHom.coe_mk, LinearMap.mem_ker, Module.End.genEigenspace, Submodule.mem_iSup_of_directed
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
x y : { l : ℕ // (↑l : ℕ∞) ≤ k }
h : x ≤ y
⊢ LE.le (α := ℕ∞) ((fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ ((↑(↑x : ℕ) : ℕ∞) : ℕ∞)) x)
    ((fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ ((↑(↑x : ℕ) : ℕ∞) : ℕ∞)) y)

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ Monotone (β := ℕ∞) fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ (↑(↑x : ℕ) : ℕ∞)

Tactic:
have aux : Monotone ((↑) : {l : ℕ // l ≤ k} → ℕ∞) := fun x y h ↦ by simpa using h
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
aux : Monotone (β := ℕ∞) fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ (↑(↑x : ℕ) : ℕ∞)
⊢ Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) fun (l : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦
    (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞)

Tactic:
((genEigenspace f μ).monotone.comp aux).directed_le

Premises used: OrderHom.monotone, Monotone.comp, Module.End.genEigenspace, Monotone.directed_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ∞
aux : Monotone (β := ℕ∞) fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ (↑(↑x : ℕ) : ℕ∞)
⊢ Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) fun (l : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦
    (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞)

Tactic:
exact ((genEigenspace f μ).monotone.comp aux).directed_le

Premises used: OrderHom.monotone, Monotone.comp, Module.End.genEigenspace, Monotone.directed_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
rw :
  (∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker) ↔
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ↔
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
rw [mem_genEigenspace]

Premises used: Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
mp :
  (∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker) →
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
mpr :
  x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker →
    ∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker) ↔
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
l : ℕ
hl : LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞)
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ l ≤ k

Tactic:
simp only [Nat.cast_le] at hl

Premises used: Nat.cast_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
l : ℕ
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hl : l ≤ k
⊢ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
(f - μ • 1).iterateKer.monotone hl hx

Premises used: OrderHom.monotone, Set.Mem, HSub.hSub, LinearMap.iterateKer, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
l : ℕ
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hl : l ≤ k
⊢ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
exact (f - μ • 1).iterateKer.monotone hl hx

Premises used: OrderHom.monotone, HSub.hSub, LinearMap.iterateKer, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
⊢ ∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker

Tactic:
⟨k, le_rfl, hx⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
⊢ ∃ (l : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker

Tactic:
exact ⟨k, le_rfl, hx⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) x ↔
    ∃ (k : ℕ), x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
simp [mem_genEigenspace]

Premises used: Module.End.mem_genEigenspace