From 985d9611745df1bdb8afc971bb952d78bbbdab07 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 10 Oct 2024 16:56:05 +0000 Subject: [PATCH] chore: fix a structure instance for lean4#5528 (#17567) [lean4#5528](/~https://github.com/leanprover/lean4/pull/5528) fixes some issues with how structure instance notation expands, which breaks `OrderIso.mapSetOfMaximal`. This PR manually expands the spread notation. For the curious, this definition is making use of both the implicit lambda feature and implicit arguments in `map_rel_iff' := f.map_rel_iff`. Concretely, this is equivalent to `map_rel_iff' {_ _} := f.map_rel_iff _ _` where the `_`'s don't match up. --- Mathlib/Order/Minimal.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Order/Minimal.lean b/Mathlib/Order/Minimal.lean index 728087a7dbdf4..cfc38ab8c1e32 100644 --- a/Mathlib/Order/Minimal.lean +++ b/Mathlib/Order/Minimal.lean @@ -621,15 +621,17 @@ theorem map_maximal_mem (f : s ≃o t) (hx : Maximal (· ∈ s) x) : def mapSetOfMinimal (f : s ≃o t) : {x | Minimal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) x} where toFun x := ⟨f ⟨x, x.2.1⟩, f.map_minimal_mem x.2⟩ invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_minimal_mem x.2⟩ - left_inv x := Subtype.ext (by apply congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩) - right_inv x := Subtype.ext (by apply congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩) - map_rel_iff' {_ _} := f.map_rel_iff + left_inv x := Subtype.ext (congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩ :) + right_inv x := Subtype.ext (congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩ :) + map_rel_iff' := f.map_rel_iff /-- If two sets are order isomorphic, their maximals are also order isomorphic. -/ def mapSetOfMaximal (f : s ≃o t) : {x | Maximal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) x} where toFun x := ⟨f ⟨x, x.2.1⟩, f.map_maximal_mem x.2⟩ invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_maximal_mem x.2⟩ - __ := (show OrderDual.ofDual ⁻¹' s ≃o OrderDual.ofDual ⁻¹' t from f.dual).mapSetOfMinimal + left_inv x := Subtype.ext (congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩ :) + right_inv x := Subtype.ext (congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩ :) + map_rel_iff' := f.map_rel_iff /-- If two sets are antitonically order isomorphic, their minimals/maximals are too. -/ def setOfMinimalIsoSetOfMaximal (f : s ≃o tᵒᵈ) :