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

State before:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ elim ⟦L⟧ f h = f L ⋯
Tactic:
simp [elim]
State after:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ Quotient.elim ⟦L⟧ f h = f L ⋯

State before:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ Quotient.elim ⟦L⟧ f h = f L ⋯
Tactic:
apply Trunc.lift_mk
State after:
no goals