!4#4063 RingTheory.MatrixAlgebra

Stream: mathlib4

[Jeremy Tan]

!4#4063 I've got two remaining errors in this file, both regarding convert and failures to synthesise things with metavariables. Specifying implicit arguments, though, generates lots of unsolvable goals even if using 1 is put in

[Jeremy Tan]

so how can they be fixed?

[Jeremy Tan]

OK, one error has been fixed, but the other one will not budge

theorem right_inv (M : Matrix n n A) : (toFunAlgHom R A n) (invFun R A n M) = M := by
  simp only [invFun, AlgHom.map_sum, stdBasisMatrix, apply_ite ↑(algebraMap R A), smul_eq_mul,
    mul_boole, toFunAlgHom_apply, RingHom.map_zero, RingHom.map_one, Matrix.map_apply,
    Pi.smul_def]
  convert Finset.sum_product; apply matrix_eq_sum_std_basis

It may have to do with apply_ite ⇑(algebraMap R A) not working