# Zulip Chat Archive

## Stream: general

### Topic: eq.subst vs. ▸

#### Junyan Xu (Jun 22 2022 at 06:34):

`▸`

is simply the notation for docs#eq.subst, but I've found it sometimes less powerful, e.g. The two `subst`

here cannot be replaced by `▸`

. Why is this, and is it possible to make them equally powerful? This is desirable since `h ▸`

is shorter than `h.subst`

; it's less a problem for `h.symm ▸`

vs. `h.substr`

since they have equal length (but a pair of parentheses may be eliminable using `h.symm ▸`

), though it will be another story if we introduce a notation for `eq.substr`

...

#### Kevin Buzzard (Jun 22 2022 at 07:54):

Huh, yeah that's pretty weird. Note that `eq.subst h ...`

also doesn't work (even though `h.subst`

does).

#### Kevin Buzzard (Jun 22 2022 at 07:58):

Here's the issue on master and I've no doubt that it can be minimised a lot more:

```
import field_theory.splitting_field
variables {K : Type} [field K] (i : K →+* K)
open_locale polynomial
open polynomial
lemma roots_ne_zero_of_splits {f : K[X]} (hs : splits i f) (hf0 : nat_degree f ≠ 0) :
(f.map i).roots ≠ 0 :=
begin
obtain ⟨x, hx⟩ := exists_root_of_splits i hs (λ h, hf0 $ nat_degree_eq_of_degree_eq_some h),
intro h, -- h : (map i f).roots = 0
rw ← eval_map at hx,
-- cases eq.subst h ((mem_roots _).2 hx), -- fails
cases h.subst ((mem_roots _).2 hx), -- works
exact map_ne_zero (λ h, (h.subst hf0) rfl)
end
```

#### Yaël Dillies (Jun 22 2022 at 09:00):

I'm pretty sure this is the result of `elab_as_eliminator`

. I'm not certain we want to get the two to do the same thing because if I remember correctly I sometimes reached the opposite situation, so it's nice to have both options available.

#### Junyan Xu (Jun 22 2022 at 09:07):

Interesting, I didn't know `elab_as_eliminator`

has to do with dot notation.

#### Yaël Dillies (Jun 22 2022 at 10:44):

Dot notation in general messes up with elaboration, so dot notation has to do with `elab_as_eliminator`

to the extent that both change elaboration. As a result, I'm not sure the difference in behavior is intended.

#### Peter Nelson (Jun 22 2022 at 11:04):

I’ve run into this problem too - I am not sure that having both options available is a great solution, since it is rather opaque when one works over the other. I don’t understand what fixing this would entail, though.

Last updated: Dec 20 2023 at 11:08 UTC