Theorem: Multiset.elim_eq_forall (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
β : Type u_2
s : Multiset α
f : (L : List α) → ↑L = s → β
h : ∀ (a b : List α) (ha : ↑a = s) (hb : ↑b = s), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s}, elim s f h = f L hL → motive
⊢ motive
Tactic:
induction s using Quotient.inductionOn with | _ L =>
exact hmotive rfl
State after:
no goals

State before:
case h
α : Type u_1
β : Type u_2
motive : Prop
L : List α
f : (L_1 : List α) → ↑L_1 = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ↑a = ⟦L⟧) (hb : ↑b = ⟦L⟧), f a ha = f b hb
hmotive : ∀ {L_1 : List α} {hL : ↑L_1 = ⟦L⟧}, elim ⟦L⟧ f h = f L_1 hL → motive
⊢ motive
Tactic:
exact hmotive rfl
State after:
no goals