Tactic doesn't work in record syntax

Stream: general

[Adam Topaz]

Can anyone help me understand what's going on with the following code?

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

lemma foo : ![(1 : L),0] ≠ 0 := by tidy -- this works...

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := by tidy } -- this fails...

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := foo _ } -- this works

tidy very happily proves that $(1,0)$ is nonzero in the lemma foo, but it doesn't work in the second example.

[Kevin Buzzard]

goodness knows whether this is relevant, but the infoview says that the first goal is about a map fin 1.succ → L but the failure is about a map fin 2 → L

[Kevin Buzzard]

this is I think a red herring.

example : nonzero_vectors (fin (nat.succ 1) → L) :=
{ to_vec := ![1,0],
  nonzero := by tidy } -- this still fails...

[Kevin Buzzard]

example : ![(1 : L),0] ≠ 0 := by tidy? -- intros ᾰ, simp at *, assumption

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := by {intros x, simp at *, assumption} } -- simp fails...

[Kenny Lau]

https://www.diffchecker.com/xOMY4t91

[Kenny Lau]

the LHS is the version of ᾰ that fails; RHS is the version that succeeds

[Adam Topaz]

It this supposed to be read by a human?

[Kevin Buzzard]

example : ![(1 : L),0] ≠ 0 := by { intros x, simp at x, assumption }

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := by {intros x, simp at x, assumption} } -- simp fails...

[Kevin Buzzard]

example : ![(1 : L),0] ≠ 0 := begin
  intros x,
  simp only [one_ne_zero, matrix.cons_eq_zero_iff, false_and] at x,
  assumption
end

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := by {
    intros x,
    simp only [one_ne_zero, matrix.cons_eq_zero_iff, false_and] at x, -- fails
    assumption} }

[Kenny Lau]

this is the diff when I use (nat.succ $ nat.succ 0): https://www.diffchecker.com/CR8HCTXs

[Kenny Lau]

the diff is smaller, but still exists

[Adam Topaz]

I don't think it's about the 2 in fin 2. The second example works

[Kevin Buzzard]

Adam Topaz said:

It this supposed to be read by a human?

This is what kids who don't have diff do.

[Kenny Lau]

example : ![(1 : L),0] ≠ 0 :=
begin
  intros ᾰ,
  rw [matrix.cons_eq_zero_iff] at ᾰ, -- works
end

example : nonzero_vectors (fin (nat.succ $ nat.succ 0) → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros ᾰ,
    rw [matrix.cons_eq_zero_iff] at ᾰ, -- fails
  end
 }

[Adam Topaz]

I think this is related:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L]

abbreviation bar : fin 2 → L := ![1,0]
lemma foo : bar L ≠ 0 := by tidy -- this works...

@[reducible]
def baz : fin 2 → L := ![1,0]
lemma foo' : baz L ≠ 0 := by tidy -- this works...

def baz' : fin 2 → L := ![1,0]
lemma foo'' : baz' L ≠ 0 := by tidy -- this fails...

[Kevin Buzzard]

Fixed it for you:

example : nonzero_vectors (fin (0 : ℕ).succ.succ → L) :=
{ to_vec := ![1,0],
  nonzero := by {
    intros x,
    set goodzero :=
    (@has_zero.zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
       (@pi.has_zero.{0 0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))))
          (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L)
          (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))),
             @mul_zero_class.to_has_zero.{0} L
               (@monoid_with_zero.to_mul_zero_class.{0} L
                  (@semiring.to_monoid_with_zero.{0} L
                     (@ring.to_semiring.{0} L
                        (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_1))))))))
      with hgoodzero,
    set badzero :=
    (@has_zero.zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
       (@add_monoid.to_has_zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
          (@add_group.to_add_monoid.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
             (@add_comm_group.to_add_group.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
                (@pi.add_comm_group.{0 0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))))
                   (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L)
                   (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))),
                      @ring.to_add_comm_group.{0} L
                        (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_1))))))))
      with hbadzero,
    have : badzero = goodzero := rfl,
    rw this at x,
    tidy } }

