# Zulip Chat Archive

## Stream: new members

### Topic: Why doesn't this rewrite?

#### Daniele Pusceddu (May 05 2023 at 07:47):

Hello, I can't figure out why the `rw [same]`

in the example below does not work.

I introduced `same`

as a sanity check to verify they are indeed equal, but even a direct rewrite does not work... I also tried conv.

```
import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finset.Basic
structure test where
f: ℕ →₀ ℕ
h: f.support.card = 2
def test.upd
(t: test) (n: ℕ) (m: ℕ)
(hin: n ∈ t.f.support) (hpos: ¬m=0): test :=
⟨t.f.update n m, by
simp [Finsupp.update, hpos]
have same:
Finset.card (insert n t.f.support) = Finset.card t.f.support
:= by exact Finset.card_insert_of_mem hin
rw [same]
sorry
⟩
```

#### Andrés Goens (May 05 2023 at 09:41):

@Daniele Pusceddu Lean pretty-prints your proof state so that it's more readable, but you can add an option to make it show everything in detail (turn off pretty printing), e.g. by adding the line `set_option pp.all true in`

above your `def test.upd`

.

#### Andrés Goens (May 05 2023 at 09:42):

in your case it gives me this:

```
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
@Finset.card.{0} Nat
(@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
(@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) n
(@Finsupp.support.{0, 0} Nat Nat
(@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t)))
t : test
n m : Nat
hin :
@Membership.mem.{0, 0} Nat (Finset.{0} Nat) (@Finset.instMembershipFinset.{0} Nat) n
(@Finsupp.support.{0, 0} Nat Nat
(@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))
hpos : Not (@Eq.{1} Nat m (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
same :
@Eq.{1} Nat
(@Finset.card.{0} Nat
(@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
(@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) n
(@Finsupp.support.{0, 0} Nat Nat
(@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))))
(@Finset.card.{0} Nat
(@Finsupp.support.{0, 0} Nat Nat
(@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t)))
⊢ @Eq.{1} Nat
(@Finset.card.{0} Nat
(@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
(@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => Classical.decEq.{1} Nat a b) n
(@Finsupp.support.{0, 0} Nat Nat
(@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))))
(@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
```

#### Andrés Goens (May 05 2023 at 09:43):

and if you compare `same`

with your goal, it looks ilke it's using a different equality type for `a = b`

, ` instDecidableEqNat a b`

vs `Classical.decEq.{1} Nat a b`

#### Andrés Goens (May 05 2023 at 09:45):

that answers why it doesn't rewrite. How to fix that I'm not sure, I don't really know what `Classical.decEq`

does and why your `h`

in `test`

asks for that

#### Andrés Goens (May 05 2023 at 09:46):

What I do in situations like that is just write a line

`#check Classical.decEq`

so that I can use my editor to "go to definition", and that sends me to the mathlib definition of `Classical.decEq`

:

```
/-- Any type `α` has decidable equality classically. -/
noncomputable def decEq (α : Sort u) : DecidableEq α := by infer_instance
#align classical.dec_eq Classical.decEq
```

#### Andrés Goens (May 05 2023 at 09:49):

the strange thing is that it's using that instance for your cardinalities, which are `Nat`

s. I have no idea why though

#### Yaël Dillies (May 05 2023 at 10:29):

The answer is that docs4#Finsupp is classical and something in the API is leaking this implementation detail. I don't know where exactly the problem is, but I can tell you something is wrong and it's not your fault.

#### Andrés Goens (May 05 2023 at 10:55):

thanks, that's a much better way of putting it @Yaël Dillies :sweat_smile:

#### Kyle Miller (May 05 2023 at 11:11):

@Daniele Pusceddu There's a tactic that can be useful here, which is `convert`

. It knows that there is at most one `Fintype`

instance for a given type and inserts rewrites automatically for you to convert from one to the other. Since the LHS of `same`

is supposed to match the LHS of the goal (except for the fact it's not defeq), we can do `convert same`

to have it line things up and create new goals for things it can't figure out are equal.

```
import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic.Convert
structure test where
f: ℕ →₀ ℕ
h: f.support.card = 2
def test.upd
(t: test) (n: ℕ) (m: ℕ)
(hin: n ∈ t.f.support) (hpos: ¬m=0): test :=
⟨t.f.update n m,
by
simp [Finsupp.update, hpos]
have same: Finset.card (insert n t.f.support) = Finset.card t.f.support
:= by exact Finset.card_insert_of_mem hin
convert same -- or do `convert ← same` to get the goal to be reversed, which looks better
sorry
⟩
```

#### Kyle Miller (May 05 2023 at 11:12):

In general, think of `convert`

to be like `exact`

but it creates side goals wherever there are differences that it can't resolve itself.

Last updated: Dec 20 2023 at 11:08 UTC