## 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: Aug 03 2023 at 10:10 UTC