-- 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
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) :=
  Basis.end (Free.chooseBasis R M)
g : (i : ι) → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  Eq (α := MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R)
        (((↑(bind₁ (toMvPolynomial b B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k)) :
      MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) 0 : MvPolynomial ι' R)
this :
  toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
    (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)
rwa :
  ∀
    (H :
      Eq (α := MvPolynomial ι' R)
        ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R)
            (((↑(bind₁ (toMvPolynomial b B φ)) :
                  MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
                (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
              (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k)) :
          MvPolynomial ι' R)
        (0 : MvPolynomial ι' R))
    (this :
      toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
        (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)),
    Eq (α := MvPolynomial ι' R)
      (((↑(bind₁ (toMvPolynomial b' B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R)
rwa₁ :
  ∀
    (H :
      Eq (α := MvPolynomial ι' R)
        ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R)
            ((bind₁ (toMvPolynomial b B φ) :
                (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
              (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k)) :
          MvPolynomial ι' R)
        (0 : MvPolynomial ι' R))
    (this :
      toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
        (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)),
    Eq (α := MvPolynomial ι' R)
      (((↑(bind₁ (toMvPolynomial b' B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R)
rwa₂ :
  ∀
    (H :
      Eq (α := MvPolynomial ι' R)
        ((bind₁ fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
                (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i) :
              (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
            (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
          MvPolynomial ι' R)
        (0 : MvPolynomial ι' R))
    (this :
      toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
        (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)),
    Eq (α := MvPolynomial ι' R)
      (((↑(bind₁ (toMvPolynomial b' B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R)
⊢ Eq (α := MvPolynomial ι' R)
    (((↑(bind₁ (toMvPolynomial b' B φ)) :
            MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
          (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
        (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
      MvPolynomial ι' R)
    (0 : MvPolynomial ι' R)
have rwa₃ : ∀
  (H :
    Eq (α := MvPolynomial ι' R)
      ((bind₁ (toMvPolynomial b' B φ) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R))
  (this :
    toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
      (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)),
  Eq (α := MvPolynomial ι' R)
    (((↑(bind₁ (toMvPolynomial b' B φ)) :
            MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
          (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
        (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
      MvPolynomial ι' R)
    (0 : MvPolynomial ι' R)
Tactic: rwa [map_zero, RingHom.coe_coe, MvPolynomial.bind₁_bind₁, ← this] at H
Cleared hypotheses: H, this