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

State before:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ elim ⟦a⟧ f h = f a ⋯
Tactic:
simp [elim]
State after:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ Trunc.lift (fun x => f ↑x ⋯) ⋯ (toTrunc ⟦a⟧) = f a ⋯

State before:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ Trunc.lift (fun x => f ↑x ⋯) ⋯ (toTrunc ⟦a⟧) = f a ⋯
Tactic:
apply Trunc.lift_mk
State after:
no goals