From 93805a1b5e7c380bc1c08aca23556e5d9e7bb417 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 7 Nov 2026 15:52:20 -0500
Subject: [PATCH 01/17] feat: TableMessage

---
 ImportGraph/Util/TableMessage.lean | 73 ++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 ImportGraph/Util/TableMessage.lean

diff --git a/ImportGraph/Util/TableMessage.lean b/ImportGraph/Util/TableMessage.lean
new file mode 100644
index 0000000..2d6de22
--- /dev/null
+++ b/ImportGraph/Util/TableMessage.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+
+import Lean.Elab.Command
+
+/-!
+# Formatting tables
+
+This module provides basic utilities for formatting tables with aligned columns.
+For now, we only supports tables of strings.
+
+## Future work
+
+- Specifying dividers and borders, padding characters, right/left alignment, column widths
+  - Ideally this is granular, e.g. per cell/row/column
+- Composing and stacking tables
+- Widget version using HTML tables to avoid awkward reflowing + allow `MessageData`
+-/
+
+namespace ImportGraph
+
+open ImportGraph
+
+public section
+
+/-- Pad a string on the right with `c : Char` (by default `' '`), until it reaches length `n`. Does
+not trim strings already over length `n` down to length `n`. -/
+@[inline] def String.rightPad (n : Nat) (s : String) (char : Char := ' ') :=
+  s.pushn char (n - s.positions.length)
+
+/-- Pad a string on the left with `c : Char` (by default `' '`), until it reaches length `n`. Does
+not trim strings already over length `n` down to length `n`. -/
+@[inline] def String.leftPad (n : Nat) (s : String) (char : Char := ' ') :=
+  "".pushn char (n - s.positions.length) ++ s
+
+namespace Table
+
+/-- A row with a fixed number of elements in a table such as `Array (Table.Row 5)`. (The `String`s
+in a `Row` are allowed to have any length.) -/
+protected abbrev Row (n : Nat) := Vector String n
+
+/-- Given an array of table rows, arranges them in a table. Each cell is left-aligned, and
+separated from the next cell in the row by a space. Spaces at the end of each row are trimmed. -/
+protected def formatSimple (rows : Array (Table.Row n)) : String := Id.run do
+  if h : rows.size > 0 then
+    let mut colWidths := rows[0].map (·.positions.length)
+    for h : i in 1...rows.size do
+      colWidths := colWidths.zipWith (max · ·.positions.length) rows[i]
+    let mut table := ""
+    for hRow : rowIdx in 0...rows.size do
+      for hCol : i in 0...n do
+        if h : i + 1 < n then
+          table := table ++ rows[rowIdx][i].rightPad colWidths[i] |>.push ' '
+        else
+          -- The last column needs neither padding nor a `' '` separator
+          -- However, it may still have spaces (e.g. empty cell) so trim them; do not drop `'\n'`.
+          table := table ++ rows[rowIdx][i] |>.dropEndWhile (· = ' ') |>.copy
+      unless rowIdx + 1 == rows.size do
+        table := table.push '\n'
+    return table
+  else return ""
+
+/-- An empty row in a table. -/
+def emptyRow {n} : Table.Row n := Vector.replicate n ""
+
+/-- Increase the size of a row by padding it on the right with empty cells. -/
+def Row.rightPad (row : Table.Row n) (h : n ≤ m := by grind) : Table.Row m :=
+  (show max m n = m by grind) ▸ row.rightpad m ""

From c7da3bae64f2b9b81b22ccd0529f20e6d44bf7b9 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 7 Nov 2026 15:52:26 -0500
Subject: [PATCH 02/17] chore: test

---
 ImportGraphTest/Shake/Algebra.lean | 33 +++++++++++++++---------------
 ImportGraphTest/TableMessage.lean  | 32 +++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 16 deletions(-)
 create mode 100644 ImportGraphTest/TableMessage.lean

diff --git a/ImportGraphTest/Shake/Algebra.lean b/ImportGraphTest/Shake/Algebra.lean
index 0117a0b..6931e1a 100644
--- a/ImportGraphTest/Shake/Algebra.lean
+++ b/ImportGraphTest/Shake/Algebra.lean
@@ -7,6 +7,7 @@ module
 
 public meta import ImportGraph.Shake.Algebra
 public meta import Lean.Elab.Command
+public meta import ImportGraph.Util.TableMessage
 
 /-!
 # Tests for the import hierarchy algebra
@@ -35,26 +36,26 @@ def NeedsKind.allPairs : Array (NeedsKind × NeedsKind) :=
 def pad (n : Nat) (s : String) : String := s ++ "".pushn ' ' (n - s.length)
 
 /-- The composition table of `NeedsKind.andThen`, with the first factor on the left. -/
-meta def compositionTable : String :=
-  let row (cells : List String) := (String.join <| cells.map (pad 7)).trimAsciiEnd.toString
+meta def compositionTable : String := Id.run do
   -- push meta to the end instead of `all` for a cleaner table
-  let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta) |>.toList
-  "\n".intercalate <|
-    row ("(↓) ≫ (→) " :: ks.map shortName) ::
-      ks.map fun k₁ =>
-        row <| pad 10 (shortName k₁) :: ks.map fun k₂ =>
-          if h : k₁.target = k₂.source then shortName (andThen k₁ k₂) else "-"
+  let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta)
+  let mut rows : Array (Table.Row (1 + ks.size)) :=
+    #[#v["(↓) ≫ (→)"] ++ ks.toVector.map shortName]
+  rows := rows ++ ks.map fun k₁ =>
+    #v[shortName k₁] ++ (ks.toVector.map fun k₂ =>
+      if h : k₁.target = k₂.source then shortName (k₁.andThen k₂) else "-")
+  Table.formatSimple rows
 
 /--
 info:
 
