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

State before:
α : Type u_1
β : Type u_2
s : Finset α
f : (L : List α) → ↑L = s.val → β
h : ∀ (a b : List α) (ha : ↑a = s.val) (hb : ↑b = s.val), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s.val}, elim s f h = f L hL → motive
⊢ motive
Tactic:
rcases s with ⟨s,h⟩
State after:
case mk
α : Type u_1
β : Type u_2
motive : Prop
s : Multiset α
h✝ : Multiset.Nodup s
f : (L : List α) → ↑L = { val := s, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := s, nodup := h✝ }.val) (hb : ↑b = { val := s, nodup := h✝ }.val), f a ha = f b hb
hmotive : ∀ {L : List α} {hL : ↑L = { val := s, nodup := h✝ }.val}, elim { val := s, nodup := h✝ } f h = f L hL → motive
⊢ motive

State before:
case mk
α : Type u_1
β : Type u_2
motive : Prop
s : Multiset α
h✝ : Multiset.Nodup s
f : (L : List α) → ↑L = { val := s, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := s, nodup := h✝ }.val) (hb : ↑b = { val := s, nodup := h✝ }.val), f a ha = f b hb
hmotive : ∀ {L : List α} {hL : ↑L = { val := s, nodup := h✝ }.val}, elim { val := s, nodup := h✝ } 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 mk.h
α : Type u_1
β : Type u_2
motive : Prop
L : List α
h✝ : Multiset.Nodup ⟦L⟧
f : (L_1 : List α) → ↑L_1 = { val := ⟦L⟧, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := ⟦L⟧, nodup := h✝ }.val) (hb : ↑b = { val := ⟦L⟧, nodup := h✝ }.val),
    f a ha = f b hb
hmotive :
  ∀ {L_1 : List α} {hL : ↑L_1 = { val := ⟦L⟧, nodup := h✝ }.val},
    elim { val := ⟦L⟧, nodup := h✝ } f h = f L_1 hL → motive
⊢ motive
Tactic:
exact hmotive rfl
State after:
no goals