rintro not unpacking the way I expected

Stream: new members

[Ryan Smith]

While unpacking a universal quantifier for a complex number I found that rintro doesn't expand in the way I would expect it work. What I have right now works ok, so the point of this question is in better understanding:

s : Multiset ℂ
have hibd : ∀ t ∈ s.toEnumFinset, (f t).re ≤ 1 := by
    rintro ⟨z, n⟩
    -- ⊢ (z, n) ∈ s.toEnumFinset → (f (z, n)).re ≤ 1
    intro heig
    -- ⊢ (f (z, n)).re ≤ 1     this is fine and now we are ready to prove our result

Can we combine the rintro and intro statements together? When I tried introduce another term to the constructor it doesn't work as expected. Asking for teaching value.

[Kevin Buzzard]

If you asked with a #mwe rather than a code fragment then it would be much easier for others to answer. Does rintro \<z, n\> heig not work?

[Ryan Smith]

Sorry you're totally right about that.

It does! So why does heig not sit inside the brackets?

[Kevin Buzzard]

The pointy brackets are taking a term apart. heig is a different term.

[Ruben Van de Velde]

∀ t ∈ s.toEnumFinset, (f t).re ≤ 1 actually means ∀ t, ∀ ht : t ∈ s.toEnumFinset, (f t).re ≤ 1, and rintro takes space-separated arguments for each ∀

[Ruben Van de Velde]

It's equivalent to

intro t heig
obtain ⟨z, n⟩ := t

[Kevin Buzzard]

Aah yes! It's not at all obvious that it's a different term! Hence the confusion. This is an implementation detail I guess.

[Ryan Smith]

Thanks for the explanation. Now back to grinding away at a lemma that seems like it should be trivially obvious :)