awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ 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)
have 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: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ 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)
have 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: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N)
have refine_1 : dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id
Tactic: refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N)
have refine_2 : dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id
Tactic: refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
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
⊢ 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
have this : Nonempty { l : ℕ // (↑l : ℕ∞) ≤ k }
Tactic: have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
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 }
⊢ 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
have this₁ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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
have simp_rw : Membership.mem (γ := Submodule R M)
    (({ toFun := fun (k : ℕ∞) ↦ ⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker,
            monotone' := sorry : ℕ∞ →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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
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 : ℕ∞
⊢ Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) fun (l : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦
    (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞)
have aux : Monotone (β := ℕ∞) fun (x : { l : ℕ // (↑l : ℕ∞) ≤ k }) ↦ (↑(↑x : ℕ) : ℕ∞)
Tactic: have aux : Monotone ((↑) : {l : ℕ // l ≤ k} → ℕ∞) := fun x y h ↦ by simpa using h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [mem_genEigenspace]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 : ℕ), LE.le (α := ℕ∞) (↑l : ℕ∞) (↑k : ℕ∞) ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker) ↔
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
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
⊢ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
have hl₁ : l ≤ k
Tactic: simp only [Nat.cast_le] at hl
Cleared hypotheses: hl