From cb172855f1712a9e906e91f3e14541960562fb78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Wed, 17 Apr 2024 06:24:45 +0200 Subject: [PATCH] feat: Function.funext_iff and Sum.elim_eq_iff (#715) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * feat: Function.funext_iff and Sum.elim_eq_iff * Update Std/Data/Sum/Lemmas.lean Co-authored-by: Scott Morrison * Function.funext_iff moved * Update Std/Logic.lean Co-authored-by: François G. Dorais * fix --------- Co-authored-by: Scott Morrison Co-authored-by: François G. Dorais --- Std/Data/Sum/Lemmas.lean | 5 +++++ Std/Logic.lean | 3 +++ 2 files changed, 8 insertions(+) diff --git a/Std/Data/Sum/Lemmas.lean b/Std/Data/Sum/Lemmas.lean index f7766d2985..80d4fb4230 100644 --- a/Std/Data/Sum/Lemmas.lean +++ b/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 : β → β') : diff --git a/Std/Logic.lean b/Std/Logic.lean index 43a9b31f66..759164aec1 100644 --- a/Std/Logic.lean +++ b/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 _