-(↓) ≫ (→) pub    priv   all    𝓶pub   𝓶priv  𝓶all
-pub       pub    priv   -      𝓶pub   𝓶priv  -
-priv      -      -      priv   -      -      𝓶priv
-all       -      -      all    -      -      𝓶all
-𝓶pub      𝓶pub   𝓶priv  -      𝓶pub   𝓶priv  -
-𝓶priv     -      -      𝓶priv  -      -      𝓶priv
-𝓶all      -      -      𝓶all   -      -      𝓶all
+(↓) ≫ (→) pub  priv  all   𝓶pub 𝓶priv 𝓶all
+pub       pub  priv  -     𝓶pub 𝓶priv -
+priv      -    -     priv  -    -     𝓶priv
+all       -    -     all   -    -     𝓶all
+𝓶pub      𝓶pub 𝓶priv -     𝓶pub 𝓶priv -
+𝓶priv     -    -     𝓶priv -    -     𝓶priv
+𝓶all      -    -     𝓶all  -    -     𝓶all
 -/
 #guard_msgs in
 #eval IO.println s!"\n\n{compositionTable}"
@@ -165,7 +166,7 @@ protected def Needs.randM (hierarchySize : Nat)
 
 -- TODO: should maybe choose randomly how many are in each "layer"?
 /-- A topologically sorted array of needs, i.e. one in which each `Needs` only refers to prior
-ones. If the config is `none`, it's randomized each time. This allows for more module-tomodule
+ones. If the config is `none`, it's randomized each time. This allows for more module-to-module
 variation in quality, perhaps more like a real repo. -/
 def Needs.randArrayM (hierarchySize : Nat)
     (cfg? : Option RandNeedsConfig := none) :
diff --git a/ImportGraphTest/TableMessage.lean b/ImportGraphTest/TableMessage.lean
new file mode 100644
index 0000000..0d3f4e1
--- /dev/null
+++ b/ImportGraphTest/TableMessage.lean
@@ -0,0 +1,32 @@
+module
+
+import ImportGraph.Util.TableMessage
+import Lean.Elab.Command
+
+open ImportGraph
+
+/--
+info: Table:
+
+          header1 h2   header3!      h₄
+row₁:     item1   foo  bar           baz
+row₂:     item₂   foo₂ bar₂          baz₂
+
+row₃:     1       2    (long item 3) 4
+shortrow: a₁      a₂
+finalrow: 0       1    1             0
+-/
+#guard_msgs in
+run_cmd do
+  let mut rows : Array (Table.Row 5) := #[]
+  rows := rows.push #v["", "header1", "h2", "header3!", "h₄"]
+  let shortRow : Table.Row 3 := #v["shortrow:", "a₁", "a₂"]
+  rows := rows ++ #[
+    #v["row₁:", "item1", "foo", "bar", "baz"],
+    #v["row₂:", "item₂", "foo₂", "bar₂", "baz₂"],
+    Table.emptyRow,
+    #v["row₃:", "1", "2", "(long item 3)", "4"],
+    shortRow.rightPad,
+    #v["finalrow:", "0", "1", "1", "0"]
+  ]
+  Lean.logInfo m!"Table:\n\n{Table.formatSimple rows}"

From 57dbab03861c2f2f17af37554466be60fbceeba3 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 7 Nov 2026 15:52:34 -0500
Subject: [PATCH 03/17] chore: root imports

---
 ImportGraph.lean     | 1 +
 ImportGraphTest.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/ImportGraph.lean b/ImportGraph.lean
index 9646dcb..0ba9185 100644
--- a/ImportGraph.lean
+++ b/ImportGraph.lean
@@ -24,6 +24,7 @@ public import ImportGraph.Shake.EnvExtension
 public import ImportGraph.Shake.Environment
 public import ImportGraph.Shake.Workspace
 public import ImportGraph.Util.FindSorry
+public import ImportGraph.Util.TableMessage
 public import ImportGraph.WorkspaceModel.Base
 public import ImportGraph.WorkspaceModel.Build
 public import ImportGraph.WorkspaceModel.Model
diff --git a/ImportGraphTest.lean b/ImportGraphTest.lean
index 05604b5..513b04f 100644
--- a/ImportGraphTest.lean
+++ b/ImportGraphTest.lean
@@ -22,6 +22,7 @@ import ImportGraphTest.NormImports
 import ImportGraphTest.NoLakeAxioms
 import ImportGraphTest.Shake.Algebra
 import ImportGraphTest.Shake.Workspace
+import ImportGraphTest.TableMessage
 import ImportGraphTest.ToTarget
 import ImportGraphTest.Unused
 import ImportGraphTest.Used

From 4d5f8d1dc11859f37ff3953223a893970b430f10 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 7 Nov 2026 17:33:07 -0500
Subject: [PATCH 04/17] .

