awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ ∀ (x : M), Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : M) → M) x : M)

Tactic:
exact fun x => hI (LinearMap.mem_range_self f x)

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ ∀ (x : M),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Ideal.finsuppTotal ι M I b))
      ((f : (a : M) → M) x : M)

Tactic:
have : ∀ x, f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b) := by
    rw [Ideal.range_finsuppTotal, hb]
    exact fun x => hI (LinearMap.mem_range_self f x)
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
this :
  ∀ (x : M),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Ideal.finsuppTotal ι M I b))
      ((f : (a : M) → M) x : M)
choose :
  ∀ (bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I)
    (hbM' :
      ∀ (x : M),
        Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)),
    ∃ (M_1 : ↥(isRepresentation R b)),
      (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) M_1 = f ∧
        ∀ (i j : ι), (↑M_1 : Matrix ι ι R) i j ∈ I
⊢ ∃ (M_1 : ↥(isRepresentation R b)),
    (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) M_1 = f ∧ ∀ (i j : ι), (↑M_1 : Matrix ι ι R) i j ∈ I

Tactic:
choose bM' hbM' using this
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
rw : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
⊢ Represents b A f

Tactic:
rw [Matrix.represents_iff']

Premises used: Matrix.represents_iff'
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
dsimp :
  ∀ (j : ι),
    Eq (α := M) (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((bM' (b j) : (a : ι) → ↥I) i) : R) (b i) : M)
      ((f : (a : M) → M) (b j) : M)
⊢ ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)

Tactic:
dsimp [A]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
j : ι
⊢ Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' (b j)) : M) ((f : (a : M) → M) (b j) : M)

Tactic:
specialize hbM' (b j)
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
j : ι
hbM' :
  Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' (b j)) : M) ((f : (a : M) → M) (b j) : M)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hbM' :
      Eq (α := M) (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((bM' (b j) : (a : ι) → ↥I) i) : R) (b i) : M)
        ((f : (a : M) → M) (b j) : M)),
    Eq (α := M) (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((bM' (b j) : (a : ι) → ↥I) i) : R) (b i) : M)
      ((f : (a : M) → M) (b j) : M)
⊢ Eq (α := M) (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((bM' (b j) : (a : ι) → ↥I) i) : R) (b i) : M)
    ((f : (a : M) → M) (b j) : M)

Tactic:
rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'

Premises used: Ideal.finsuppTotal_apply_eq_of_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
⊢ Represents b A f

Tactic:
have : A.Represents b f := by
    rw [Matrix.represents_iff']
    dsimp [A]
    intro j
    specialize hbM' (b j)
    rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
this : Represents b A f
⊢ ∃ (M_1 : ↥(isRepresentation R b)),
    (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) M_1 = f ∧ ∀ (i j : ι), (↑M_1 : Matrix ι ι R) i j ∈ I

Tactic:
⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this,
      fun i j => (bM' (b j) i).prop⟩

Premises used: Subtype.mk, Subtype.prop, And.intro, Exists.intro, Matrix.isRepresentation.eq_toEnd_of_represents, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
bM' : (x : M) → Finsupp.{u_1, u_3} ι ↥I
hbM' :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := M) ((Ideal.finsuppTotal ι M I b : (a : ι →₀ ↥I) → M) (bM' x) : M) ((f : (a : M) → M) x : M)
A : Matrix ι ι R := fun (i j : ι) ↦ (↑((bM' (b j) : (a : ι) → ↥I) i) : R)
this : Represents b A f
⊢ ∃ (M_1 : ↥(isRepresentation R b)),
    (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) M_1 = f ∧ ∀ (i j : ι), (↑M_1 : Matrix ι ι R) i j ∈ I

Tactic:
exact
    ⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this,
      fun i j => (bM' (b j) i).prop⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
⊢ LinearMap.range f ≤ HSMul.hSMul.{u_3, u_2, u_2} (α := Ideal R) (β := Submodule R M) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
obtain :
  ∀ (M_1 : ↥(isRepresentation R b)) (e : (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) M_1 = f),
    ∃ (a : ↥(isRepresentation R b)), (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) a = f
⊢ ∃ (a : ↥(isRepresentation R b)), (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) a = f

Tactic:
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)

Premises used: Matrix.isRepresentation.toEnd_exists_mem_ideal, Top.top
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M_1 : Type u_2
inst_1 : AddCommGroup M_1
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M_1
b : ι → M_1
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M_1) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M_1
M : ↥(isRepresentation R b)
e : (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M_1) M = f
⊢ ∃ (a : ↥(isRepresentation R b)), (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M_1) a = f

Tactic:
⟨M, e⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M_1 : Type u_2
inst_1 : AddCommGroup M_1
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M_1
b : ι → M_1
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M_1) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M_1
M : ↥(isRepresentation R b)
e : (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M_1) M = f
⊢ ∃ (a : ↥(isRepresentation R b)), (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M_1) a = f

Tactic:
exact ⟨M, e⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr :
  Nontrivial R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Subsingleton R
⊢ Monic.{u_3} (R := R) 0 ∧
    natDegree.{u_3} (R := R) 0 = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
      (∀ (k : ℕ), coeff 0 k ∈ I ^ (natDegree.{u_3} (R := R) 0 - k)) ∧
        Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) 0) 0

Tactic:
simp [nontriviality]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Subsingleton R
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)

Tactic:
exact ⟨0, by simp [nontriviality]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Nontrivial R
inr :
  ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
    (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)

Tactic:
obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top

Premises used: Submodule.FG.exists_span_finset_card_eq_spanFinrank, Module.Finite.fg_top
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤

Tactic:
simp [hs_span]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤

Tactic:
have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
h : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
inr :
  ∀ (A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I)
    (hI :
      range (R := R) (M := M) (τ₁₂ := RingHom.id R)
          ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
              (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
            A) ≤
        HSMul.hSMul (β := Submodule R M) I ⊤),
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M)
              (((aeval
                        ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
                            (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
                          A) :
                      AlgHom.{u_3, u_3, u_2} R R[X] (Module.End R M)) :
                    (a : R[X]) → Module.End R M)
                  p :
                Module.End R M)
              (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)

Tactic:
obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI

Premises used: Matrix.isRepresentation.toEnd_exists_mem_ideal, Subtype.val, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
⊢ natDegree (↑A : Matrix (↥s) (↥s) R).charpoly = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤

Tactic:
simp [hs_card]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
⊢ ∀ (k : ℕ), coeff (↑A : Matrix (↥s) (↥s) R).charpoly k ∈ I ^ (natDegree (↑A : Matrix (↥s) (↥s) R).charpoly - k)

Tactic:
simpa using coeff_charpoly_mem_ideal_pow h

Premises used: Matrix.coeff_charpoly_mem_ideal_pow
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq.{u_2 + 1} (α := Module.End R M)
    (((aeval
              ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
                  (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
                A) :
            AlgHom.{u_3, u_3, u_2} R R[X] (Module.End R M)) :
          (a : R[X]) → Module.End R M)
        (↑A : Matrix (↥s) (↥s) R).charpoly :
      Module.End R M)
    (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M)
            (((aeval
                      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
                          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
                        A) :
                    AlgHom.{u_3, u_3, u_2} R R[X] (Module.End R M)) :
                  (a : R[X]) → Module.End R M)
                p :
              Module.End R M)
            (0 : Module.End R M)

Tactic:
refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