diff --git a/LeanPool.lean b/LeanPool.lean
index 7955865c08..704077a5af 100644
--- a/LeanPool.lean
+++ b/LeanPool.lean
@@ -860,15 +860,23 @@ import LeanPool.PolyaEnumerationTheorem.PermutationAuxiliary
 import LeanPool.PolyaEnumerationTheorem.ReductionToFin
 import LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum
 import LeanPool.Polylean
+import LeanPool.Polylean.Complexes
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
 import LeanPool.Polylean.Complexes.GraphPaths
 import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
 import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
 import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+import LeanPool.Polylean.ConjInvLength
 import LeanPool.Polylean.ConjInvLength.Length
 import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
 import LeanPool.Polylean.ConjInvLength.MemoLength
 import LeanPool.Polylean.ConjInvLength.ProvedBound
 import LeanPool.Polylean.ConjInvLength.WordTree
+import LeanPool.Polylean.Polymath
 import LeanPool.Polylean.UnitConjecture
 import LeanPool.Polylean.UnitConjecture.AddFreeGroup
 import LeanPool.Polylean.UnitConjecture.Cocycle
@@ -880,6 +888,7 @@ import LeanPool.Polylean.UnitConjecture.GroupRing
 import LeanPool.Polylean.UnitConjecture.MetabelianGroup
 import LeanPool.Polylean.UnitConjecture.Tactics
 import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets
+import LeanPool.Polylean.UnitConjecture.Tactics.ReduceGoal
 import LeanPool.Polylean.UnitConjecture.TorsionFree
 import LeanPool.QuasiBorelSpaces
 import LeanPool.QuasiBorelSpaces.Basic
diff --git a/LeanPool/Polylean.lean b/LeanPool/Polylean.lean
index e153051e7a..1821c84efe 100644
--- a/LeanPool/Polylean.lean
+++ b/LeanPool/Polylean.lean
@@ -5,15 +5,23 @@ Authors: Siddhartha Gadgil, Anand Rao
 -/
 
 import LeanPool.Polylean.UnitConjecture
+import LeanPool.Polylean.Complexes
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
 import LeanPool.Polylean.Complexes.GraphPaths
 import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
 import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
 import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+import LeanPool.Polylean.ConjInvLength
 import LeanPool.Polylean.ConjInvLength.Length
 import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
 import LeanPool.Polylean.ConjInvLength.MemoLength
 import LeanPool.Polylean.ConjInvLength.ProvedBound
 import LeanPool.Polylean.ConjInvLength.WordTree
+import LeanPool.Polylean.Polymath
 
 /-!
 # Polylean Unit Conjecture Counterexample