[Kevin Buzzard]

variables (L : Type) [field L] (V : Type) [add_comm_group V] [vector_space L V]

[Reid Barton]

Kevin, you're not supposed to write the name ᾰ explicitly

[Kevin Buzzard]

That was Kenny! I'd never dream of doing that!

[Kevin Buzzard]

In fact the moment I saw his code I linted it, hoping that there was now an ᾰ linter.

[Kevin Buzzard]

oh no crap I just saw it in mine too :-/ Who put that there?

[Reid Barton]

We really should have gone with something like :nuclear:

[Kevin Buzzard]

Patrick claimed recently that we didn't need pp.all any more because the infoview would take care of everything, but it was very handy here. Of course I don't have a clue about the actual problem, namely that for some reason we have two different zeros.

[Kevin Buzzard]

Here's all the code. You can see after the two intros x that the types are slightly different -- this was Kenny's observation.

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type) [field L] (V : Type) [add_comm_group V] [vector_space L V]

@[ext]
structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

set_option pp.all true
example : ![(1 : L),0] ≠ 0 := begin
  intros x,
  rw matrix.cons_eq_zero_iff at x,
  simp only [one_ne_zero, matrix.cons_eq_zero_iff, false_and] at x,
  assumption
end

example : nonzero_vectors (fin (0 : ℕ).succ.succ → L) :=
{ to_vec := ![1,0],
  nonzero := by {
    intros x,
    set goodzero :=
    (@has_zero.zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
       (@pi.has_zero.{0 0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))))
          (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L)
          (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))),
             @mul_zero_class.to_has_zero.{0} L
               (@monoid_with_zero.to_mul_zero_class.{0} L
                  (@semiring.to_monoid_with_zero.{0} L
                     (@ring.to_semiring.{0} L
                        (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_1))))))))
      with hgoodzero,
    set badzero :=
    (@has_zero.zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
       (@add_monoid.to_has_zero.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
          (@add_group.to_add_monoid.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
             (@add_comm_group.to_add_group.{0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L)
                (@pi.add_comm_group.{0 0} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))))
                   (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L)
                   (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))),
                      @ring.to_add_comm_group.{0} L
                        (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_1))))))))
      with hbadzero,
    have : badzero = goodzero := rfl,
    rw this at x,
    tidy } }

[Kenny Lau]

Kevin Buzzard said:

this was Kenny's observation

This sounds like research-paper language to me

[Adam Topaz]

$$\text{[5] K. Lau, \emph{Private communication} (2020).}$$

[Adam Topaz]

fail

[Adam Topaz]

So do I understand correctly that the issue is with the 0 in \neq 0?

[Kevin Buzzard]

Yes that's my understanding too -- the RHS zeros are for some reason different.

[Adam Topaz]

This is less than ideal, but it works :expressionless:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L]

@[ext]
structure nonzero_vectors (n : ℕ) :=
(to_vec : fin n → L)
(nonzero : to_vec ≠ 0)

lemma foo : ![(1 : L),0] ≠ 0 := by tidy -- this works...

example : nonzero_vectors L 2 :=
{ to_vec := ![1,0],
  nonzero := by tidy }

[Adam Topaz]

Even better:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L]

@[ext]
structure nonzero_vectors (n : ℕ) :=
(to_vec : fin n → L)
(nonzero : to_vec ≠ 0 . obviously)

example : nonzero_vectors L 2 := ⟨![1,0]⟩

[Kevin Buzzard]

why are these things working but other things aren't working?

[Adam Topaz]

¯\_(ツ)_/¯

[Adam Topaz]

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L]

local attribute [reducible] has_zero.zero

@[ext]
structure nonzero_vectors (V : Type*) [add_comm_group V] [vector_space L V] :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

example : nonzero_vectors L (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    change _ ≠ 0, -- fail!?

  end}

[Adam Topaz]

The change line fails. not definitionally equal

[Kevin Buzzard]