---
 ImportGraph/Util/Diff/Basic.lean | 147 +++++++++++++++++++++++++++++++
 ImportGraph/Util/Diff/Shake.lean |  26 ++++++
 2 files changed, 173 insertions(+)
 create mode 100644 ImportGraph/Util/Diff/Basic.lean
 create mode 100644 ImportGraph/Util/Diff/Shake.lean

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
new file mode 100644
index 0000000..e96586e
--- /dev/null
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -0,0 +1,147 @@
+module
+
+public import ImportGraph.Util.TableMessage
+
+public section
+
+open Lean
+
+namespace ImportGraph
+
+namespace Diff
+
+protected class Measureable α where
+  measure : α → Nat
+export Measureable (measure)
+
+instance : Diff.Measureable Nat := ⟨id⟩
+
+open Diff
+
+/-- If an integer is (strictly) greater than 0, display it with `+`. -/
+def Int.toStringWithSign (i : Int) := if i > 0 then s!"+{i}" else s!"{i}"
+
+/-- A simple structure with two states, `initial : α` and `final : α`, which models a transition. -/
+structure Transition α where
+  /-- The state before `final`. -/
+  initial : α
+  /-- The state after `initial`. -/
+  final : α
+
+namespace Transition
+
+@[inline] def map (t : Transition α) (f : α → β) : Transition β where
+  initial := f t.initial
+  final := f t.final
+
+@[inline] def deltaBy (t : Transition α) (f : α → α → β) : β := f t.final t.initial
+
+@[inline] def delta (t : Transition α) [Diff.Measureable α] : Int :=
+  (Diff.measure t.final : Int) - Diff.measure t.initial
+
+end Transition
+
+/-- A `Transition` with an `initial : Nat` and a `final : Nat`. -/
+abbrev TransitionMeasure := Transition Nat
+
+@[inline] def Transition.measure (t : Transition α) [Diff.Measureable α] : TransitionMeasure :=
+  t.map Diff.measure
+
+namespace TransitionMeasure
+
+def header : Table.Row 4 := #v["", "Δ", "new", "old"]
+
+def toRow (t : TransitionMeasure) (rowHeader : String) : Table.Row 4 :=
+  #v[rowHeader, t.delta.toStringWithSign, s!"{t.final}", s!"{t.initial}"]
+
+end TransitionMeasure
+
+/-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and
+final state. -/
+structure Venn α where
+  /-- What the final state has gained that was not present in the initial state. -/
+  plus   : α
+  /-- What the initial state has lost that is no longer present in the final state. -/
+  minus  : α
+  /-- What the initial and final state have in common. -/
+  shared : α
+
+@[inline] def Transition.toVennBy (t : Transition α) (sdiff : α → α → β) (inter : α → α → β) :
+    Venn β where
+  plus := sdiff t.final t.initial
+  minus := sdiff t.initial t.final
+  shared := inter t.initial t.final
+
+class HVennLike α β where
+  protected sdiff : α → α → β
+  protected inter : α → α → β
+  -- TODO: isEmpty field? isDisjoint?
+
+abbrev VennLike α := HVennLike α α
+
+def Transition.toVenn (t : Transition α) [HVennLike α β] : Venn β :=
+  t.toVennBy HVennLike.sdiff HVennLike.inter
+
+namespace Venn
+
+@[inline] def map (v : Venn α) (f : α → β) : Venn β where
+  plus := f v.plus
+  minus := f v.minus
+  shared := f v.shared
+
+/-- A `v : VennMeasure` represents no change iff `v.plus = v.minus = 0`. -/
+@[inline] def isUnchangedBy (v : Venn α) (isEmpty : α → Bool) :=
+  isEmpty v.plus && isEmpty v.minus
+
+/-- A `v : VennMeasure` represents a change of some kind iff `v.plus` is nonzero or `v.minus` is
+nonzero. -/
+@[inline] def isChangedBy (v : Venn α) (isEmpty : α → Bool) := !(v.isUnchangedBy isEmpty)
+
+/-- Whether the `Venn` diagram implicitly represents a strict increase (`.gt`), a strict decrease
+(`.lt`), no change (`.eq`), or incomparable final and initial states.  -/
+@[inline] def compareBy? (v : Venn α) (isEmpty : α → Bool) : Option Ordering :=
+  match isEmpty v.plus, isEmpty v.minus with
+  | true,  true  => some .eq
+  | true,  false => some .lt
+  | false, true  => some .gt
+  | false, false => none
+
+/-- The net difference between the implicit initial and final state, collapsing the independent
+measurements of `plus` and `minus` together. -/
+@[inline] def delta (v : Venn α) [Diff.Measureable α] : Int :=
+  (Diff.measure v.plus : Int) - Diff.measure v.minus
+
+/-- A `v : VennMeasure` represents no change iff `v.plus = v.minus = 0`. -/
+@[inline] def isUnchanged (v : Venn α) [Diff.Measureable α] :=
+  v.isUnchangedBy (Diff.measure · = 0)
+
+/-- A `v : VennMeasure` represents a change of some kind iff `v.plus` is nonzero or `v.minus` is
+nonzero. -/
+@[inline] def isChanged (v : Venn α) [Diff.Measureable α] :=
+  !v.isUnchanged
+
+@[inline] def compare? (v : Venn α) [Diff.Measureable α] : Option Ordering :=
+  v.compareBy? (Diff.measure · = 0)
+
+end Venn
+
+/-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state
+and final state. -/
+abbrev VennMeasure := Venn Nat
+
+namespace VennMeasure
+
+open ImportGraph Diff
+
+/-- A header row for a table consisting of rows created by `VennMeasure.toRow`. -/
+def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
+
+/-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
+def toRow (rowHeader : String) (t : VennMeasure) : Table.Row 5 := #v[
+  rowHeader,
+  t.delta.toStringWithSign,
+  s!"+{t.plus}",
+  s!"-{t.minus}",
+  s!"{t.shared}"]
+
+end Diff.VennMeasure
diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean
new file mode 100644
index 0000000..53df37d
--- /dev/null
+++ b/ImportGraph/Util/Diff/Shake.lean
@@ -0,0 +1,26 @@
+module
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Shake.Basic
+
+open ImportGraph Diff Shake
+
+instance : Diff.Measureable Bitset where
+  measure b := b.size
+
+instance : VennLike Provides Provides where
+
+
+def ofBitsetTransition (t : Transition Bitset) (ignoredShared : Bitset := ∅) : Venn Bitset :=
+  t.toVennBy (sdiff := (· \ ·)) (inter := fun a b => (a ∩ b) \ ignoredShared)
+
+def ofProvidesTransition (t : Transition Provides) (ignoredShared : Provides := ∅) :
+    Venn Provides :=
+  t.toVennBy
+    (sdiff := (· \ ·))
+    (inter := fun a b => (a.map₂ b (· ∩ ·)) \ ignoredShared |>.linearize)
+
+@[inline] def Venn.measureBitset (v : Venn Bitset) : VennMeasure := v.map (·.size)
+
+def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : VennMeasure :=
+  needs.map (·.get k |>.size)

From cce95da72314a978381b86c823debd3bfbd4d3e2 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 18:29:47 -0500
Subject: [PATCH 05/17] refactor

---
 ImportGraph/Shake/Basic.lean     |  14 +++++
 ImportGraph/Util/Diff/Basic.lean | 103 +++++++++++++++++--------------
 ImportGraph/Util/Diff/Shake.lean |  34 +++++-----
 3 files changed, 91 insertions(+), 60 deletions(-)

