From c1056b03e9852a84baf7442076353f2ccf05c47b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 25 Mar 2024 01:53:52 +0000 Subject: [PATCH] chore: rm @[eqns] in Ordmap (#11645) Co-authored-by: Scott Morrison --- Mathlib/Data/Ordmap/Ordnode.lean | 12 +++++++----- Mathlib/Data/Ordmap/Ordset.lean | 4 ++-- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/Ordmap/Ordnode.lean b/Mathlib/Data/Ordmap/Ordnode.lean index 46d293f306cc2..07c6256b07290 100644 --- a/Mathlib/Data/Ordmap/Ordnode.lean +++ b/Mathlib/Data/Ordmap/Ordnode.lean @@ -138,14 +138,16 @@ def size : Ordnode α → ℕ | node sz _ _ _ => sz #align ordnode.size Ordnode.size -theorem size_nil : size (nil : Ordnode α) = 0 := +-- Adaptation note: +-- During the port we marked these lemmas with `@[eqns]` to emulate the old Lean 3 behaviour. +-- See https://github.com/leanprover-community/mathlib4/issues/11647 + +@[simp] theorem size_nil : size (nil : Ordnode α) = 0 := rfl -theorem size_node (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : size (node sz l x r) = sz := +@[simp] theorem size_node (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : + size (node sz l x r) = sz := rfl -attribute [eqns size_nil size_node] size -attribute [simp] size - /-- O(1). Is the set empty? empty ∅ = tt diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean index 25185a3f39b72..c7931c55c559a 100644 --- a/Mathlib/Data/Ordmap/Ordset.lean +++ b/Mathlib/Data/Ordmap/Ordset.lean @@ -808,7 +808,7 @@ theorem Raised.add_right (k) {n m} (H : Raised n m) : Raised (n + k) (m + k) := theorem Raised.right {l x₁ x₂ r₁ r₂} (H : Raised (size r₁) (size r₂)) : Raised (size (@node' α l x₁ r₁)) (size (@node' α l x₂ r₂)) := by - rw [node', size, size]; generalize size r₂ = m at H ⊢ + rw [node', size_node, size_node]; generalize size r₂ = m at H ⊢ rcases H with (rfl | rfl) · exact Or.inl rfl · exact Or.inr rfl @@ -1395,7 +1395,7 @@ theorem Valid'.eraseMax_aux {s l x r o₁ o₂} (H : Valid' o₁ (.node s l x r) rcases IHrr H.right with ⟨h, e⟩ refine' ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), _⟩ rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)] - rw [size, e]; rfl + rw [size_node, e]; rfl #align ordnode.valid'.erase_max_aux Ordnode.Valid'.eraseMax_aux theorem Valid'.eraseMin_aux {s l} {x : α} {r o₁ o₂} (H : Valid' o₁ (.node s l x r) o₂) :