We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
funext₂
1 parent 77d9317 commit a02b532Copy full SHA for a02b532
Mathlib/Order/Antisymmetrization.lean
@@ -40,7 +40,7 @@ def AntisymmRel (a b : α) : Prop :=
40
r a b ∧ r b a
41
42
theorem antisymmRel_swap : AntisymmRel (swap r) = AntisymmRel r :=
43
- funext fun _ => funext fun _ => propext and_comm
+ funext₂ fun _ _ ↦ propext and_comm
44
45
@[refl]
46
theorem antisymmRel_refl [IsRefl α r] (a : α) : AntisymmRel r a a :=
0 commit comments