diff --git a/ImportGraph/Shake/Basic.lean b/ImportGraph/Shake/Basic.lean
index f31f12f..c2e53b8 100644
--- a/ImportGraph/Shake/Basic.lean
+++ b/ImportGraph/Shake/Basic.lean
@@ -301,6 +301,9 @@ Rephrasing of `f (n.get k)` for readability. -/
 @[inline] def foldWithKind (n : Needs) (f : α → NeedsKind → Bitset → α) (init : α) : α :=
   NeedsKind.all.foldl (init := init) fun a k => n.applyAt k (f a k)
 
+/-- The union of all bitsets in a `Needs`-/
+def flatten (n : Needs) : Bitset := n.fold (· ∪ ·) (init := ∅)
+
 /-- Applies `f` to all component `Bitset`s of the given `Needs`. -/
 @[specialize f] def map (n : Needs) (f : Bitset → Bitset) : Needs where
   pub      := f n.pub
@@ -429,6 +432,17 @@ instance : ToString NeedsKind where
     | .privOfPriv     => "all"
     | .metaPrivOfPriv => "meta all"
 
+/-- The prefix to the import command corresponding to the import. If `clarifyPriv` is `true`,
+(default `false`), we include "`private`" in front of private imports. This is useful in display
+situations, even though it is not a valid form of `import`. -/
+def toImportString (clarifyPriv := false) : NeedsKind → String
+  | .pub      => "public import"
+  | .metaPub  => "public meta import"
+  | .priv     => s!"{if clarifyPriv then "private " else ""}import"
+  | .metaPriv => s!"{if clarifyPriv then "private " else ""}meta import"
+  | .privOfPriv     => "import all"
+  | .metaPrivOfPriv => "meta import all"
+
 /-- The `NeedsKind`s which land (directly) in the private scope. -/
 @[inline, expose, grind] def toPrivate   : Array NeedsKind :=
   #[.priv, .privOfPriv, .metaPriv, .metaPrivOfPriv]
diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index e96586e..fa3045e 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -30,31 +30,30 @@ structure Transition α where
 
 namespace Transition
 
+/-- Apply `f` to both the initial and final state. -/
 @[inline] def map (t : Transition α) (f : α → β) : Transition β where
   initial := f t.initial
   final := f t.final
 
-@[inline] def deltaBy (t : Transition α) (f : α → α → β) : β := f t.final t.initial
-
+/-- The difference between the measures of the `final` state and `initial` state. -/
 @[inline] def delta (t : Transition α) [Diff.Measureable α] : Int :=
-  (Diff.measure t.final : Int) - Diff.measure t.initial
+  (measure t.final : Int) - measure t.initial
 
-end Transition
 
-/-- A `Transition` with an `initial : Nat` and a `final : Nat`. -/
-abbrev TransitionMeasure := Transition Nat
+/-- `abbrev` for `Transition Nat`. The result of measuring a `Transition` with
+`Transition.measure`. -/
+protected abbrev Measured := Transition Nat
 
-@[inline] def Transition.measure (t : Transition α) [Diff.Measureable α] : TransitionMeasure :=
+@[inline] def measure (t : Transition α) [Diff.Measureable α] : Transition.Measured :=
   t.map Diff.measure
 
-namespace TransitionMeasure
-
+/-- A header row for a table consisting of rows created by `Transition.toRow`. -/
 def header : Table.Row 4 := #v["", "Δ", "new", "old"]
 
-def toRow (t : TransitionMeasure) (rowHeader : String) : Table.Row 4 :=
-  #v[rowHeader, t.delta.toStringWithSign, s!"{t.final}", s!"{t.initial}"]
+def toRow (rowHeader : String) (t : Transition α) [Diff.Measureable α] : Table.Row 4 :=
+  #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"]
 
-end TransitionMeasure
+end Transition
 
 /-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and
 final state. -/
@@ -66,35 +65,51 @@ structure Venn α where
   /-- What the initial and final state have in common. -/
   shared : α
 
+/-- Convert a `Transition α` into a `Venn β` according to the provided notions of set difference
+and interesection. Note that this is slightly more general than using a `VennLike α` instance, as
+it allows changing the type to `β` and does not require `isEmpty`. -/
 @[inline] def Transition.toVennBy (t : Transition α) (sdiff : α → α → β) (inter : α → α → β) :
     Venn β where
   plus := sdiff t.final t.initial
   minus := sdiff t.initial t.final
   shared := inter t.initial t.final
 
-class HVennLike α β where
-  protected sdiff : α → α → β
-  protected inter : α → α → β
-  -- TODO: isEmpty field? isDisjoint?
-
-abbrev VennLike α := HVennLike α α
-
-def Transition.toVenn (t : Transition α) [HVennLike α β] : Venn β :=
-  t.toVennBy HVennLike.sdiff HVennLike.inter
+/-- Provides the structure necessary to view `α` as "setlike" enough to support `Venn`, namely a
+means of taking the set difference, a means of intersection, and a notion of emptiness. This
+typeclass is homogeneous, i.e. we assume that `α` itself is sufficient for representing both states
+and the differences/shared aspects between them. -/
+class VennLike α where
+  /-- A "set difference" such that `VennLike.sdiff a b` tells us what `a` has that `b` does not.  -/
+  protected sdiff : α → α → α
+  /--
+  An "intersection" such that `VennLike.inter a b` tells us what is common to both `a` and `b`.
+  -/
+  protected inter : α → α → α
+  /-- A notion of emptiness. `VennLike.isEmpty <| VennLike.sdiff a b = true` should imply that, for
+  the purposes of the Venn diagram, `a` is a "subset" of `b`. (Both directions should indicate
+  equality.) Likewise, `VennLike.isEmpty <| VennLike.inter a b` should imply that `a` is disjoint
+  from `b`. -/
+  protected isEmpty : α → Bool
+
+/-- Convert an `initial` and `final` state into their Venn diagram using the type's `VennLike`
+instance. -/
+def Transition.toVenn (t : Transition α) [VennLike α] : Venn α :=
+  t.toVennBy VennLike.sdiff VennLike.inter
 
 namespace Venn
 
+/-- Apply `f` to each field of `v`. -/
 @[inline] def map (v : Venn α) (f : α → β) : Venn β where
   plus := f v.plus
   minus := f v.minus
   shared := f v.shared
 
