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 e1736e9 commit 58d3780Copy full SHA for 58d3780
src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -3376,7 +3376,7 @@ theorem union_insert_right_equiv_insert_union [TransOrd α] {p : (a : α) × β
3376
. apply List.Perm.symm
3377
. apply toListModel_union_list (by wf_trivial) (by wf_trivial)
3378
3379
-theorem union!_insert_right_equiv_insert_union! [TransOrd α] {p : (a : α) × β a}
+theorem union!_insert_right_equiv_insert_union! [TransOrd α] {p : (a : α) × β a}
3380
(h₁ : m₁.WF) (h₂ : m₂.WF) :
3381
Equiv (m₁.union! (m₂.insert! p.fst p.snd)) ((m₁.union! m₂).insert! p.fst p.snd) := by
3382
rw [← union_eq_union!, ← union_eq_union!]
0 commit comments