From 3c50f70f0a80c3bb4c35acfbab8ab5792a6e35e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 18 Feb 2024 22:57:44 +0000 Subject: [PATCH 1/5] chore: Remove `Init.Propext` These lemmas can easily go to `Logic.Basic` --- Mathlib.lean | 1 - Mathlib/Init/Propext.lean | 47 ------------------------------------- Mathlib/Logic/Basic.lean | 19 +++++++++++++++ Mathlib/Logic/Relation.lean | 1 - 4 files changed, 19 insertions(+), 49 deletions(-) delete mode 100644 Mathlib/Init/Propext.lean diff --git a/Mathlib.lean b/Mathlib.lean index 7ececd9ec2a54..ef72745b1a8f2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2403,7 +2403,6 @@ import Mathlib.Init.Logic import Mathlib.Init.Meta.WellFoundedTactics import Mathlib.Init.Order.Defs import Mathlib.Init.Order.LinearOrder -import Mathlib.Init.Propext import Mathlib.Init.Quot import Mathlib.Init.Set import Mathlib.Init.ZeroOne diff --git a/Mathlib/Init/Propext.lean b/Mathlib/Init/Propext.lean deleted file mode 100644 index 28dcf63eacc6f..0000000000000 --- a/Mathlib/Init/Propext.lean +++ /dev/null @@ -1,47 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -import Std.Logic -import Mathlib.Mathport.Rename - -/-! Additional congruence lemmas. -/ - --- Porting note: --- the statement of `forall_congr_eq` in Lean 3 is identical to `forall_congr` in Lean 4, --- so is omitted. --- theorem forall_congr_eq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : --- (∀ x, p x) = ∀ x, q x := --- (forall_congr fun a ↦ (h a)) -#align forall_congr_eq forall_congr - -theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) := - propext (imp_congr h₁.to_iff h₂.to_iff) - -theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a → b) = (c → d) := - propext (imp_congr_ctx h₁.to_iff fun hc ↦ (h₂ hc).to_iff) - -theorem eq_true_intro {a : Prop} (h : a) : a = True := - propext (iff_true_intro h) - -theorem eq_false_intro {a : Prop} (h : ¬a) : a = False := - propext (iff_false_intro h) - -theorem Iff.to_eq {a b : Prop} (h : a ↔ b) : a = b := - propext h - -theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := - propext (Iff.intro (fun h ↦ Iff.to_eq h) fun h ↦ h.to_iff) - --- Porting note: --- `eq_false` and `eq_true` in Lean 3 are not used in mathlib3, --- and there are already lemmas with these names in Lean 4, so they have not been ported. - --- theorem eq_false {a : Prop} : (a = False) = ¬a := --- have : (a ↔ False) = ¬a := propext (iff_false a) --- Eq.subst (@iff_eq_eq a False) this - --- theorem eq_true {a : Prop} : (a = True) = a := --- have : (a ↔ True) = a := propext (iff_true a) --- Eq.subst (@iff_eq_eq a True) this diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index 896d1c2d2755b..f5aa416bf3349 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -914,6 +914,25 @@ theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h propext (forall_prop_congr hq hp) #align forall_prop_congr' forall_prop_congr' +#align forall_congr_eq forall_congr + +lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) := + propext (imp_congr h₁.to_iff h₂.to_iff) + +lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a → b) = (c → d) := + propext (imp_congr_ctx h₁.to_iff fun hc ↦ (h₂ hc).to_iff) + +lemma eq_true_intro (h : a) : a = True := propext (iff_true_intro h) +lemma eq_false_intro (h : ¬a) : a = False := propext (iff_false_intro h) + +alias Iff.eq := propext + +lemma iff_eq_eq : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩ + +-- They were not used in Lean 3 and there are already lemmas with those names in Lean 4 +#noalign eq_false +#noalign eq_true + /-- See `IsEmpty.forall_iff` for the `False` version. -/ @[simp] theorem forall_true_left (p : True → Prop) : (∀ x, p x) ↔ p True.intro := forall_prop_of_true _ diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean index 6fcfb39847fdb..59c1c6ca480cf 100644 --- a/Mathlib/Logic/Relation.lean +++ b/Mathlib/Logic/Relation.lean @@ -5,7 +5,6 @@ Authors: Johannes Hölzl -/ import Mathlib.Logic.Function.Basic import Mathlib.Logic.Relator -import Mathlib.Init.Propext import Mathlib.Init.Data.Quot import Mathlib.Tactic.Cases import Mathlib.Tactic.Use From e9435fc68e6ead848b33a2efa2b924fff9b57729 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 19 Feb 2024 09:01:32 +0000 Subject: [PATCH 2/5] fix --- Mathlib/CategoryTheory/IsConnected.lean | 2 +- Mathlib/GroupTheory/GroupAction/Quotient.lean | 2 +- Mathlib/Order/Filter/Basic.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/IsConnected.lean b/Mathlib/CategoryTheory/IsConnected.lean index 960f20d2acf91..ad25c61197832 100644 --- a/Mathlib/CategoryTheory/IsConnected.lean +++ b/Mathlib/CategoryTheory/IsConnected.lean @@ -167,7 +167,7 @@ The converse is given in `IsConnected.of_induct`. -/ theorem induct_on_objects [IsPreconnected J] (p : Set J) {j₀ : J} (h0 : j₀ ∈ p) (h1 : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) (j : J) : j ∈ p := by - let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).to_eq + let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).eq injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i rwa [i] #align category_theory.induct_on_objects CategoryTheory.induct_on_objects diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 3249807d690fd..cd36a15d777b3 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -427,7 +427,7 @@ theorem card_comm_eq_card_conjClasses_mul_card (G : Type*) [Group G] : rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma, sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b }) (fun g ↦ card (MulAction.fixedBy G g)) - fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq, + fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group] congr 1; apply card_congr'; congr; ext; exact (Setoid.comm' _).trans isConj_iff.symm diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 5a15268186a70..1e5c89429db89 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -1476,7 +1476,7 @@ theorem EventuallyEq.rw {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (p : #align filter.eventually_eq.rw Filter.EventuallyEq.rw theorem eventuallyEq_set {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ s ↔ x ∈ t := - eventually_congr <| eventually_of_forall fun _ => ⟨Eq.to_iff, Iff.to_eq⟩ + eventually_congr <| eventually_of_forall fun _ ↦ eq_iff_iff #align filter.eventually_eq_set Filter.eventuallyEq_set alias ⟨EventuallyEq.mem_iff, Eventually.set_eq⟩ := eventuallyEq_set From 629aba1f9fd44645dbf85cbe87ef29ebf774833e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 19 Feb 2024 11:34:36 +0000 Subject: [PATCH 3/5] fix --- Mathlib/Logic/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index f5aa416bf3349..ea7d0f7719ab4 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -925,7 +925,8 @@ lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a lemma eq_true_intro (h : a) : a = True := propext (iff_true_intro h) lemma eq_false_intro (h : ¬a) : a = False := propext (iff_false_intro h) -alias Iff.eq := propext +/-- Alias of `propext`. -/ +lemma Iff.eq : (a ↔ b) → a = b := propext lemma iff_eq_eq : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩ From 5a6355df8f9ad5b1d04db05953253077308012d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 4 Apr 2024 06:17:22 +0000 Subject: [PATCH 4/5] turn into an alias --- Mathlib/Logic/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index ca0d9f6ba031c..5f9cc39c90684 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -934,8 +934,7 @@ lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a lemma eq_true_intro (h : a) : a = True := propext (iff_true_intro h) lemma eq_false_intro (h : ¬a) : a = False := propext (iff_false_intro h) -/-- Alias of `propext`. -/ -lemma Iff.eq : (a ↔ b) → a = b := propext +alias Iff.eq := propext lemma iff_eq_eq : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩ From 04170a9d6d9862e03adea26dfd37772610c41eda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 4 Apr 2024 10:13:54 +0000 Subject: [PATCH 5/5] nolint --- Mathlib/Logic/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index 31d3882ffcb27..8d548b900d932 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -934,7 +934,8 @@ lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a lemma eq_true_intro (h : a) : a = True := propext (iff_true_intro h) lemma eq_false_intro (h : ¬a) : a = False := propext (iff_false_intro h) -alias Iff.eq := propext +-- FIXME: `alias` creates `def Iff.eq := propext` instead of `lemma Iff.eq := propext` +@[nolint defLemma] alias Iff.eq := propext lemma iff_eq_eq : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