-/-- A `v : VennMeasure` represents no change iff `v.plus = v.minus = 0`. -/
+/-- A `v : Venn α` represents no change iff both `isEmpty v.plus` and `isEmpty v.minus`. -/
 @[inline] def isUnchangedBy (v : Venn α) (isEmpty : α → Bool) :=
   isEmpty v.plus && isEmpty v.minus
 
-/-- A `v : VennMeasure` represents a change of some kind iff `v.plus` is nonzero or `v.minus` is
-nonzero. -/
+/-- A `v : Venn α` represents a change of some kind iff `v.plus` is not `isEmpty`  or\
+`v.minus` is not `isEmpty`. -/
 @[inline] def isChangedBy (v : Venn α) (isEmpty : α → Bool) := !(v.isUnchangedBy isEmpty)
 
 /-- Whether the `Venn` diagram implicitly represents a strict increase (`.gt`), a strict decrease
@@ -111,37 +126,35 @@ measurements of `plus` and `minus` together. -/
 @[inline] def delta (v : Venn α) [Diff.Measureable α] : Int :=
   (Diff.measure v.plus : Int) - Diff.measure v.minus
 
-/-- A `v : VennMeasure` represents no change iff `v.plus = v.minus = 0`. -/
-@[inline] def isUnchanged (v : Venn α) [Diff.Measureable α] :=
-  v.isUnchangedBy (Diff.measure · = 0)
+/-- A `v : VennMeasure` represents no change iff both `v.plus` and `v.minus` satisfy
+`VennLike.isEmpty`. -/
+@[inline] def isUnchanged (v : Venn α) [VennLike α] :=
+  v.isUnchangedBy VennLike.isEmpty
 
-/-- A `v : VennMeasure` represents a change of some kind iff `v.plus` is nonzero or `v.minus` is
-nonzero. -/
-@[inline] def isChanged (v : Venn α) [Diff.Measureable α] :=
+/-- A `v : VennMeasure` represents a change of some kind iff either `v.plus` is not empty or
+`v.minus` is not empty, according to `VennLike.isEmpty`. -/
+@[inline] def isChanged (v : Venn α) [VennLike α] :=
   !v.isUnchanged
 
-@[inline] def compare? (v : Venn α) [Diff.Measureable α] : Option Ordering :=
-  v.compareBy? (Diff.measure · = 0)
-
-end Venn
+/-- Whether the `Venn` diagram implicitly represents a strict increase (`.gt`), a strict decrease
+(`.lt`), no change (`.eq`), or incomparable final and initial states, according to
+`VennLike.isEmpty`. -/
+@[inline] def compare? (v : Venn α) [VennLike α] : Option Ordering :=
+  v.compareBy? VennLike.isEmpty
 
 /-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state
-and final state. -/
-abbrev VennMeasure := Venn Nat
-
-namespace VennMeasure
-
-open ImportGraph Diff
+and final state. Abbrev for `Venn Nat`. -/
+protected abbrev Measured := Venn Nat
 
 /-- A header row for a table consisting of rows created by `VennMeasure.toRow`. -/
 def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
 
 /-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
-def toRow (rowHeader : String) (t : VennMeasure) : Table.Row 5 := #v[
+def toRow (rowHeader : String) (t : Venn α) [Diff.Measureable α]: Table.Row 5 := #v[
   rowHeader,
   t.delta.toStringWithSign,
-  s!"+{t.plus}",
-  s!"-{t.minus}",
-  s!"{t.shared}"]
+  s!"+{measure t.plus}",
+  s!"-{measure t.minus}",
+  s!"{measure t.shared}"]
 
-end Diff.VennMeasure
+end Diff.Venn
diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean
index 53df37d..a12292d 100644
--- a/ImportGraph/Util/Diff/Shake.lean
+++ b/ImportGraph/Util/Diff/Shake.lean
@@ -1,26 +1,30 @@
 module
 
 public import ImportGraph.Util.Diff.Basic
-public import ImportGraph.Shake.Basic
+public import ImportGraph.Shake.Algebra
 
-open ImportGraph Diff Shake
+public section
 
-instance : Diff.Measureable Bitset where
-  measure b := b.size
+namespace ImportGraph.Diff
 
-instance : VennLike Provides Provides where
+open ImportGraph Diff Shake
 
+instance : Diff.Measureable Bitset where
+  measure := (·.size)
 
-def ofBitsetTransition (t : Transition Bitset) (ignoredShared : Bitset := ∅) : Venn Bitset :=
-  t.toVennBy (sdiff := (· \ ·)) (inter := fun a b => (a ∩ b) \ ignoredShared)
+instance : VennLike Bitset where
+  sdiff := (· \ ·)
+  inter := (· ∩ ·)
+  isEmpty := (·.isEmpty)
 
-def ofProvidesTransition (t : Transition Provides) (ignoredShared : Provides := ∅) :
-    Venn Provides :=
-  t.toVennBy
-    (sdiff := (· \ ·))
-    (inter := fun a b => (a.map₂ b (· ∩ ·)) \ ignoredShared |>.linearize)
+/-- Measures the Venn diagram of `Bitset`s at the given `NeedsKind`. -/
+def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : Venn.Measured :=
+  needs.map (·.get k |>.size)
 
-@[inline] def Venn.measureBitset (v : Venn Bitset) : VennMeasure := v.map (·.size)
+instance : Diff.Measureable Provides where
+  measure := (·.flatten.size)
 
-def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : VennMeasure :=
-  needs.map (·.get k |>.size)
+instance : VennLike Provides where
+  sdiff := (· \ ·)
+  inter a b := a.map₂ b (· ∩ ·) |>.linearize
+  isEmpty := (·.isEmpty)

From ad1dbcf54e43c513a57d5abd9470f7ffe10f1afd Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 18:44:28 -0500
Subject: [PATCH 06/17] chore: copyright

---
 ImportGraph/Util/Diff/Basic.lean | 5 +++++
 ImportGraph/Util/Diff/Shake.lean | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index fa3045e..459c3ab 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
 module
 
 public import ImportGraph.Util.TableMessage
diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean
index a12292d..cc20516 100644
--- a/ImportGraph/Util/Diff/Shake.lean
+++ b/ImportGraph/Util/Diff/Shake.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
 module
 
 public import ImportGraph.Util.Diff.Basic

From db936f13fb327613ada8758eeaf6f9d06c874070 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 18:48:51 -0500
Subject: [PATCH 07/17] chore: factor intersection

---
 ImportGraph/Shake/Basic.lean     | 14 +++++++++++++-
 ImportGraph/Util/Diff/Shake.lean |  4 +++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/ImportGraph/Shake/Basic.lean b/ImportGraph/Shake/Basic.lean
index c2e53b8..cd74b89 100644
--- a/ImportGraph/Shake/Basic.lean
+++ b/ImportGraph/Shake/Basic.lean
@@ -544,4 +544,16 @@ def connecting? (src tgt : Environment.Visibility) (isMeta : Bool := false) : Op
   | .private, .private => some { isExported := false, isMeta, isAll := true }
   | .private, .public  => none
 
-end ImportGraph.Shake.NeedsKind
+end NeedsKind
+
+namespace Provides
+
+/-- Intersects each field of two `Provides`.
+
+Generally, intersection is not meaningful on a bare `Needs`, but is meaningful on a
+transitively closed and linearized `Provides`.
+
+We avoid making this an instance of `Inter` to avoid `a ∩ b` succeeding on `Needs`. -/
+@[inline] def inter (a b : Provides) := a.map₂ b (· ∩ ·)
+
+end Provides
diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean
index cc20516..9df3781 100644
--- a/ImportGraph/Util/Diff/Shake.lean
+++ b/ImportGraph/Util/Diff/Shake.lean
@@ -30,6 +30,8 @@ instance : Diff.Measureable Provides where
   measure := (·.flatten.size)
 
 instance : VennLike Provides where
+  -- avoid linearizing to capture one `Provides` providing public while the other provides public
   sdiff := (· \ ·)
-  inter a b := a.map₂ b (· ∩ ·) |>.linearize
+  -- `a` and `b` should be linearized already and remain linearized under intersection
+  inter := Provides.inter
   isEmpty := (·.isEmpty)

From 1ecdd25abc586dbc74ee87b98db3ffaf13484ec5 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 18:57:22 -0500
Subject: [PATCH 08/17] chore: oops, fix spelling

---
 ImportGraph/Util/Diff/Basic.lean | 16 ++++++++--------
 ImportGraph/Util/Diff/Shake.lean |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index 459c3ab..8ed2c8e 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -15,11 +15,11 @@ namespace ImportGraph
 
 namespace Diff
 
-protected class Measureable α where
+protected class Measurable α where
   measure : α → Nat
-export Measureable (measure)
+export Measurable (measure)
 
-instance : Diff.Measureable Nat := ⟨id⟩
+instance : Diff.Measurable Nat := ⟨id⟩
 
 open Diff
 
@@ -41,7 +41,7 @@ namespace Transition
   final := f t.final
 
 /-- The difference between the measures of the `final` state and `initial` state. -/
-@[inline] def delta (t : Transition α) [Diff.Measureable α] : Int :=
+@[inline] def delta (t : Transition α) [Diff.Measurable α] : Int :=
   (measure t.final : Int) - measure t.initial
 
 
@@ -49,13 +49,13 @@ namespace Transition
 `Transition.measure`. -/
 protected abbrev Measured := Transition Nat
 
-@[inline] def measure (t : Transition α) [Diff.Measureable α] : Transition.Measured :=
+@[inline] def measure (t : Transition α) [Diff.Measurable α] : Transition.Measured :=
   t.map Diff.measure
 
 /-- A header row for a table consisting of rows created by `Transition.toRow`. -/
 def header : Table.Row 4 := #v["", "Δ", "new", "old"]
 
-def toRow (rowHeader : String) (t : Transition α) [Diff.Measureable α] : Table.Row 4 :=
+def toRow (rowHeader : String) (t : Transition α) [Diff.Measurable α] : Table.Row 4 :=
   #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"]
 
 end Transition
@@ -128,7 +128,7 @@ namespace Venn
 
 /-- The net difference between the implicit initial and final state, collapsing the independent
 measurements of `plus` and `minus` together. -/
-@[inline] def delta (v : Venn α) [Diff.Measureable α] : Int :=
+@[inline] def delta (v : Venn α) [Diff.Measurable α] : Int :=
   (Diff.measure v.plus : Int) - Diff.measure v.minus
 
 /-- A `v : VennMeasure` represents no change iff both `v.plus` and `v.minus` satisfy
@@ -155,7 +155,7 @@ protected abbrev Measured := Venn Nat
 def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
 
 /-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