So I guess what's happening is that when you make the structure

variables (L : Type) [field L] (V : Type) [add_comm_group V] [vector_space L V]

structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

the zero is coming from the fact that V is an add_comm_group. But here

example : ![(1 : L),0] ≠ 0 := begin
...

Lean knows that the vector space is fin 2 -> L and whilst this is an add_comm_group, the zero comes from pi.has_zero. These things are defeq so there are no diamond problems, but the problem is that the solution found by simp involves matrix.cons_eq_zero_iff which has the pi.has_zero zero. The rewrite shouldn't fail because the zeros are defeq, but for some reason it does fail -- this is not the first time I have seen rewrite failing under suspicious circumstances recently. Has there been a regression or something? Or am I talking nonsense?

[Adam Topaz]

I assume erw would work. It doesn't

[Adam Topaz]

But yes, that sounds like a reasonable conclusion.

[Adam Topaz]

But this doesn't really explain why change doesn't work.

[Kevin Buzzard]

The change fails because that 0 is 0 : nat. change doesn't try to do any unification with the goal, it's much more stupid than that. It interprets what you give it and then unifies afterwards.

[Adam Topaz]

Oh, right. I figured lean would be smart enough to replace 0 with has_zero.zero, but I guess not.

[Kevin Buzzard]

It's all about when elaboration happens I guess -- this is just something I've picked up over time. Before it attempts the change it decides it wants to figure out the type of 0 and because it doesn't have any other info, it goes for nat, and from then on we're doomed.

[Adam Topaz]

I'm still a little puzzled as to why foo0 works but not foo:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L]

lemma foo0 : ![(1 : L),0,0,0,0,0] ≠ 0 := by tidy

lemma foo {n} (v : fin n → L) : ![1,v] ≠ 0 :=
begin
  tidy,
  sorry,
end

[Kevin Buzzard]

Oh I don't think we've got to the bottom of this! I still don't understand why the rewrite fails.

[Adam Topaz]

To un-#xy things, I'm trying to mimic a (fairly technical) argument using classical projective spaces (i.e. projectivization of (fin n \to L)), so I'm happy to restrict myself to those vector spaces, at least for now.

[Kevin Buzzard]

I think tidy made a wrong turn in the foo proof above. If n=0 then probably the goal isn't solvable after tidy.

[Adam Topaz]

Note:

lemma foo {n} (v : fin n → L) : (matrix.vec_cons 1 v) ≠ 0 :=
begin
  tidy, -- works
end

[Reid Barton]

I would definitely suggest not using tidy as your proof when trying to debug something like this unless the problem is tidy-specific

[Kevin Buzzard]

oh it's nothing to do with tidy -- ![1,v] is being interpreted as two terms of type fin n -> F in the failing proof. foo isn't true I suspect.

[Reid Barton]

right, because n could be 0

[Adam Topaz]

But this fails:

lemma foo' {n} (v : fin n → L) : (fin.cons (1 : L) v : fin (n+1) → L) ≠ 0 :=
begin
  tidy,
end

[Adam Topaz]

And @Reid Barton I agree that we should not be using tidy, but the main thing I'm trying to accomplish with this is to have some (however rudimentary) automation for proving vectors are nonzero, so that working with projective spaces isn't as awful, and tidy seems like the best choice.

[Reid Barton]

Right but if there's some obscure elaboration issue going on, then getting rid of mysterious gadgets like tidy is the first step

[Reid Barton]

if tidy does the same thing in the working and non-working cases, study that thing

[Adam Topaz]

tidy isn't mysterious in this case. It just does intros a, simp at *, assumption

[Reid Barton]

if it does different things, then there's your problem

[Reid Barton]

great, so get rid of tidy asap

[Adam Topaz]

and the simp at * fails for the second one.

[Adam Topaz]

Looks like it has to do with matrix.cons_eq_zero_iff

[Adam Topaz]

So lean can't unify the fin.cons with matrix.vec_cons, I guess?

[Reid Barton]