diff --git a/LeanPool/Polylean/Complexes.lean b/LeanPool/Polylean/Complexes.lean
new file mode 100644
index 0000000000..d3cbc25b21
--- /dev/null
+++ b/LeanPool/Polylean/Complexes.lean
@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
+import LeanPool.Polylean.Complexes.GraphPaths
+import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
+import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+
+/-!
+# Complexes
+
+Import index for the Polylean complex and groupoid structures that are
+available without upstream `sorry`s.
+-/
diff --git a/LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean b/LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean
new file mode 100644
index 0000000000..9330db3649
--- /dev/null
+++ b/LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
+
+namespace LeanPool.Polylean
+
+/-!
+# Universal Covers
+
+This upstream file currently contains only commented exploratory code after the
+`FreeGroupoid` import, so the Lean Pool port keeps the importable module stub.
+-/
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean b/LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean
new file mode 100644
index 0000000000..9c0e80c43e
--- /dev/null
+++ b/LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+
+namespace LeanPool.Polylean
+
+universe u vq vg
+
+namespace FreeGroupoid
+
+/-- The definition of a free groupoid with basis `Q`. -/
+class Struct {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S) where
+  /-- Map each generating quiver edge into the generated groupoid. -/
+  map : {X Y : S} → Q.hom X Y → G.hom X Y
+  /-- Extend a quiver pre-functor out of the basis to a groupoid functor. -/
+  inducedMap : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      Quiver.PreFunctor Q G'.toQuiver → Groupoid.Functor G G'
+
+/-- The inclusion of a quiver into a groupoid generated freely by it. -/
+def ι {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S)
+    [FreeGroupoid.Struct Q G] :
+    Quiver.PreFunctor Q G.toQuiver :=
+  { obj := id, map := FreeGroupoid.Struct.map }
+
+end FreeGroupoid
+
+/-- The universal property characterizing a free groupoid on a quiver. -/
+class FreeGroupoid {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S) extends
+    _root_.LeanPool.Polylean.FreeGroupoid.Struct Q G where
+  induced_extends : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      (φ : Quiver.PreFunctor Q G'.toQuiver) →
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G)
+          (inducedMap φ).toPreFunctor = φ
+  induced_unique : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      (Φ Ψ : Groupoid.Functor G G') →
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G) Φ.toPreFunctor =
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G) Ψ.toPreFunctor →
+          Φ = Ψ
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/Complexes/Structures/Invertegory.lean b/LeanPool/Polylean/Complexes/Structures/Invertegory.lean
new file mode 100644
index 0000000000..ed7b179e00
--- /dev/null
+++ b/LeanPool/Polylean/Complexes/Structures/Invertegory.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Category
+
+namespace LeanPool.Polylean
+
+/-!
+`Invertegory` is an intermediate structure between a category and a groupoid:
+every morphism has a formal inverse, but the inverse is not required to satisfy
+the groupoid inverse laws.
+-/
+
+/-- A category equipped with formal inverses for all morphisms. -/
+class Invertegory (Obj : Sort _) extends Category Obj where
+  /-- Formal inverse of a morphism. -/
+  inv : {X Y : Obj} → (X ⟶ Y) → (Y ⟶ X)
+  invInv : ∀ e : X ⟶ Y, inv (inv e) = e
+
+namespace Invertegory
+
+/-- A morphism of `Invertegory`s preserving formal inverses. -/
+structure Functor {C D : Sort _} (ℭ : Invertegory C) (𝔇 : Invertegory D)
+    extends Category.Functor ℭ.toCategory 𝔇.toCategory where
+  mapInv : {X Y : C} → {f : X ⟶ Y} → map (Invertegory.inv f) = Invertegory.inv (map f)
+
+attribute [simp] Functor.mapInv
+
+end Invertegory
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/Complexes/Structures/TwoComplex.lean b/LeanPool/Polylean/Complexes/Structures/TwoComplex.lean
new file mode 100644
index 0000000000..d6b9e37cd8
--- /dev/null
+++ b/LeanPool/Polylean/Complexes/Structures/TwoComplex.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+
+namespace LeanPool.Polylean
+
+universe u vq vg
+
+/-!
+A two-complex is defined by an underlying quiver, a groupoid whose morphisms
+represent path-homotopy classes of the one-complex, and a pre-functor from the
+quiver to that groupoid.
+
+The lifting principle below says the groupoid has no extra edges beyond those
+generated by the quiver modulo the identifications represented by `map`.
+-/
+
+/-- A two-complex presented by a quiver and its path-homotopy groupoid. -/
+class TwoComplex (V : Sort u) [Q : Quiver.{u, vq} V] [H : Groupoid.{u, vg} V] extends
+    Quiver.PreFunctor Q H.toQuiver where
+  /-- Lift a compatible quiver pre-functor to a groupoid functor. -/
+  lift : {W : Sort u} → [G : Groupoid.{u, vg} W] →
+    (F : Quiver.PreFunctor Q G.toQuiver) →
+    (∀ {X Y : V} {e e' : X ⟶ Y}, map e = map e' → F.map e = F.map e') →
+      Groupoid.Functor H G
+  /-- The lifted functor extends the original quiver pre-functor. -/
+  lift_comp : {W : Sort u} → [G : Groupoid.{u, vg} W] →
+    (F : Quiver.PreFunctor Q G.toQuiver) →
+    (h : ∀ {X Y : V} {e e' : X ⟶ Y}, map e = map e' → F.map e = F.map e') →
+      Quiver.PreFunctor.comp ⟨obj, map⟩ (lift F h).toPreFunctor = F
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/ConjInvLength.lean b/LeanPool/Polylean/ConjInvLength.lean
new file mode 100644
index 0000000000..4b65d89a66
--- /dev/null
+++ b/LeanPool/Polylean/ConjInvLength.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.ConjInvLength.Length
+import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
+import LeanPool.Polylean.ConjInvLength.MemoLength
+import LeanPool.Polylean.ConjInvLength.ProvedBound
+import LeanPool.Polylean.ConjInvLength.WordTree
+
+/-!
+# Conjugacy-Invariant Length
+
+Import index for the Polylean conjugacy-invariant length computations.
+-/
diff --git a/LeanPool/Polylean/ConjInvLength/LengthNode.lean b/LeanPool/Polylean/ConjInvLength/LengthNode.lean
new file mode 100644
index 0000000000..295f58cad4
--- /dev/null
+++ b/LeanPool/Polylean/ConjInvLength/LengthNode.lean
@@ -0,0 +1,212 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.ConjInvLength.Length
+import Std.Data.HashMap
+
+/-!
+# Cached proof nodes for conjugacy-invariant length bounds
+-/
+
+namespace LeanPool.Polylean
+
+/-- A node recording which inequality or equality was used to derive a word-length bound. -/
+inductive ProofNode : Type
+| empty : ProofNode
+| gen : (l : Letter) → ProofNode
+| triang : (w₁ w₂ : Wrd) → ProofNode
+| conj : (l : Letter) → (w : Wrd) → ProofNode
+| power : (n : Nat) → (w : Wrd) → ProofNode
+deriving Repr, BEq
+
+open ProofNode
+
+namespace ProofNode
+
+/-- The word whose length bound is justified by a proof node. -/
+def top : ProofNode → Wrd
+| empty => #[]
+| gen l => #[l]
+| triang w₁ w₂ => w₁ ++ w₂
+| conj l w => w ^ l
+| power _ w => w
+
+/-- Render a proof node as a human-readable proof step. -/
+def toString : ProofNode → String
+| empty => "l(e) = 0 (trivial word)"
+| gen l => s!"l({l}) = 1 (normalization)"
+| triang w₁ w₂ => s!"l({w₁ ++ w₂}) ≤ l({w₁}) + l({w₂}) (triangle inequality)"
+| conj l w => s!"l({w}^{l}) = l({w}) (conjugacy invariance)"
+| power n w => s!"l(w) ≤  l({w^n})/{n} (homogeneity)"
+
+instance : ToString ProofNode := ⟨ProofNode.toString⟩
+
+/-- The previously derived words needed by this proof node. -/
+def base : ProofNode → List Wrd
+| empty => []
+| gen _ => []
+| triang w₁ w₂ => [w₁, w₂]
+| conj _ w => [w]
+| power n w => [w ^ n]
+
+
+/-- Length immediately justified by a base proof node, if any. -/
+def baseLength : ProofNode → Option Nat
+| empty => some 0
+| gen _ => some 1
+| _ => none
+
+end ProofNode
+
+
+/-- Cache of floating-point length bounds for array-backed words. -/
+initialize floatNormCache :
+    IO.Ref (Std.HashMap Wrd Float) ← IO.mkRef Std.HashMap.emptyWithCapacity
+
+/-- Cache of proof nodes witnessing the best known bound for each word. -/
+initialize proofCache :
+    IO.Ref (Std.HashMap Wrd ProofNode) ← IO.mkRef Std.HashMap.emptyWithCapacity
+
+/-- Look up a cached floating-point length bound. -/
+private def cacheLength? (w : Wrd) : IO (Option Float) :=
+    do
+    let cache ← floatNormCache.get
+    match cache.get? w with
+    | some n => pure (some n)
+    | none => pure none
+
+/-- Compute a floating-point length bound while caching the proof nodes used. -/
+def lengthNodes (w : Wrd) : IO Float := do
+  match ← cacheLength? w with
+  | some n =>
+      pure n
+  | none =>
+    match h : w.size with
+    | 0 =>
+      floatNormCache.set <| (← floatNormCache.get).insert #[] 0
+      proofCache.set <| (← proofCache.get).insert #[] empty
+      return 0
+    | m + 1 => do
+      let x := w.back
+      let ys : Wrd := w.pop
+      have ysize : ys.size = m := by
+        rw [Array.size_pop, h]
+        rfl
+      have _ : ys.size < w.size := by
+        rw [ysize, h]
+        exact Nat.lt_succ_self m
+      let base := 1 + (← lengthNodes ys)
+      let derived ←  (ys.splits x⁻¹).mapM fun ⟨(fst, snd), hfst_snd⟩ => do
+        have hsplit : fst.size + snd.size < w.size := by
+          rw [h, ← ysize]
+          exact Nat.lt_trans hfst_snd (Nat.lt_succ_self _)
+        have _ : fst.size < w.size := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) hsplit
+        have _ : snd.size < w.size := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) hsplit
+        return ((← lengthNodes fst) + (← lengthNodes snd), fst, snd)
+      let (res, nodes) := derived.foldl (
+          fun (l₁, ns) (l₂, fst, snd) =>
+            if l₂ < l₁ then (l₂, [triang fst (snd^(x⁻¹)), conj (x⁻¹) snd]) else (l₁, ns)
+      ) (base, [gen x, triang ys #[x]])
+      floatNormCache.set <| (← floatNormCache.get).insert w res
+      for node in nodes do
+        proofCache.set <| (← proofCache.get).insert (node.top) node
+      return res
+termination_by w.size
+
+/-- Improve a word-length bound using a power of the word. -/
+def powerLength : Wrd → Nat → IO Float
+| w, n => do
+  let pl ← lengthNodes (w ^ n)
+  let res := pl / n.toFloat
+  match ← cacheLength? w with
+  | none =>
+    floatNormCache.set <| (← floatNormCache.get).insert w res
+    if n > 1 then
+      proofCache.set <| (← proofCache.get).insert w (power n w)
+    return res
+  | some l₀ =>
+    if res < l₀ then
+      IO.println s!"updated cache for {w}"
+      floatNormCache.set <| (← floatNormCache.get).insert w res
+      if n > 1 then
+        proofCache.set <| (← proofCache.get).insert w (power n w)
+      return res
+    else
+      return l₀
+
+/-- Recursively expand cached proof nodes with a bounded traversal fuel. -/
+private def resolveProofWithFuel : Nat → Wrd → IO ((List ProofNode) × (List Wrd))
+| 0, w => return ([], [w])
+| fuel + 1, w => do
+  let cache ← proofCache.get
+  match cache.get? w with
+  | none => return ([], [w])
+  | some node =>
+    let ws := node.base
+    let offspring ←  ws.mapM (resolveProofWithFuel fuel)
+    return offspring.foldl (fun (ns, ws) (ns', ws') => (ns ++ ns', ws ++ ws') ) ([node], [])
+
+/-- Recursively expand cached proof nodes needed to justify a word. -/
+def resolveProof (w : Wrd) : IO ((List ProofNode) × (List Wrd)) := do
+  let cache ← proofCache.get
+  resolveProofWithFuel (cache.size + 1) w
+
+/-- Recompute a derived length with a bounded traversal fuel. -/
+private def derivedLengthWithFuel : Nat → Wrd → IO Float
+| 0, w => throw <| IO.userError s!"proof cache recursion exhausted at {w}"
+| fuel + 1, w => do
+  let cache ← proofCache.get
+  match cache.get? w with
+  | none => panic! s!"no cached node for {w}"
+  | some node =>
+    match node with
+    | empty => return 0.0
+    | gen _ => return 1.0
+    | triang w₁ w₂ => return (← derivedLengthWithFuel fuel w₁) + (← derivedLengthWithFuel fuel w₂)
+    | conj _ w => derivedLengthWithFuel fuel w
+    | power n w => return (← derivedLengthWithFuel fuel (w^n)) / n.toFloat
+
+/-- Recompute the derived length from cached proof nodes, panicking if a node is absent. -/
+def derivedLength (w : Wrd) : IO Float := do
+  let cache ← proofCache.get
+  derivedLengthWithFuel (cache.size + 1) w
+
+/-- Recompute the derived length from cached proof nodes, panicking if a node is absent. -/
+private def derivedLength! (w : Wrd) : IO Float := do
+  derivedLength w
+
+/-- Recompute a derived length proof with a bounded traversal fuel. -/
+private def derivedProofWithFuel : Nat → Wrd → IO (Float × (List ProofNode))
+| 0, w => throw <| IO.userError s!"proof cache recursion exhausted at {w}"
+| fuel + 1, w => do
+  let cache ← proofCache.get
+  match cache.get? w with
+  | none => panic! s!"no cached node for {w}"
+  | some node =>
+    match node with
+    | empty => return (0.0, [empty])
+    | gen l => return (1.0, [gen l])
+    | triang w₁ w₂ =>
+      let (l₁, ns₁) ← derivedProofWithFuel fuel w₁
+      let (l₂, ns₂) ← derivedProofWithFuel fuel w₂
+      return (l₁ + l₂, ns₁ ++ ns₂ ++ [triang w₁ w₂])
+    | conj l w =>
+      let (l₀, ns) ← derivedProofWithFuel fuel w
+      return (l₀, ns ++ [conj l w])
+    | power n w =>
+      let (l₀, ns) ← derivedProofWithFuel fuel (w^n)
+      return (l₀ / n.toFloat, ns ++ [power n w])
+
+/-- Recompute the derived length together with the list of proof nodes used. -/
+def derivedProof (w : Wrd) : IO (Float × (List ProofNode)) := do
+  let cache ← proofCache.get
+  derivedProofWithFuel (cache.size + 1) w
+
+/-- Recompute the derived length together with the list of proof nodes used. -/
+private def derivedProof! (w : Wrd) : IO (Float × (List ProofNode)) := do
+  derivedProof w
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/Polymath.lean b/LeanPool/Polylean/Polymath.lean
new file mode 100644
index 0000000000..2c497a990f
--- /dev/null
+++ b/LeanPool/Polylean/Polymath.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.ConjInvLength.Length
+import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
+import LeanPool.Polylean.ConjInvLength.MemoLength
+import LeanPool.Polylean.ConjInvLength.ProvedBound
+
+/-!
+# Demonstration executable for Polylean length computations
+-/
+
+namespace LeanPool.Polylean
+
+open Letter
+
+/-- Demonstration executable for the conjugacy-invariant length computations. -/
+def polymathMain : IO Unit := do
+  for k in [1, 2, 6] do
+    let w := #[α, β, α!, β!]^k ++ #[α]
+    IO.println s!"computing length via powers of {w}"
+    for n in [1:21] do
+      let l ← powerLength w n
+      IO.println s!"length of {w} from power {n}: {l}"
+  let w := #[α, β, α!, β!]
+  IO.println s!"computing length via powers of the commutator {w}"
+  for n in [1:21] do
+    let l ← powerLength w n
+    IO.println s!"length of {w} from power {n}: {l}"
+  let l ← lengthNodes w
+  IO.println s!"length of {w}: {l}"
+  IO.println s!"derived length: {(← derivedLength w)}"
+  let (_, ns) ← derivedProof w
+  let ns := ns.eraseDups
+  let mut j := 0
+  for node in ns do
+    j := j + 1
+    let w := node.top
+    let l ← lengthNodes w
+    IO.println s!"Lemma {j}: l({w}) ≤ {l}"
+    IO.println s!"Proof: apply {node}"
+    for w in node.base do
+      let l ← lengthNodes w
+      IO.println s!"  using l({w}) ≤ {l}"
+    IO.println ""
+
+end LeanPool.Polylean
diff --git a/LeanPool/Polylean/UnitConjecture/Tactics.lean b/LeanPool/Polylean/UnitConjecture/Tactics.lean
index c8f19fc7ad..30691c2092 100644
--- a/LeanPool/Polylean/UnitConjecture/Tactics.lean
+++ b/LeanPool/Polylean/UnitConjecture/Tactics.lean
@@ -5,6 +5,7 @@ Authors: Siddhartha Gadgil, Anand Rao
 -/
 
 import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets
+import LeanPool.Polylean.UnitConjecture.Tactics.ReduceGoal
 
 /-!
 # Unit Conjecture tactics
diff --git a/LeanPool/Polylean/UnitConjecture/Tactics/ReduceGoal.lean b/LeanPool/Polylean/UnitConjecture/Tactics/ReduceGoal.lean
new file mode 100644
index 0000000000..bc8bd1c164
--- /dev/null
+++ b/LeanPool/Polylean/UnitConjecture/Tactics/ReduceGoal.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import Lean
+
+open Lean Meta Elab Tactic Term
+
+namespace LeanPool.Polylean
+
+/-- A tactic to reduce the main goal, up to definitional equality. -/
+private def reduceGoal (transparency : TransparencyMode) : TacticM Unit := do
+  let goal ← getMainGoal
+  let reducedGoalType ← withTransparency transparency <|
+    reduce (skipTypes := false) (skipProofs := false) (← getMainTarget)
+  let newGoal ← mkFreshExprMVar reducedGoalType
+  goal.assign newGoal
+  replaceMainGoal [newGoal.mvarId!]
+
+/--
+`reduce_goal transparency` replaces the main goal by its reduced form using the
+chosen transparency mode.
+-/
+elab "reduce_goal" tpc:ident : tactic => do
+  let transparency : TransparencyMode :=
+    match tpc.getId with
+      |    `all    => .all
+      |  `default  => .default
+      | `reducible => .reducible
+      | `instances => .instances
+      |     _      => panic! "Unknown transparency mode"
+  reduceGoal transparency
+
+private abbrev reduceGoalAll := reduceGoal .all
+private abbrev reduceGoalDefault := reduceGoal .default
+private abbrev reduceGoalReducible := reduceGoal .reducible
+private abbrev reduceGoalInstances := reduceGoal .instances
+
+end LeanPool.Polylean