-def toRow (rowHeader : String) (t : Venn α) [Diff.Measureable α]: Table.Row 5 := #v[
+def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[
   rowHeader,
   t.delta.toStringWithSign,
   s!"+{measure t.plus}",
diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean
index 9df3781..e3a829f 100644
--- a/ImportGraph/Util/Diff/Shake.lean
+++ b/ImportGraph/Util/Diff/Shake.lean
@@ -14,7 +14,7 @@ namespace ImportGraph.Diff
 
 open ImportGraph Diff Shake
 
-instance : Diff.Measureable Bitset where
+instance : Diff.Measurable Bitset where
   measure := (·.size)
 
 instance : VennLike Bitset where
@@ -26,7 +26,7 @@ instance : VennLike Bitset where
 def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : Venn.Measured :=
   needs.map (·.get k |>.size)
 
-instance : Diff.Measureable Provides where
+instance : Diff.Measurable Provides where
   measure := (·.flatten.size)
 
 instance : VennLike Provides where

From 55fcb9a4bd5ee6efe0767c71eda1f42e770e32e1 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 19:01:09 -0500
Subject: [PATCH 09/17] chore: move table into other file

---
 ImportGraph/Util/Diff/Basic.lean   | 19 ----------------
 ImportGraph/Util/Diff/Message.lean | 35 ++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 19 deletions(-)
 create mode 100644 ImportGraph/Util/Diff/Message.lean

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index 8ed2c8e..2cbbe82 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -5,8 +5,6 @@ Authors: Thomas R. Murrills
 -/
 module
 
-public import ImportGraph.Util.TableMessage
-
 public section
 
 open Lean
@@ -52,12 +50,6 @@ protected abbrev Measured := Transition Nat
 @[inline] def measure (t : Transition α) [Diff.Measurable α] : Transition.Measured :=
   t.map Diff.measure
 
-/-- A header row for a table consisting of rows created by `Transition.toRow`. -/
-def header : Table.Row 4 := #v["", "Δ", "new", "old"]
-
-def toRow (rowHeader : String) (t : Transition α) [Diff.Measurable α] : Table.Row 4 :=
-  #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"]
-
 end Transition
 
 /-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and
@@ -151,15 +143,4 @@ measurements of `plus` and `minus` together. -/
 and final state. Abbrev for `Venn Nat`. -/
 protected abbrev Measured := Venn Nat
 
-/-- A header row for a table consisting of rows created by `VennMeasure.toRow`. -/
-def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
-
-/-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
-def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[
-  rowHeader,
-  t.delta.toStringWithSign,
-  s!"+{measure t.plus}",
-  s!"-{measure t.minus}",
-  s!"{measure t.shared}"]
-
 end Diff.Venn
diff --git a/ImportGraph/Util/Diff/Message.lean b/ImportGraph/Util/Diff/Message.lean
new file mode 100644
index 0000000..3ea1db2
--- /dev/null
+++ b/ImportGraph/Util/Diff/Message.lean
@@ -0,0 +1,35 @@
+module
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Util.TableMessage
+
+public section
+
+namespace ImportGraph.Diff
+
+open ImportGraph.Diff
+
+namespace Transition
+
+/-- A header row for a table consisting of rows created by `Transition.toRow`. -/
+def header : Table.Row 4 := #v["", "Δ", "new", "old"]
+
+def toRow (rowHeader : String) (t : Transition α) [Diff.Measurable α] : Table.Row 4 :=
+  #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"]
+
+end Transition
+
+namespace Venn
+
+/-- A header row for a table consisting of rows created by `Venn.toRow`. -/
+def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
+
+/-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
+def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[
+  rowHeader,
+  t.delta.toStringWithSign,
+  s!"+{measure t.plus}",
+  s!"-{measure t.minus}",
+  s!"{measure t.shared}"]
+
+end Venn

From 7a44c09596ef60c6871b0e083d14eba85ee52394 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 19:08:37 -0500
Subject: [PATCH 10/17] chore: basic derivings (needs Type instead of Sort)

---
 ImportGraph/Util/Diff/Basic.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index 2cbbe82..0b607a3 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -25,11 +25,12 @@ open Diff
 def Int.toStringWithSign (i : Int) := if i > 0 then s!"+{i}" else s!"{i}"
 
 /-- A simple structure with two states, `initial : α` and `final : α`, which models a transition. -/
-structure Transition α where
+structure Transition (α : Type u) where
   /-- The state before `final`. -/
   initial : α
   /-- The state after `initial`. -/
   final : α
+deriving Inhabited, Hashable, BEq, Repr
 
 namespace Transition
 
@@ -42,7 +43,6 @@ namespace Transition
 @[inline] def delta (t : Transition α) [Diff.Measurable α] : Int :=
   (measure t.final : Int) - measure t.initial
 
-
 /-- `abbrev` for `Transition Nat`. The result of measuring a `Transition` with
 `Transition.measure`. -/
 protected abbrev Measured := Transition Nat
@@ -54,13 +54,14 @@ end Transition
 
 /-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and
 final state. -/
-structure Venn α where
+structure Venn (α : Type u) where
   /-- What the final state has gained that was not present in the initial state. -/
   plus   : α
   /-- What the initial state has lost that is no longer present in the final state. -/
   minus  : α
   /-- What the initial and final state have in common. -/
   shared : α
+deriving Inhabited, Hashable, BEq, Repr
 
 /-- Convert a `Transition α` into a `Venn β` according to the provided notions of set difference
 and interesection. Note that this is slightly more general than using a `VennLike α` instance, as

From 355cfc0191a81425e84b9382f3662b68e38e949f Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 19:15:35 -0500
Subject: [PATCH 11/17] chore: importing files

---
 ImportGraph.lean           | 1 +
 ImportGraph/Util/Diff.lean | 5 +++++
 2 files changed, 6 insertions(+)
 create mode 100644 ImportGraph/Util/Diff.lean

diff --git a/ImportGraph.lean b/ImportGraph.lean
index 0ba9185..37cfd08 100644
--- a/ImportGraph.lean
+++ b/ImportGraph.lean
@@ -23,6 +23,7 @@ public import ImportGraph.Shake.DeclNeeds
 public import ImportGraph.Shake.EnvExtension
 public import ImportGraph.Shake.Environment
 public import ImportGraph.Shake.Workspace
+public import ImportGraph.Util.Diff
 public import ImportGraph.Util.FindSorry
 public import ImportGraph.Util.TableMessage
 public import ImportGraph.WorkspaceModel.Base
diff --git a/ImportGraph/Util/Diff.lean b/ImportGraph/Util/Diff.lean
new file mode 100644
index 0000000..9dcae5f
--- /dev/null
+++ b/ImportGraph/Util/Diff.lean
@@ -0,0 +1,5 @@
+module
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Util.Diff.Message
+public import ImportGraph.Util.Diff.Shake

From 34899c2ded24c83b2a0bdef01b4375502e3b3279 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 20:54:29 -0500
Subject: [PATCH 12/17] chore: `Venn.measure`

---
 ImportGraph/Util/Diff/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index 0b607a3..7fada95 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -144,4 +144,7 @@ measurements of `plus` and `minus` together. -/
 and final state. Abbrev for `Venn Nat`. -/
 protected abbrev Measured := Venn Nat
 
+@[inline] def measure (t : Venn α) [Diff.Measurable α] : Venn.Measured :=
+  t.map Diff.measure
+
 end Diff.Venn

From 2e642bcec242e7d50f721dfcc33685d2b5634dbc Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 20:55:08 -0500
Subject: [PATCH 13/17] chore: fix test import

---
 ImportGraphTest/TableMessage.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/ImportGraphTest/TableMessage.lean b/ImportGraphTest/TableMessage.lean
index 0d3f4e1..3f54368 100644
--- a/ImportGraphTest/TableMessage.lean
+++ b/ImportGraphTest/TableMessage.lean
@@ -1,7 +1,8 @@
 module
 
+public meta import Lean.Elab.Command
+
 import ImportGraph.Util.TableMessage
-import Lean.Elab.Command
 
 open ImportGraph
 

From 6078e23f7bac19feb94924725160cd8db611acf9 Mon Sep 17 00:00:00 2001
From: thorimur <thomasmurrills@gmail.com>
Date: Sat, 7 Nov 2026 20:58:25 -0500
Subject: [PATCH 14/17] chore: fix

---
 ImportGraph/Util/Diff/Message.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/ImportGraph/Util/Diff/Message.lean b/ImportGraph/Util/Diff/Message.lean
index 3ea1db2..7229e9a 100644
--- a/ImportGraph/Util/Diff/Message.lean
+++ b/ImportGraph/Util/Diff/Message.lean
@@ -28,8 +28,8 @@ def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
 def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[
   rowHeader,
   t.delta.toStringWithSign,
-  s!"+{measure t.plus}",
-  s!"-{measure t.minus}",
-  s!"{measure t.shared}"]
+  s!"+{Diff.measure t.plus}",
+  s!"-{Diff.measure t.minus}",
+  s!"{Diff.measure t.shared}"]
 
 end Venn