and then try to figure out whether it's simp not trying to apply the lemma, or whether rw won't do it either, or whether explicitly using the lemma also fails, etc

[Reid Barton]

it sounds like you've already done this

[Kenny Lau]

Kenny Lau said:

example : ![(1 : L),0] ≠ 0 :=
begin
  intros ᾰ,
  rw [matrix.cons_eq_zero_iff] at ᾰ, -- works
end

example : nonzero_vectors (fin (nat.succ $ nat.succ 0) → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros ᾰ,
    rw [matrix.cons_eq_zero_iff] at ᾰ, -- fails
  end
 }

I already extracted the crucial component

[Adam Topaz]

Playing a bit more with @Kenny Lau 's examples:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

example : ![(1 : L),0] ≠ 0 :=
begin
  intros a,
  rw [matrix.cons_eq_zero_iff] at a, -- works
  finish,
end

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros a,
    -- "a : ![1,0] = 0" in context
    change _ = (0 : fin 2 → L) at a,
    -- "a : ![1,0] = 0" in context
    rw [matrix.cons_eq_zero_iff] at a, --works
    finish,
  end
 }

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros a,
    erw [matrix.cons_eq_zero_iff] at a, --fails
    sorry,
  end
 }

[Adam Topaz]

Here's a slightly more minimised version:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure zero_vectors :=
(to_vec : V)
(foo : to_vec = 0)

example : zero_vectors (fin 1 → L) :=
{ to_vec := ![0],
  foo := begin
    erw matrix.cons_eq_zero_iff, -- fails
  end }

example : zero_vectors (fin 1 → L) :=
{ to_vec := ![0],
  foo := begin
    change _ = (0 : fin 1 → L),
    rw matrix.cons_eq_zero_iff, -- works
    finish,
  end }

[Adam Topaz]

Okay, I think I'm starting to understand the issue here...

example : (![0] : fin 1 → L) = 0 := by refl -- fails

example : (![0] : fin 1 → L) = 0 :=
begin
  rw matrix.cons_eq_zero_iff,
  split,
  refl,
  rw eq_iff_true_of_subsingleton,
  tauto,
end

[Adam Topaz]

Where is has_zero (fin n \to L) defined?

[Adam Topaz]

docs#pi.has_zero

[Adam Topaz]

Well.... I don't know. I think for now I'll just hack it like this:

import algebra
import linear_algebra
import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure zero_vectors :=
(to_vec : V)
(foo : to_vec = 0 . obviously)

@[simp] lemma zero_eq {n} {α : Type*} [has_zero α] :
  (0 : fin (n + 1) → α) = matrix.vec_cons (0 : α) 0 := by tidy

example : zero_vectors (fin 1 → L) := { to_vec := ![0] }

[Adam Topaz]

Unfortunately, this hack doesn't work for nonzero_vectors.

[Kevin Buzzard]

import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

example : ![(1 : L),0] ≠ 0 := begin
  intros h,
  --  rw matrix.cons_eq_zero_iff at h, -- works
  simpa using h, -- uses `matrix.cons_eq_zero_iff`
end

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros h,
--    rw matrix.cons_eq_zero_iff at h, -- fails
--    rw @matrix.cons_eq_zero_iff L _ at h, -- fails
    rw @matrix.cons_eq_zero_iff L _ _ at h, -- works, presumably because Lean uses L's zero finally
    simpa using h,
  end }

[Adam Topaz]

import data.matrix.notation

variables (L : Type*) [field L] (V : Type*) [add_comm_group V] [vector_space L V]

@[ext]
structure nonzero_vectors :=
(to_vec : V)
(nonzero : to_vec ≠ 0)

open matrix

@[simp] lemma cons_eq_zero_iff' {n} {α} [has_zero α] {v : fin n → α} {x : α} :
  vec_cons x v = (λ _, 0) ↔ x = 0 ∧ v = 0 := cons_eq_zero_iff

