awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (hypothesis)
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 ⊤
⊢ ∃ (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
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ ∃ (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
have 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
Tactic: choose bM' hbM' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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
have rw : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
Tactic: rw [Matrix.represents_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (hypothesis)
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 (α := 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)
have 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)
Tactic: specialize hbM' (b j)
Cleared hypotheses: hbM'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
Cleared hypotheses: hbM'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (hypothesis)
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)
⊢ ∃ (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
have this : 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'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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
⊢ ∃ (a : ↥(isRepresentation R b)), (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) a = f
have 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
Tactic: obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ ∃ (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)
have 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)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (hypothesis)
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)) ⊤
⊢ ∃ (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)
have this : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)))) ⊤
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
Cleared hypotheses: f, hI
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ ∃ (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)
have 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)
Tactic: refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ 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)
have inr : Eq.{u_2 + 1} (α := Module.End R M)
  ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
        (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
      ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
    Module.End R M)
  ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
        (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
      0 :
    Module.End R M)
Tactic: rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ Eq.{u_2 + 1} (α := Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        0 :
      Module.End R M)
have inr : Eq (α := ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
  ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly :
    ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
  (0 : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ Eq (α := ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly :
      ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (0 : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have inr : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
  (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
    Matrix (↥s) (↥s) R)
  (↑0 : Matrix (↥s) (↥s) R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ⊤
⊢ Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Matrix (↥s) (↥s) R)
    (↑0 : Matrix (↥s) (↥s) R)
have inr : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
  ((aeval (↑A : Matrix (↥s) (↥s) R) : (a : R[X]) → Matrix (↥s) (↥s) R) (↑A : Matrix (↥s) (↥s) R).charpoly :
    Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
  ((↑0 : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
Tactic: rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((aeval (↑A : Matrix (↥s) (↥s) R) : (a : R[X]) → Matrix (↥s) (↥s) R) (↑A : Matrix (↥s) (↥s) R).charpoly :
      Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((↑0 : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
⊢ Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Matrix (↥s) (↥s) R)
    (↑0 : Matrix (↥s) (↥s) R)
have inr₁ : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) 0 (↑0 : Matrix (↥s) (↥s) R)
Tactic: rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]