rfl not working, totally confused

Stream: general

[Johan Commelin]

import data.polynomial.degree.basic

noncomputable theory

namespace polynomial

variables {R : Type*} [semiring R] {f : polynomial R}

/-- erase_lead of a polynomial f is the polynomial obtained by
subtracting from f the leading term of f. -/
def erase_lead (f : polynomial R) : polynomial R :=
finsupp.erase f.nat_degree f

@[simp] lemma erase_lead_support (f : polynomial R) :
  f.erase_lead.support = f.support.erase f.nat_degree :=
rfl -- fails

end polynomial

[Johan Commelin]

@eq.{1} (finset.{0} nat)
 (@finset.erase.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b))
 (@finsupp.support.{0 u_1} nat R (@mul_zero_class.to_has_zero.{u_1} R (@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1))) f) (@polynomial.nat_degree.{u_1} R _inst_1 f))
 (@finset.erase.{0} nat nat.decidable_eq
 (@finsupp.support.{0 u_1} nat R (@mul_zero_class.to_has_zero.{u_1} R (@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1))) f) (@polynomial.nat_degree.{u_1} R _inst_1 f))

[Johan Commelin]

decidable eq issue on nat :angry_cat:

[Chris Hughes]

lhs is classical dec eq and rhs is honest dec eq on nat.

[Johan Commelin]

This is sad

[Johan Commelin]

I want

def tactic.interactive.RFL := `[by convert rfl]

[Chris Hughes]

convert might not even help when you have to unfold the lhs

[Johan Commelin]

It worked in this case :shrug:

[Eric Wieser]

Does changing finsupp to use less classical help with this type of thing?

[Johan Commelin]

I think we changed it to use more classical to help with this kind of thing :oops: :see_no_evil:

[Chris Hughes]

It's your fault for unfolding finsupp and not using the API.

[Johan Commelin]

ok, ok, I take the blame (-;

[Johan Commelin]

I view this as part of extending the API

[Yury G. Kudryashov]

In my experience, using very precise [decidable] assumptions in the best way to make lemmas that work both with classical and without it.

[Yury G. Kudryashov]

E.g., it's OK to add a [decidable] assumption that can be deduced from others if this assumption is used somewhere in the statement (not the proof).