example : nonzero_vectors (fin 2 → L) :=
{ to_vec := ![1,0],
  nonzero := begin
    intros h,
    --erw cons_eq_zero_iff at h, -- fails
    --rw cons_eq_zero_iff' at h, -- fails
    erw cons_eq_zero_iff' at h, -- works
    simpa using h,
  end }

[Kevin Buzzard]

My mental model of erw is "like rw, but tries harder to unify". However my mental model of what is actually going on with unification is poor.

[Kevin Buzzard]

simp only [cons_eq_zero_iff'] at h, fails. We need esimp (and esimpa)

[Adam Topaz]

Is it obvious what needs to be changed in cons_eq_zero_iff' to make rw work as opposed to erw? I think when rw works, then simp can apply it, but that's not the case with erw.

[Kevin Buzzard]

The "mistake" is not made by the lemma, my understanding of the issue is that unification has chosen a rather exotic zero for the right hand side of h, so somehow it's not the lemma's fault that we have to resort to eew

[Kevin Buzzard]

or whatever it's called

[Kevin Buzzard]

It used to work in Lean 4

[Adam Topaz]

Isn't there some way to write a simp lemma that would allow us to solve nonzeroin the example with by tidy?

[Adam Topaz]

I was hoping cons_eq_zero_iff' would do it, but no.

[Kevin Buzzard]

Oh I understand now, you're really trying to emulate the pi zero.

[Kevin Buzzard]

replace h := cons_eq_zero_iff'.1 h,

now works, but apparently this isn't good enough for rw. (oh -- the point is that not even this works with cons_eq_zero_iff -- I thought I'd posted some replace code but I ended up getting rw @ to work)

[Kevin Buzzard]

There's a way of turning on some trace messages so you can see exactly why it's failing...

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/your.20favourite.20set_option.20option/near/201825547

[Kevin Buzzard]

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

and then you can try and figure out why the rewrite is failing. I think.

[Adam Topaz]

Trace message

rewrite tactic failed, did not find instance of the pattern in the target expression
  _ = 0
state:
L : Type u_1,
_inst_1 : field L,
h : ![1, 0] = 0
⊢ false

