awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
      (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij)
    (X ij)
rw :
  Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
⊢ Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
have rw₁ : Eq (α := MvPolynomial ι A)
  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
    (basis A bₘ.end) (baseChange A φ) ij)
  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
    (basis A bₘ.end) (baseChange A φ) ij)
Tactic: rw [this, bind₁_X_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
⊢ Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
have e_f : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
  (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
    (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij)
  (X ij)
Tactic: suffices toMvPolynomial (M₂ := (Module.End A (TensorProduct R A M)))
        (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij = X ij by
      rw [this, bind₁_X_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (∑ j : ιM × ιM,
      (monomial (Finsupp.single j 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij j))
    (X ij)
have rw : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
  ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
          (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
        (tensorProduct R A M M) ij ij) :
    MvPolynomial.{u_7, u_8} (ιM × ιM) A)
  (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
Tactic: rw [Finset.sum_eq_single ij]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (∑ j : ιM × ιM,
      (monomial (Finsupp.single j 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij j))
    (X ij)
have h₀ : ∀ (b : ιM × ιM),
  Membership.mem (γ := Finset (ιM × ιM)) Finset.univ b →
    b ≠ ij →
      Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
        ((monomial (Finsupp.single b 1) : (a : A) → MvPolynomial (ιM × ιM) A)
            ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
                (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
              (tensorProduct R A M M) ij b) :
          MvPolynomial.{u_7, u_8} (ιM × ιM) A)
        (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
Tactic: rw [Finset.sum_eq_single ij]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
h₀ :
  ∀ (b : ιM × ιM),
    Membership.mem (γ := Finset (ιM × ιM)) Finset.univ b →
      b ≠ ij →
        Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
          ((monomial (Finsupp.single b 1) : (a : A) → MvPolynomial (ιM × ιM) A)
              ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
                  (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
                (tensorProduct R A M M) ij b) :
            MvPolynomial.{u_7, u_8} (ιM × ιM) A)
          (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (∑ j : ιM × ιM,
      (monomial (Finsupp.single j 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij j))
    (X ij)
have h₁ : ij ∉ Finset.univ →
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
Tactic: rw [Finset.sum_eq_single ij]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have rw : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
  ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if ij = ij then 1 else 0)) (X ij)
Tactic: rw [this, if_pos rfl, X]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if ij = ij then 1 else 0)) (X ij)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have rw₁ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A) ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1)
  (X ij)
Tactic: rw [this, if_pos rfl, X]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if ij = ij then 1 else 0)) (X ij)
rw₁ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1) (X ij)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have rw₂ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A) ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1)
  ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1)
Tactic: rw [this, if_pos rfl, X]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
kl : ιM × ιM
H : kl ≠ ij
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have h₀ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
  ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if kl = ij then 1 else 0)) 0
Tactic: rw [this, if_neg H, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
kl : ιM × ιM
H : kl ≠ ij
h₀ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if kl = ij then 1 else 0)) 0
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have h₁ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A) ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) 0)
  0
Tactic: rw [this, if_neg H, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
kl : ιM × ιM
H : kl ≠ ij
h₀ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if kl = ij then 1 else 0)) 0
h₁ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) 0) 0
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
have h₂ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A) 0 0
Tactic: rw [this, if_neg H, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (∑ j : ιM × ιM,
      (monomial (Finsupp.single j 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij j))
    (X ij)
have e_f : ∀ (kl : ιM × ιM),
  Eq.{u_8 + 1} (α := A)
    ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
          (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
        (tensorProduct R A M M) ij kl :
      A)
    (if kl = ij then 1 else 0 : A)
Tactic: suffices ∀ kl,
        (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl =
        if kl = ij then 1 else 0 by
      rw [Finset.sum_eq_single ij]
      · rw [this, if_pos rfl, X]
      · rintro kl - H
        rw [this, if_neg H, map_zero]
      · grind
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij kl : ιM × ιM
⊢ Eq.{u_8 + 1} (α := A)
    ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
          (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
        (tensorProduct R A M M) ij kl :
      A)
    (if kl = ij then 1 else 0 : A)
have e_f : Eq.{u_8 + 1} (α := A)
  ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
            ((({
                      toFun := fun (a : A) ↦
                        HSMul.hSMul (β := (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M) a
                          (baseChangeHom R A M M),
                      map_add' := sorry, map_smul' := sorry } :
                    (a : A) → (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M)
                  1 :
                (a : M →ₗ[R] M) → TensorProduct R A M →ₗ[A] TensorProduct R A M)
              ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
          Finsupp.{u_7, u_8} (ιM × ιM) A) :
        (a : ιM × ιM) → A)
      ij :
    A)
  (if kl = ij then 1 else 0 : A)
Tactic: rw [toMatrix_apply, tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply,
      basis_apply, TensorProduct.lift.tmul, coe_restrictScalars]