We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 4e9d7dc commit 677875cCopy full SHA for 677875c
src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -3545,7 +3545,7 @@ theorem getD_union_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h
3545
exact contains_eq_false
3546
3547
theorem getD_union!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
3548
- {k : α} {fallback : β k} (contains_eq_false : m₂.contains k = false) :
+ {k : α} {fallback : β k} (contains_eq_false : m₂.contains k = false) :
3549
(m₁.union! m₂).getD k fallback = m₁.getD k fallback := by
3550
rw [← union_eq_union!]
3551
apply getD_union_of_contains_eq_false_right h₁ h₂
0 commit comments