[type_context.is_def_eq_detail] [1]: vec_cons ?m_3 ?m_4 = 0 =?= ![1, 0] = 0
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] [2]: vec_cons ?m_3 ?m_4 =?= ![1, 0]
[type_context.is_def_eq_detail] [3]: vec_cons =?= vec_cons
[type_context.is_def_eq_detail] process_assignment ?m_1 := L
[type_context.is_def_eq_detail] assign: ?m_1 := L
[type_context.is_def_eq_detail] process_assignment ?m_1 := 1
[type_context.is_def_eq_detail] assign: ?m_1 := 1
[type_context.is_def_eq_detail] process_assignment ?m_1 := 1
[type_context.is_def_eq_detail] assign: ?m_1 := 1
[type_context.is_def_eq_detail] process_assignment ?m_1 := ![0]
[type_context.is_def_eq_detail] [3]: fin ?m_1 =?= fin 1
[type_context.is_def_eq_detail] [4]: 1 =?= 1
[type_context.is_def_eq_detail] assign: ?m_1 := ![0]
[type_context.is_def_eq_detail] [2]: 0 =?= 0
[type_context.is_def_eq_detail] [3]: fin 1.succ =?= fin 2
[type_context.is_def_eq_detail] [4]: 1.succ =?= 2
[type_context.is_def_eq_detail] [3]: pi.has_zero =?= add_monoid.to_has_zero (fin 2 → L)
[type_context.is_def_eq_detail] [4]: {zero := λ (_x : fin 1.succ), 0} =?= {zero := add_monoid.zero (add_group.to_add_monoid (fin 2 → L))}
[type_context.is_def_eq_detail] [5]: λ (_x : fin 1.succ), 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [6]: λ (_x : fin 1.succ), 0 =?= add_group.zero
[type_context.is_def_eq_detail] [7]: λ (_x : fin 1.succ), 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [8]: λ (_x : fin 1.succ), 0 =?= 0
[type_context.is_def_eq_detail] [9]: 0 =?= 0
[type_context.is_def_eq_detail] [10]: (λ (ᾰ : fin 1.succ), L) _x =?= (λ (i : fin 2), (λ (ᾰ : fin 2), L) i) _x
[type_context.is_def_eq_detail] after whnf_core: L =?= L
[type_context.is_def_eq_detail] [10]: (λ (i : fin 1.succ), ?m_1) _x =?= (λ (i : fin 2), add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) i)) _x
[type_context.is_def_eq_detail] after whnf_core: ?m_1 =?= add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] process_assignment ?m_1 := add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] failed to assign ?m_1 to
add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
value contains local declaration _x which is not in the scope of the metavariable
[type_context.is_def_eq_detail] [10]: 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [11]: 0 =?= add_group.zero
[type_context.is_def_eq_detail] [12]: 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [13]: 0 =?= ring.zero
[type_context.is_def_eq_detail] [14]: 0 =?= division_ring.zero
[type_context.is_def_eq_detail] [15]: 0 =?= field.zero
[type_context.is_def_eq_detail] [16]: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: 0 =?= field.zero
[type_context.is_def_eq_detail] on failure: {zero := λ (_x : fin 1.succ), 0} =?= {zero := add_monoid.zero (add_group.to_add_monoid (fin 2 → L))}
[type_context.is_def_eq_detail] [3]: has_zero.zero =?= has_zero.zero
[type_context.is_def_eq_detail] [3]: fin ?m_1.succ =?= fin 2
[type_context.is_def_eq_detail] [4]: ?m_1.succ =?= 2
[type_context.is_def_eq_detail] [3]: pi.has_zero =?= add_monoid.to_has_zero (fin 2 → L)
[type_context.is_def_eq_detail] [4]: {zero := λ (_x : fin ?m_1.succ), 0} =?= {zero := add_monoid.zero (add_group.to_add_monoid (fin 2 → L))}
[type_context.is_def_eq_detail] [5]: has_zero.mk =?= has_zero.mk
[type_context.is_def_eq_detail] [5]: λ (_x : fin ?m_1.succ), 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [6]: λ (_x : fin ?m_1.succ), 0 =?= add_group.zero
[type_context.is_def_eq_detail] [7]: λ (_x : fin ?m_1.succ), 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [8]: λ (_x : fin ?m_1.succ), 0 =?= 0
[type_context.is_def_eq_detail] [9]: fin ?m_1.succ =?= fin 2
[type_context.is_def_eq_detail] [10]: ?m_1.succ =?= 2
[type_context.is_def_eq_detail] [9]: 0 =?= 0
[type_context.is_def_eq_detail] [10]: (λ (ᾰ : fin 1.succ), L) _x =?= (λ (i : fin 2), (λ (ᾰ : fin 2), L) i) _x
[type_context.is_def_eq_detail] after whnf_core: L =?= L
[type_context.is_def_eq_detail] [10]: (λ (i : fin 1.succ), ?m_1) _x =?= (λ (i : fin 2), add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) i)) _x
[type_context.is_def_eq_detail] after whnf_core: ?m_1 =?= add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] process_assignment ?m_1 := add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] failed to assign ?m_1 to
add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
value contains local declaration _x which is not in the scope of the metavariable
[type_context.is_def_eq_detail] [10]: 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [11]: 0 =?= add_group.zero
[type_context.is_def_eq_detail] [12]: 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [13]: 0 =?= ring.zero
[type_context.is_def_eq_detail] [14]: 0 =?= division_ring.zero
[type_context.is_def_eq_detail] [15]: 0 =?= field.zero
[type_context.is_def_eq_detail] [16]: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: 0 =?= field.zero
[type_context.is_def_eq_detail] on failure: {zero := λ (_x : fin ?m_1.succ), 0} =?= {zero := add_monoid.zero (add_group.to_add_monoid (fin 2 → L))}
[type_context.is_def_eq_detail] on failure: 0 =?= 0
[type_context.is_def_eq_detail] on failure: vec_cons ?m_3 ?m_4 = 0 =?= ![1, 0] = 0
[type_context.is_def_eq] vec_cons ?m_3 ?m_4 = 0 =?= ![1, 0] = 0 ... failed  (approximate mode)

