Tactic for getting all hypotheses out of a finite forall

Stream: mathlib4

[Bolton Bailey]

Suppose I have a hypothesis which looks like

h : ∀ x : Fin 2 ⊕ Fin 2, f x = 0

Is there some one-line tactic I can use to get the hypotheses

h_inr_0 : f (inr 0) = 0
h_inr_1 : f (inr 1) = 0
h_inl_0 : f (inl 0) = 0
h_inl_1 : f (inl 1) = 0

[Yaël Dillies]

simp_rw [Sum.forall, Fin.forall_fin_succ, Fin.forall_fin_one] at h?

[Bolton Bailey]

Thanks. I was wondering if there was something a bit more general that would work on any finite type, but I suppose that works.

[Bolton Bailey]

I guess I was thinking it would be useful for automation to have access to splitting things into hypotheses, but I guess it could actually just do this and then split into cases.

[Yaël Dillies]

fin_cases could handle this, I guess. But it's not super fast, compared to using the appropriate lemmas straight ahead.

[Heather Macbeth]

I agree that this would be a nice tactic. I've noticed the gap before (there would be some nice use cases in the matrix computations in the polyrith tutorial).

[Eric Rodriguez]

I'm confused how fin_cases isn't the right tool for this job

[Heather Macbeth]

Maybe I'm missing something, what did you have in mind Eric?

[Eric Rodriguez]

Oh I understand now, it's in the hypothesis and not the goal.

[Yaël Dillies]

fin_cases at it could be, though

[Yaël Dillies]

Luckily for speed, it doesn't even have to prove that the list is exhaustive (for foralls at least, not for exist).

[Bolton Bailey]

Yaël Dillies said:

fin_cases at it could be, though

Yeah, at first I thought/hoped that might be the name

[Bolton Bailey]

Possibly related: A tactic that would convert a hypothesis of the form h : ∑ x : Fin 4, f x = 0 into f 0 + f 1 + f 2 + f 3 = 0. Does this exist?

[Yaël Dillies]

simp_rw [Fin.sum_univ_succ, Fin.sum_univ_zero]