From 209df8788595986c74877439c01597362c5633ca Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 7 Nov 2026 21:09:50 -0500
Subject: [PATCH 15/17] chore: oops, reversed

---
 ImportGraphTest/TableMessage.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ImportGraphTest/TableMessage.lean b/ImportGraphTest/TableMessage.lean
index 3f54368..16dc1e1 100644
--- a/ImportGraphTest/TableMessage.lean
+++ b/ImportGraphTest/TableMessage.lean
@@ -1,8 +1,8 @@
 module
 
-public meta import Lean.Elab.Command
+public meta import ImportGraph.Util.TableMessage
 
-import ImportGraph.Util.TableMessage
+import Lean.Elab.Command
 
 open ImportGraph
 

From 843197be6987ccc59a1907b6e1727780b60f84c8 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sun, 8 Nov 2026 17:32:22 -0500
Subject: [PATCH 16/17] chore: docs, modifyShared

---
 ImportGraph/Util/Diff/Basic.lean | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index 7fada95..b06a5de 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -110,8 +110,13 @@ namespace Venn
 `v.minus` is not `isEmpty`. -/
 @[inline] def isChangedBy (v : Venn α) (isEmpty : α → Bool) := !(v.isUnchangedBy isEmpty)
 
-/-- Whether the `Venn` diagram implicitly represents a strict increase (`.gt`), a strict decrease
-(`.lt`), no change (`.eq`), or incomparable final and initial states.  -/
+/-- If comparable, the relationship `final ≷ initial`, according to the provided notion of
+`isEmpty`.
+
+- `some .gt`: the `Venn` diagram implicitly represents a strict increase
+- `some .lt`: the `Venn` diagram implicitly represents a strict decrease
+- `some .eq`: no change in state at all
+- `none`: incomparable states (some increase, some decrease) -/
 @[inline] def compareBy? (v : Venn α) (isEmpty : α → Bool) : Option Ordering :=
   match isEmpty v.plus, isEmpty v.minus with
   | true,  true  => some .eq
@@ -134,12 +139,20 @@ measurements of `plus` and `minus` together. -/
 @[inline] def isChanged (v : Venn α) [VennLike α] :=
   !v.isUnchanged
 
-/-- Whether the `Venn` diagram implicitly represents a strict increase (`.gt`), a strict decrease
-(`.lt`), no change (`.eq`), or incomparable final and initial states, according to
-`VennLike.isEmpty`. -/
+/-- If comparable, the relationship `final ≷ initial`.
+
+- `some .gt`: the `Venn` diagram implicitly represents a strict increase
+- `some .lt`: the `Venn` diagram implicitly represents a strict decrease
+- `some .eq`: no change in state at all
+- `none`: incomparable states (some increase, some decrease)
+
+The presence of a change is determined by `VennLike.isEmpty`. -/
 @[inline] def compare? (v : Venn α) [VennLike α] : Option Ordering :=
   v.compareBy? VennLike.isEmpty
 
+/-- Apply `f` to the `shared` field. -/
+@[inline] def modifyShared (v : Venn α) (f : α → α) : Venn α := { v with shared := f v.shared }
+
 /-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state
 and final state. Abbrev for `Venn Nat`. -/
 protected abbrev Measured := Venn Nat

From aabed7e8b24459720a306f8538dd7c7ab9da4f37 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sun, 8 Nov 2026 17:37:09 -0500
Subject: [PATCH 17/17] chore: ignoreShared

---
 ImportGraph/Util/Diff/Basic.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean
index b06a5de..910ac8a 100644
--- a/ImportGraph/Util/Diff/Basic.lean
+++ b/ImportGraph/Util/Diff/Basic.lean
@@ -153,6 +153,10 @@ The presence of a change is determined by `VennLike.isEmpty`. -/
 /-- Apply `f` to the `shared` field. -/
 @[inline] def modifyShared (v : Venn α) (f : α → α) : Venn α := { v with shared := f v.shared }
 
+/-- Removes `ignored` from the `shared` field, according to `VennLike.sdiff`. This is useful when we want to ignore "obvious" common factors. -/
+def ignoreShared (ignored : α) (v : Venn α) [VennLike α] : Venn α :=
+  v.modifyShared (VennLike.sdiff · ignored)
+
 /-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state
 and final state. Abbrev for `Venn Nat`. -/
 protected abbrev Measured := Venn Nat