[Kevin Buzzard]

With erw the trace indicates success here:

...
[type_context.is_def_eq_detail] [13]: 0 =?= field.zero
[type_context.is_def_eq_detail] [14]: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: 0 =?= field.zero
[type_context.is_def_eq_detail] synthesized instances on left
[type_context.is_def_eq_detail] [14]: 0 =?= field.zero
[type_context.is_def_eq_detail] [15]: mul_zero_class.zero =?= field.zero
[type_context.is_def_eq_detail] [16]: monoid_with_zero.zero =?= field.zero
[type_context.is_def_eq_detail] [17]: semiring.zero =?= field.zero
[type_context.is_def_eq_detail] [18]: ring.zero =?= field.zero
[type_context.is_def_eq_detail] [19]: division_ring.zero =?= field.zero
[type_context.is_def_eq_detail] [2]: fin ?m_1.succ =?= fin 2
[type_context.is_def_eq_detail] [3]: ?m_1.succ =?= 2
[type_context.is_def_eq] vec_cons ?m_3 ?m_4 = λ (_x : fin ?m_1.succ), 0 =?= ![1, 0] = 0 ... success  (approximate mode)

With rw the "synthesized instances on left" message never appears and the failure is

...
[type_context.is_def_eq_detail] [15]: 0 =?= field.zero
[type_context.is_def_eq_detail] [16]: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: 0 =?= field.zero
[type_context.is_def_eq_detail] on failure: {zero := λ (_x : fin 1.succ), 0} =?= {zero := add_monoid.zero (add_group.to_add_monoid (fin 2 → L))}
[type_context.is_def_eq_detail] [3]: λ (_x : fin 1.succ), 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [4]: λ (_x : fin 1.succ), 0 =?= add_group.zero
[type_context.is_def_eq_detail] [5]: λ (_x : fin 1.succ), 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [6]: λ (_x : fin 1.succ), 0 =?= 0
[type_context.is_def_eq_detail] [7]: 0 =?= 0
[type_context.is_def_eq_detail] [8]: (λ (ᾰ : fin 1.succ), L) _x =?= (λ (i : fin 2), (λ (ᾰ : fin 2), L) i) _x
[type_context.is_def_eq_detail] after whnf_core: L =?= L
[type_context.is_def_eq_detail] [8]: (λ (i : fin 1.succ), ?m_1) _x =?= (λ (i : fin 2), add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) i)) _x
[type_context.is_def_eq_detail] after whnf_core: ?m_1 =?= add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] process_assignment ?m_1 := add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
[type_context.is_def_eq_detail] failed to assign ?m_1 to
add_monoid.to_has_zero ((λ (ᾰ : fin 2), L) _x)
value contains local declaration _x which is not in the scope of the metavariable
[type_context.is_def_eq_detail] [8]: 0 =?= add_monoid.zero
[type_context.is_def_eq_detail] [9]: 0 =?= add_group.zero
[type_context.is_def_eq_detail] [10]: 0 =?= add_comm_group.zero
[type_context.is_def_eq_detail] [11]: 0 =?= ring.zero
[type_context.is_def_eq_detail] [12]: 0 =?= division_ring.zero
[type_context.is_def_eq_detail] [13]: 0 =?= field.zero
[type_context.is_def_eq_detail] [14]: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: has_zero.zero =?= field.zero
[type_context.is_def_eq_detail] on failure: 0 =?= field.zero
[type_context.is_def_eq_detail] on failure: vec_cons ?m_3 ?m_4 = 0 =?= ![1, 0] = 0
[type_context.is_def_eq] vec_cons ?m_3 ?m_4 = 0 =?= ![1, 0] = 0 ... failed  (approximate mode)

[Kevin Buzzard]

but now I'm at the limit of my understanding.