feat: Function.funext_iff and Sum.elim_eq_iff (#715)

* feat: Function.funext_iff and Sum.elim_eq_iff

* Update Std/Data/Sum/Lemmas.lean

Co-authored-by: Scott Morrison <scott@tqft.net>

* Function.funext_iff moved

* Update Std/Logic.lean

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

* fix

---------

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Std/Data/Sum/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 
 import Std.Data.Sum.Basic
+import Std.Logic
 
 /-!
 # Disjoint union of types
@@ -112,6 +113,10 @@ theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
     Sum.elim (f ∘ inl) (f ∘ inr) = f :=
   funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
 
+theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
+    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
+  simp [funext_iff]
+
 /-! ### `Sum.map` -/
 
 @[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :

Std/Logic.lean

@@ -59,6 +59,9 @@ theorem funext₃ {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a
     {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
   funext fun _ => funext₂ <| h _
 
+theorem Function.funext_iff {β : α → Sort u} {f₁ f₂ : ∀ x : α, β x} : f₁ = f₂ ↔ ∀ a, f₁ a = f₂ a :=
+  ⟨congrFun, funext⟩
+
 theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
   mt <| congrArg _