!4#3274 typeclass instance problem

Stream: mathlib4

[Jeremy Tan]

!4#3274 there are two remaining instances of the typeclass instance problem being stuck here, can you help?

[Moritz Doll]

did you try the usual fixes?

[Moritz Doll]

(or as a better question: what is the offending code?)

[Jeremy Tan]

One of them is

theorem incMatrix_mul_transpose_apply_of_adj (h : G.Adj a b) :
    (G.incMatrix R ⬝ (G.incMatrix R)ᵀ) a b = (1 : R) := by
  classical
    simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
      Set.indicator_apply, Pi.one_apply, sum_boole]
    convert Nat.cast_one -- here
    convert card_singleton ⟦(a, b)⟧
    rw [← coe_eq_singleton, coe_filter_univ]
    exact G.incidenceSet_inter_incidenceSet_of_adj h

[Jeremy Tan]

The other is

theorem incMatrix_apply_eq_one_iff : G.incMatrix R a e = 1 ↔ e ∈ G.incidenceSet a := by
  convert one_ne_zero.ite_eq_left_iff -- here; I've tried @ on this to no avail
  infer_instance

[Moritz Doll]

ah yeah, that happens sometimes with convert. I usually rewrite the proofs to avoid convert.

[Moritz Doll]

I would not be surprised if the second one is just apply one_ne_zero.ite_eq_left_iff

[Jeremy Tan]

Moritz Doll said:

I would not be surprised if the second one is just apply one_ne_zero.ite_eq_left_iff

There's still an error with the one-line replacement:

failed to synthesize instance
  Decidable (e ∈ incidenceSet G a)

[Jeremy Tan]

(that error also showed up when I tried to do the @ on that)

[Jeremy Tan]

oh, the first problem (Nat.cast_one) is solved with convert @Nat.cast_one R _

[Jeremy Tan]

and now I fixed the other error, so it compiles now