diff --git a/leanblueprint/Packages/blueprint.py b/leanblueprint/Packages/blueprint.py
index dc83348..77d2f17 100644
--- a/leanblueprint/Packages/blueprint.py
+++ b/leanblueprint/Packages/blueprint.py
@@ -11,6 +11,9 @@
 
 You can also add options that will be passed to the dependency graph package.
 """
+
+import json
+import re
 import string
 from pathlib import Path
 
@@ -23,52 +26,294 @@
 log = getLogger()
 
 PKG_DIR = Path(__file__).parent
-STATIC_DIR = Path(__file__).parent.parent/'static'
+STATIC_DIR = Path(__file__).parent.parent / "static"
+
+
+def rewrite_lean_links(html_str: str, document) -> str:
+    """Jinja2 filter to rewrite doc-gen links at render time.
+
+    - Links to declarations in the blueprint → blueprint URL (using node.url)
+    - Links not in blueprint → project dochome
+    """
+    lean_to_node = document.userdata.get("lean_to_blueprint_node", {})
+    project_dochome = document.userdata.get(
+        "project_dochome_for_links",
+        "https://leanprover-community.github.io/mathlib4_docs",
+    )
+    project_dochome = project_dochome.rstrip("/")
+
+    def replace_link(match):
+        href = match.group(1)
+        link_text = match.group(2)
+
+        # Extract the Lean declaration name from the href
+        hash_match = re.search(r'#([^"]+)', href)
+        if hash_match:
+            lean_name = hash_match.group(1)
+
+            # Check if in blueprint
+            if lean_name in lean_to_node:
+                node = lean_to_node[lean_name]
+                # At render time, node.url should be available
+                try:
+                    node_url = node.url
+                    if node_url:
+                        return f'<a href="{node_url}" class="blueprint-link" title="View in blueprint">{link_text}</a>'
+                except Exception:
+                    pass
+
+        # Not in blueprint - rewrite to dochome
+        if href.startswith("./"):
+            new_href = project_dochome + href[1:]
+        elif href.startswith("../"):
+            path = href
+            while path.startswith("../"):
+                path = path[3:]
+            new_href = f"{project_dochome}/{path}"
+        else:
+            new_href = href
+
+        return f'<a href="{new_href}" title="View in docs">{link_text}</a>'
+
+    # Match <a href="...">...</a> patterns
+    return re.sub(
+        r'<a[^>]*href="([^"]*)"[^>]*>(.*?)</a>', replace_link, html_str, flags=re.DOTALL
+    )
+
+
+def load_docgen_declarations(document) -> dict:
+    """Load declaration data from doc-gen4 declaration-data.bmp."""
+    search_paths = [
+        document.userdata.get("docgen_declarations_path"),
+        "../docbuild/.lake/build/doc/declarations/declaration-data.bmp",
+        "../../docbuild/.lake/build/doc/declarations/declaration-data.bmp",
+    ]
+    working_dir = Path(document.userdata.get("working-dir", "."))
+
+    for rel_path in search_paths:
+        if rel_path is None:
+            continue
+        full_path = working_dir / rel_path
+        if full_path.exists():
+            try:
+                data = json.loads(full_path.read_text())
+                return data.get("declarations", {})
+            except Exception as e:
+                log.warning(f"Failed to parse {full_path}: {e}")
+    return {}
+
+
+def parse_docgen_statement(html_path: Path, decl_name: str) -> dict:
+    """Parse the Lean statement, equation, and structure fields from a doc-gen HTML file.
+
+    Returns a dict with keys:
+        - statement_text: plain text of the declaration header
+        - equation_text: plain text of equations (for defs)
+        - statement_html: HTML of the declaration header
+        - equation_html: HTML of equations (for defs)
+        - fields_html: HTML of structure fields (for structures)
+        - fields_text: plain text of structure fields (for structures)
+
+    Links are kept as-is - they will be rewritten at render time by a Jinja2 filter.
+    """
+    result = {
+        "statement_text": "",
+        "equation_text": "",
+        "statement_html": "",
+        "equation_html": "",
+        "fields_html": "",
+        "fields_text": "",
+    }
+
+    if not html_path.exists():
+        return result
+
+    try:
+        content = html_path.read_text()
+
+        # Find the specific declaration block
+        start_pattern = rf'<div class="decl" id="{re.escape(decl_name)}">'
+        start_match = re.search(start_pattern, content)
+        if not start_match:
+            return result
+
+        start_pos = start_match.end()
+
+        # Find where this declaration ends - look for next declaration or mod_doc
+        end_pattern = r'<div class="(?:decl|mod_doc)"'
+        end_match = re.search(end_pattern, content[start_pos:])
+        if end_match:
+            decl_html = content[start_pos : start_pos + end_match.start()]
+        else:
+            decl_html = content[start_pos:]
+
+        # Extract the raw decl_header HTML for styled display
+        # Keep links as-is - they'll be rewritten at render time
+        # Note: decl_header may contain nested divs (e.g., decl_type), so we need to match balanced tags
+        header_start_pattern = r'<div class="decl_header">'
+        header_start_match = re.search(header_start_pattern, decl_html)
+        if header_start_match:
+            # Find the matching closing </div> by counting nested divs
+            start_idx = header_start_match.end()
+            depth = 1
+            pos = start_idx
+            while depth > 0 and pos < len(decl_html):
+                next_open = decl_html.find("<div", pos)
+                next_close = decl_html.find("</div>", pos)
+                if next_close == -1:
+                    break
+                if next_open != -1 and next_open < next_close:
+                    depth += 1
+                    pos = next_open + 4
+                else:
+                    depth -= 1
+                    if depth == 0:
+                        raw_header = decl_html[start_idx:next_close]
+                        result["statement_html"] = (
+                            f'<div class="decl_header">{raw_header}</div>'
+                        )
+                        # Also extract plain text version as fallback
+                        header_text = raw_header
+                        header_text = re.sub(
+                            r'<span class="decl_kind">.*?</span>', "", header_text
+                        )
+                        header_text = re.sub(
+                            r'<span class="decl_name">.*?</span>', "", header_text
+                        )
+                        header_text = re.sub(
+                            r'<a[^>]*class="break_within"[^>]*>.*?</a>', "", header_text
+                        )
+                        header_text = re.sub(r"<a[^>]*>", "", header_text)
+                        header_text = re.sub(r"</a>", "", header_text)
+                        header_text = re.sub(r"<span[^>]*>", "", header_text)
+                        header_text = re.sub(r"</span>", "", header_text)
+                        header_text = re.sub(
+                            r'<div class="decl_type">', " : ", header_text
+                        )
+                        header_text = re.sub(r"</div>", "", header_text)
+                        header_text = re.sub(r"<[^>]+>", "", header_text)
+                        header_text = re.sub(r"\s+", " ", header_text).strip()
+                        header_text = re.sub(r"^[\s.]+", "", header_text)
+                        header_text = re.sub(r":\s*:", ":", header_text)
+                        result["statement_text"] = header_text
+                    pos = next_close + 6
+
+        # Extract equation from Equations details block - only within THIS declaration
+        eq_pattern = r'<details><summary>Equations</summary><ul class="equations">(.*?)</ul></details>'
+        eq_match = re.search(eq_pattern, decl_html, re.DOTALL)
+        if eq_match:
+            eq_html = eq_match.group(1)
+
+            # Keep links as-is for render-time rewriting
+            result["equation_html"] = (
+                f'<ul class="equations lean-equations">{eq_html}</ul>'
+            )
+
+            # Also create plain text version
+            eq_html_clean = re.sub(r"<a[^>]*>", "", eq_html)
+            eq_html_clean = re.sub(r"</a>", "", eq_html_clean)
+            eq_html_clean = re.sub(r"<span[^>]*>", "", eq_html_clean)
+            eq_html_clean = re.sub(r"</span>", "", eq_html_clean)
+            eq_html_clean = re.sub(r'<li class="equation">', "", eq_html_clean)
+            eq_html_clean = re.sub(r"</li>", "\n", eq_html_clean)
+            eq_html_clean = re.sub(r"<[^>]+>", "", eq_html_clean)
+            eq_html_clean = re.sub(r"\s+", " ", eq_html_clean).strip()
+            result["equation_text"] = eq_html_clean
+
+        # Extract structure fields from structure_fields ul - only within THIS declaration
+        fields_pattern = r'<ul class="structure_fields"[^>]*>(.*?)</ul>'
+        fields_match = re.search(fields_pattern, decl_html, re.DOTALL)
+        if fields_match:
+            fields_html = fields_match.group(1)
+
+            # Keep links as-is for render-time rewriting
+            result["fields_html"] = (
+                f'<ul class="structure_fields lean-structure-fields">{fields_html}</ul>'
+            )
+
+            # Also create plain text version
+            fields_text_parts = []
+            field_pattern = r'<li[^>]*class="structure_field"[^>]*>.*?<div class="structure_field_info">(.*?)</div>'
+            for field_match in re.finditer(field_pattern, fields_html, re.DOTALL):
+                field_info = field_match.group(1)
+                # Strip HTML tags for plain text
+                field_text = re.sub(r"<[^>]+>", "", field_info)
+                field_text = re.sub(r"\s+", " ", field_text).strip()
+                if field_text:
+                    fields_text_parts.append(field_text)
+            result["fields_text"] = "\n".join(fields_text_parts)
+
+        return result
+    except Exception as e:
+        log.warning(f"Failed to parse statement from {html_path}: {e}")
+    return result
+
+
+def get_docgen_base_path(document) -> Path:
+    """Get the base path for doc-gen HTML files."""
+    search_paths = [
+        "../docbuild/.lake/build/doc",
+        "../../docbuild/.lake/build/doc",
+    ]
+    working_dir = Path(document.userdata.get("working-dir", "."))
+
+    for rel_path in search_paths:
+        full_path = working_dir / rel_path
+        if full_path.exists():
+            return full_path
+    return None
 
 
 class home(Command):
     r"""\home{url}"""
-    args = 'url:url'
+
+    args = "url:url"
 
     def invoke(self, tex):
         Command.invoke(self, tex)
-        self.ownerDocument.userdata['project_home'] = self.attributes['url']
+        self.ownerDocument.userdata["project_home"] = self.attributes["url"]
         return []
 
 
 class github(Command):
     r"""\github{url}"""
-    args = 'url:url'
+
+    args = "url:url"
 
     def invoke(self, tex):
         Command.invoke(self, tex)
-        self.ownerDocument.userdata['project_github'] = self.attributes['url'].textContent.rstrip(
-            '/')
+        self.ownerDocument.userdata["project_github"] = self.attributes[
+            "url"
+        ].textContent.rstrip("/")
         return []
 
 
 class dochome(Command):
     r"""\dochome{url}"""
-    args = 'url:url'
+
+    args = "url:url"
 
     def invoke(self, tex):
         Command.invoke(self, tex)
-        self.ownerDocument.userdata['project_dochome'] = self.attributes['url'].textContent
+        self.ownerDocument.userdata["project_dochome"] = self.attributes[
+            "url"
+        ].textContent
         return []
 
 
 class graphcolor(Command):
     r"""\graphcolor{node_type}{color}{color_descr}"""
-    args = 'node_type:str color:str color_descr:str'
+
+    args = "node_type:str color:str color_descr:str"
 
     def digest(self, tokens):
         Command.digest(self, tokens)
         attrs = self.attributes
-        colors = self.ownerDocument.userdata['dep_graph']['colors']
-        node_type = attrs['node_type']
+        colors = self.ownerDocument.userdata["dep_graph"]["colors"]
+        node_type = attrs["node_type"]
         if node_type not in colors:
-            log.warning(f'Unknown node type {node_type}')
-        colors[node_type] = (attrs['color'].strip(), attrs['color_descr'].strip())
+            log.warning(f"Unknown node type {node_type}")
+        colors[node_type] = (attrs["color"].strip(), attrs["color_descr"].strip())
 
 
 class leanok(Command):
@@ -76,7 +321,23 @@ class leanok(Command):
 
     def digest(self, tokens):
         Command.digest(self, tokens)
-        self.parentNode.userdata['leanok'] = True
+        self.parentNode.userdata["leanok"] = True
+
+
+class leantarget(Command):
+    r"""\leantarget - marks this theorem/definition as a main target result"""
+
+    def digest(self, tokens):
+        Command.digest(self, tokens)
+        self.parentNode.userdata["leantarget"] = True
+
+
+class leanhelper(Command):
+    r"""\leanhelper - marks this theorem/lemma as a helper/auxiliary result"""
+
+    def digest(self, tokens):
+        Command.digest(self, tokens)
+        self.parentNode.userdata["leanhelper"] = True
 
 
 class notready(Command):
@@ -84,7 +345,7 @@ class notready(Command):
 
     def digest(self, tokens):
         Command.digest(self, tokens)
-        self.parentNode.userdata['notready'] = True
+        self.parentNode.userdata["notready"] = True
 
 
 class mathlibok(Command):
@@ -92,58 +353,109 @@ class mathlibok(Command):
 
     def digest(self, tokens):
         Command.digest(self, tokens)
-        self.parentNode.userdata['leanok'] = True
-        self.parentNode.userdata['mathlibok'] = True
+        self.parentNode.userdata["leanok"] = True
+        self.parentNode.userdata["mathlibok"] = True
 
 
 class lean(Command):
-    r"""\lean{decl list} """
-    args = 'decls:list:nox'
+    r"""\lean{decl list}"""
+
+    args = "decls:list:nox"
 
     def digest(self, tokens):
         Command.digest(self, tokens)
-        decls = [dec.strip() for dec in self.attributes['decls']]
-        self.parentNode.setUserData('leandecls', decls)
-        all_decls = self.ownerDocument.userdata.setdefault('lean_decls', [])
+        decls = [dec.strip() for dec in self.attributes["decls"]]
+        self.parentNode.setUserData("leandecls", decls)
+        all_decls = self.ownerDocument.userdata.setdefault("lean_decls", [])
         all_decls.extend(decls)
 
 
 class discussion(Command):
-    r"""\discussion{issue_number} """
-    args = 'issue:str'
+    r"""\discussion{issue_number}"""
+
+    args = "issue:str"
 
     def digest(self, tokens):
         Command.digest(self, tokens)
         self.parentNode.setUserData(
-            'issue', self.attributes['issue'].lstrip('#').strip())
+            "issue", self.attributes["issue"].lstrip("#").strip()
+        )
 
 
-CHECKMARK_TPL = Template("""
+CHECKMARK_TPL = Template(
+    """
     {% if obj.userdata.leanok and ('proved_by' not in obj.userdata or obj.userdata.proved_by.userdata.leanok ) %}
     ✓
     {% endif %}
-""")
-
-LEAN_DECLS_TPL = Template("""
-    {% if obj.userdata.leandecls %}
-    <button class="modal lean">L∃∀N</button>
-    {% call modal('Lean declarations') %}
-        <ul class="uses">
-          {% for lean, url in obj.userdata.lean_urls %}
-          <li><a href="{{ url }}" class="lean_decl">{{ lean }}</a></li>
-          {% endfor %}
-        </ul>
-    {% endcall %}
+"""
+)
+
+LEAN_SIDE_PANEL_TPL = Template(
+    """
+{% if obj.userdata.lean_entries %}
+{% set has_content = [] %}
+{% for entry in obj.userdata.lean_entries %}
+{% if entry.statement_html or entry.statement %}{% if has_content.append(1) %}{% endif %}{% endif %}
+{% endfor %}
+{% if has_content %}
+<div class="lean-side-panel{% if obj.userdata.leantarget %} lean-target{% endif %}{% if obj.userdata.leanhelper %} lean-helper{% endif %}">
+  {% for entry in obj.userdata.lean_entries %}
+  {% if entry.statement_html or entry.statement %}
+  <div class="lean-entry">
+    {% if entry.statement_html %}
+    <div class="lean-decl-box">
+      <div class="lean-decl-links">
+        <a href="{{ entry.doc_url }}" class="lean-doc-link" title="View documentation">docs</a>
+        {% if entry.github_url %}<a href="{{ entry.github_url }}" class="lean-src-link" title="View source">source</a>{% endif %}
+      </div>
+      {{ doc.userdata.rewrite_lean_links_fn(entry.statement_html, doc) | safe }}
+      {% if entry.fields_html %}
+      {{ doc.userdata.rewrite_lean_links_fn(entry.fields_html, doc) | safe }}
+      {% elif entry.fields_text %}
+      <pre class="lean-fields">{{ entry.fields_text }}</pre>
+      {% endif %}
+      {% if entry.equation_html %}
+      {{ doc.userdata.rewrite_lean_links_fn(entry.equation_html, doc) | safe }}
+      {% elif entry.equation %}
+      <pre class="lean-equation">{{ entry.equation }}</pre>
+      {% endif %}
+    </div>
+    {% elif entry.statement %}
+    <div class="lean-entry-header">
+      <a href="{{ entry.doc_url }}" class="lean-decl-link" title="View documentation">{{ entry.short_name }}</a>
+      {% if entry.github_url %}<a href="{{ entry.github_url }}" class="lean-src" title="View source">📄</a>{% endif %}
+    </div>
+    <pre class="lean-statement">{{ entry.statement }}</pre>
+    {% if entry.fields_html %}
+    {{ doc.userdata.rewrite_lean_links_fn(entry.fields_html, doc) | safe }}
+    {% elif entry.fields_text %}
+    <pre class="lean-fields">{{ entry.fields_text }}</pre>
+    {% endif %}
+    {% if entry.equation_html %}
+    {{ doc.userdata.rewrite_lean_links_fn(entry.equation_html, doc) | safe }}
+    {% elif entry.equation %}
+    <pre class="lean-equation">{{ entry.equation }}</pre>
+    {% endif %}
     {% endif %}
-""")
+  </div>
+  {% endif %}
+  {% endfor %}
+</div>
+{% endif %}
+{% endif %}
+"""
+)
 
-GITHUB_ISSUE_TPL = Template("""
+GITHUB_ISSUE_TPL = Template(
+    """
     {% if obj.userdata.issue %}
     <a class="github_link" href="{{ obj.ownerDocument.userdata.project_github }}/issues/{{ obj.userdata.issue }}">Discussion</a>
     {% endif %}
-""")
+"""
+)
 
-LEAN_LINKS_TPL = Template("""
+LEAN_LINKS_TPL = Template(
+    """
   {% if thm.userdata['lean_urls'] -%}
     {%- if thm.userdata['lean_urls']|length > 1 -%}
   <div class="tooltip">
@@ -158,13 +470,16 @@ def digest(self, tokens):
     <a class="lean_link lean_decl" href="{{ thm.userdata['lean_urls'][0][1] }}">Lean</a>
     {%- endif -%}
     {%- endif -%}
-""")
+"""
+)
 
-GITHUB_LINK_TPL = Template("""
+GITHUB_LINK_TPL = Template(
+    """
   {% if thm.userdata['issue'] -%}
   <a class="issue_link" href="{{ document.userdata['project_github'] }}/issues/{{ thm.userdata['issue'] }}">Discussion</a>
   {%- endif -%}
-""")
+"""
+)
 
 
 def ProcessOptions(options, document):
@@ -175,23 +490,26 @@ def ProcessOptions(options, document):
     # This is a bit hacky but needed for backward compatibility with
     # project who used the blueprint package before the depgraph one was
     # split.
-    plugins = document.config['general'].data['plugins'].value
-    if 'plastexdepgraph' not in plugins:
-        plugins.append('plastexdepgraph')
+    plugins = document.config["general"].data["plugins"].value
+    if "plastexdepgraph" not in plugins:
+        plugins.append("plastexdepgraph")
     # And now load the package.
-    document.context.loadPythonPackage(document, 'depgraph', options)
-    if 'showmore' in options:
-        if 'plastexshowmore' not in plugins:
-            plugins.append('plastexshowmore')
+    document.context.loadPythonPackage(document, "depgraph", options)
+    if "showmore" in options:
+        if "plastexshowmore" not in plugins:
+            plugins.append("plastexshowmore")
         # And now load the package.
-        document.context.loadPythonPackage(document, 'showmore', {})
+        document.context.loadPythonPackage(document, "showmore", {})
 
-    templatedir = PackageTemplateDir(path=PKG_DIR/'renderer_templates')
+    templatedir = PackageTemplateDir(path=PKG_DIR / "renderer_templates")
     document.addPackageResource(templatedir)
 
-    jobname = document.userdata['jobname']
-    outdir = document.config['files']['directory']
-    outdir = string.Template(outdir).substitute({'jobname': jobname})
+    # Register the link rewriting function for use in templates
+    document.userdata["rewrite_lean_links_fn"] = rewrite_lean_links
+
+    jobname = document.userdata["jobname"]
+    outdir = document.config["files"]["directory"]
+    outdir = string.Template(outdir).substitute({"jobname": jobname})
 
     def make_lean_data() -> None:
         """
@@ -199,125 +517,214 @@ def make_lean_data() -> None:
         Also create the file lean_decls of all Lean names referred to in the blueprint.
         """
 
-        project_dochome = document.userdata.get('project_dochome',
-                                                'https://leanprover-community.github.io/mathlib4_docs')
+        project_dochome = document.userdata.get(
+            "project_dochome", "https://leanprover-community.github.io/mathlib4_docs"
+        )
+        project_github = document.userdata.get("project_github", "")
+
+        # Load doc-gen data
+        docgen_decls = load_docgen_declarations(document)
+        docgen_base = get_docgen_base_path(document)
+
+        # Build mapping from Lean names to blueprint nodes
+        # URLs will be resolved at render time when node.url is available
+        lean_to_node = {}
+        for graph in document.userdata["dep_graph"]["graphs"].values():
+            for node in graph.nodes:
+                leandecls = node.userdata.get("leandecls", [])
+                for leandecl in leandecls:
+                    lean_to_node[leandecl] = node
+
+        # Store the mapping and dochome in document for access during rendering
+        document.userdata["lean_to_blueprint_node"] = lean_to_node
+        document.userdata["project_dochome_for_links"] = project_dochome
 
-        for graph in document.userdata['dep_graph']['graphs'].values():
+        for graph in document.userdata["dep_graph"]["graphs"].values():
             nodes = graph.nodes
             for node in nodes:
-                leandecls = node.userdata.get('leandecls', [])
+                leandecls = node.userdata.get("leandecls", [])
                 lean_urls = []
+                lean_entries = []
                 for leandecl in leandecls:
                     lean_urls.append(
-                        (leandecl,
-                         f'{project_dochome}/find/#doc/{leandecl}'))
-
-                node.userdata['lean_urls'] = lean_urls
-
-                used = node.userdata.get('uses', [])
-                node.userdata['can_state'] = all(thm.userdata.get('leanok')
-                                                 for thm in used) and not node.userdata.get('notready', False)
-                proof = node.userdata.get('proved_by')
+                        (leandecl, f"{project_dochome}/find/#doc/{leandecl}")
+                    )
+
+                    # Build lean_entries with docgen data
+                    decl_info = docgen_decls.get(leandecl, {})
+                    doc_link = decl_info.get("docLink", "").lstrip("./")
+
+                    # Parse statement and equation from doc-gen HTML if available
+                    # Links are kept as relative - will be rewritten at render time
+                    statement = ""
+                    equation = ""
+                    statement_html = ""
+                    equation_html = ""
+                    fields_html = ""
+                    fields_text = ""
+                    if docgen_base and doc_link:
+                        html_file = doc_link.split("#")[0]
+                        html_path = docgen_base / html_file
+                        parsed = parse_docgen_statement(html_path, leandecl)
+                        statement = parsed["statement_text"]
+                        equation = parsed["equation_text"]
+                        statement_html = parsed["statement_html"]
+                        equation_html = parsed["equation_html"]
+                        fields_html = parsed["fields_html"]
+                        fields_text = parsed["fields_text"]
+
+                    # Get short name (last component)
+                    short_name = leandecl.split(".")[-1]
+
+                    entry = {
+                        "name": leandecl,
+                        "short_name": short_name,
+                        "kind": decl_info.get("kind", ""),
+                        "doc_url": f"{project_dochome}/{doc_link}",
+                        "statement": statement,
+                        "equation": equation,
+                        "statement_html": statement_html,
+                        "equation_html": equation_html,
+                        "fields_html": fields_html,
+                        "fields_text": fields_text,
+                    }
+                    # GitHub URL from docLink path
+                    if project_github and doc_link:
+                        module_path = doc_link.split("#")[0].replace(".html", ".lean")
+                        entry["github_url"] = (
+                            f"{project_github}/blob/main/{module_path}"
+                        )
+                    lean_entries.append(entry)
+
+                node.userdata["lean_urls"] = lean_urls
+                node.userdata["lean_entries"] = lean_entries
+
+                used = node.userdata.get("uses", [])
+                node.userdata["can_state"] = all(
+                    thm.userdata.get("leanok") for thm in used
+                ) and not node.userdata.get("notready", False)
+                proof = node.userdata.get("proved_by")
                 if proof:
-                    used.extend(proof.userdata.get('uses', []))
-                    node.userdata['can_prove'] = all(thm.userdata.get('leanok')
-                                                     for thm in used)
-                    node.userdata['proved'] = proof.userdata.get(
-                        'leanok', False)
+                    used.extend(proof.userdata.get("uses", []))
+                    node.userdata["can_prove"] = all(
+                        thm.userdata.get("leanok") for thm in used
+                    )
+                    node.userdata["proved"] = proof.userdata.get("leanok", False)
                 else:
-                    node.userdata['can_prove'] = False
-                    node.userdata['proved'] = False
+                    node.userdata["can_prove"] = False
+                    node.userdata["proved"] = False
 
             for node in nodes:
-                node.userdata['fully_proved'] = all(n.userdata.get('proved', False) or item_kind(
-                    n) == 'definition' for n in graph.ancestors(node).union({node}))
+                node.userdata["fully_proved"] = all(
+                    n.userdata.get("proved", False) or item_kind(n) == "definition"
+                    for n in graph.ancestors(node).union({node})
+                )
 
-        lean_decls_path = Path(document.userdata['working-dir']).parent/"lean_decls"
+        lean_decls_path = Path(document.userdata["working-dir"]).parent / "lean_decls"
         lean_decls_path.write_text("\n".join(document.userdata.get("lean_decls", [])))
 
     document.addPostParseCallbacks(150, make_lean_data)
 
-    document.addPackageResource([PackageCss(path=STATIC_DIR/'blueprint.css')])
-
-    colors = document.userdata['dep_graph']['colors'] = {
-        'mathlib': ('darkgreen', 'Dark green'),
-        'stated': ('green', 'Green'),
-        'can_state': ('blue', 'Blue'),
-        'not_ready': ('#FFAA33', 'Orange'),
-        'proved': ('#9CEC8B', 'Green'),
-        'can_prove': ('#A3D6FF', 'Blue'),
-        'defined': ('#B0ECA3', 'Light green'),
-        'fully_proved': ('#1CAC78', 'Dark green')
+    document.addPackageResource([PackageCss(path=STATIC_DIR / "blueprint.css")])
+
+    colors = document.userdata["dep_graph"]["colors"] = {
+        "mathlib": ("darkgreen", "Dark green"),
+        "stated": ("green", "Green"),
+        "can_state": ("blue", "Blue"),
+        "not_ready": ("#FFAA33", "Orange"),
+        "proved": ("#9CEC8B", "Green"),
+        "can_prove": ("#A3D6FF", "Blue"),
+        "defined": ("#B0ECA3", "Light green"),
+        "fully_proved": ("#1CAC78", "Dark green"),
     }
 
     def colorizer(node) -> str:
         data = node.userdata
 
-        color = ''
-        if data.get('mathlibok'):
-            color = colors['mathlib'][0]
-        elif data.get('leanok'):
-            color = colors['stated'][0]
-        elif data.get('can_state'):
-            color = colors['can_state'][0]
-        elif data.get('notready'):
-            color = colors['not_ready'][0]
+        color = ""
+        if data.get("mathlibok"):
+            color = colors["mathlib"][0]
+        elif data.get("leanok"):
+            color = colors["stated"][0]
+        elif data.get("can_state"):
+            color = colors["can_state"][0]
+        elif data.get("notready"):
+            color = colors["not_ready"][0]
         return color
 
     def fillcolorizer(node) -> str:
         data = node.userdata
-        stated = data.get('leanok')
-        can_state = data.get('can_state')
-        can_prove = data.get('can_prove')
-        proved = data.get('proved')
-        fully_proved = data.get('fully_proved')
+        stated = data.get("leanok")
+        can_state = data.get("can_state")
+        can_prove = data.get("can_prove")
+        proved = data.get("proved")
+        fully_proved = data.get("fully_proved")
 
-        fillcolor = ''
+        fillcolor = ""
         if proved:
-            fillcolor = colors['proved'][0]
+            fillcolor = colors["proved"][0]
         elif can_prove and (can_state or stated):
-            fillcolor = colors['can_prove'][0]
-        if item_kind(node) == 'definition':
+            fillcolor = colors["can_prove"][0]
+        if item_kind(node) == "definition":
             if stated:
-                fillcolor = colors['defined'][0]
+                fillcolor = colors["defined"][0]
             elif can_state:
-                fillcolor = colors['can_prove'][0]
+                fillcolor = colors["can_prove"][0]
         elif fully_proved:
-            fillcolor = colors['fully_proved'][0]
+            fillcolor = colors["fully_proved"][0]
         return fillcolor
 
-    document.userdata['dep_graph']['colorizer'] = colorizer
-    document.userdata['dep_graph']['fillcolorizer'] = fillcolorizer
+    document.userdata["dep_graph"]["colorizer"] = colorizer
+    document.userdata["dep_graph"]["fillcolorizer"] = fillcolorizer
 
     def make_legend() -> None:
         """
         Extend the dependency graph legend defined by the depgraph plugin
         by adding information specific to Lean blueprints. This is registered
-        as a post-parse callback to allow users to redefine colors and their 
+        as a post-parse callback to allow users to redefine colors and their
         descriptions.
         """
-        document.userdata['dep_graph']['legend'].extend([
-            (f"{document.userdata['dep_graph']['colors']['can_state'][1]} border",
-             "the <em>statement</em> of this result is ready to be formalized; all prerequisites are done"),
-            (f"{document.userdata['dep_graph']['colors']['not_ready'][1]} border",
-                "the <em>statement</em> of this result is not ready to be formalized; the blueprint needs more work"),
-            (f"{document.userdata['dep_graph']['colors']['can_state'][1]} background",
-                "the <em>proof</em> of this result is ready to be formalized; all prerequisites are done"),
-            (f"{document.userdata['dep_graph']['colors']['proved'][1]} border",
-                "the <em>statement</em> of this result is formalized"),
-            (f"{document.userdata['dep_graph']['colors']['proved'][1]} background",
-                "the <em>proof</em> of this result is formalized"),
-            (f"{document.userdata['dep_graph']['colors']['fully_proved'][1]} background", 
-                "the <em>proof</em> of this result and all its ancestors are formalized"),
-            (f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border",
-                "this is in Mathlib"),
-        ])
+        document.userdata["dep_graph"]["legend"].extend(
+            [
+                (
+                    f"{document.userdata['dep_graph']['colors']['can_state'][1]} border",
+                    "the <em>statement</em> of this result is ready to be formalized; all prerequisites are done",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['not_ready'][1]} border",
+                    "the <em>statement</em> of this result is not ready to be formalized; the blueprint needs more work",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['can_state'][1]} background",
+                    "the <em>proof</em> of this result is ready to be formalized; all prerequisites are done",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['proved'][1]} border",
+                    "the <em>statement</em> of this result is formalized",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['proved'][1]} background",
+                    "the <em>proof</em> of this result is formalized",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['fully_proved'][1]} background",
+                    "the <em>proof</em> of this result and all its ancestors are formalized",
+                ),
+                (
+                    f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border",
+                    "this is in Mathlib",
+                ),
+            ]
+        )
 
     document.addPostParseCallbacks(150, make_legend)
 
-    document.userdata.setdefault(
-        'thm_header_extras_tpl', []).extend([CHECKMARK_TPL])
-    document.userdata.setdefault('thm_header_hidden_extras_tpl', []).extend([LEAN_DECLS_TPL,
-                                                                             GITHUB_ISSUE_TPL])
-    document.userdata['dep_graph'].setdefault('extra_modal_links_tpl', []).extend([
-        LEAN_LINKS_TPL, GITHUB_LINK_TPL])
+    document.userdata.setdefault("thm_header_extras_tpl", []).extend([CHECKMARK_TPL])
+    document.userdata.setdefault("thm_header_hidden_extras_tpl", []).extend(
+        [GITHUB_ISSUE_TPL]
+    )
+    # Side panel template goes in a new hook for content that appears after the theorem
+    document.userdata.setdefault("thm_side_panel_tpl", []).extend([LEAN_SIDE_PANEL_TPL])
+    document.userdata["dep_graph"].setdefault("extra_modal_links_tpl", []).extend(
+        [LEAN_LINKS_TPL, GITHUB_LINK_TPL]
+    )
diff --git a/leanblueprint/Packages/renderer_templates/blueprint.jinja2s b/leanblueprint/Packages/renderer_templates/blueprint.jinja2s
index 782aeda..a6141a0 100644
--- a/leanblueprint/Packages/renderer_templates/blueprint.jinja2s
+++ b/leanblueprint/Packages/renderer_templates/blueprint.jinja2s
@@ -1,2 +1,57 @@
 name: leanok lean mathlibok notready discussion
 
+
+name: thmenv
+{% macro icon(icon, id='', class='') %}
+<svg  {% if id %}id="{{id}}" {% endif %}class="icon icon-{{ icon }} {{ class }}"><use xlink:href="symbol-defs.svg#icon-{{ icon }}"></use></svg>
+{% endmacro %}
+{% macro modal(title) %}
+    <div class="modal-container">
+      <div class="modal-content">
+        <header>
+          <h1>{{ title }}</h1>
+          <button class="closebtn">{{ icon('cross') }}</button>
+        </header>
+        {{ caller() }}
+      </div>
+    </div>
+{% endmacro %}
+<div class="{{ obj.thmName }}_thmwrapper {% if obj.style %}theorem-style-{{ obj.style }}{% endif %}" id="{{ obj.id }}">
+  <div class="{{ obj.thmName }}_thmmain">
+    <div class="{{ obj.thmName }}_thmheading">
+      <span class="{{ obj.thmName }}_thmcaption">
+      {{ obj.caption }}
+      </span>
+  	{% if obj.ref %}
+      <span class="{{obj.thmName}}_thmlabel">{{obj.ref}}</span>
+      {% endif %}
+      {% if obj.title %}
+      <span class="{{obj.thmName}}_thmtitle">{{ obj.title }}</span>
+      {% endif %}
+      {% if doc.userdata['thm_header_extras_tpl'] %}
+      <div class="thm_header_extras">
+      {% for tpl in doc.userdata['thm_header_extras_tpl'] %}
+      {% include tpl %}
+      {% endfor %}
+      </div>
+      {% endif %}
+      {% if doc.userdata['thm_header_hidden_extras_tpl'] %}
+      <div class="thm_header_hidden_extras">
+      {% for tpl in doc.userdata['thm_header_hidden_extras_tpl'] %}
+      {% include tpl %}
+      {% endfor %}
+      </div>
+      {% endif %}
+    </div>
+    <div class="{{ obj.thmName }}_thmcontent">
+    {{ obj }}
+    </div>
+  </div>
+  {% if doc.userdata['thm_side_panel_tpl'] %}
+  <div class="thm_side_panel">
+  {% for tpl in doc.userdata['thm_side_panel_tpl'] %}
+  {% include tpl %}
+  {% endfor %}
+  </div>
+  {% endif %}
+</div>
diff --git a/leanblueprint/jekyll_templates/_config.yml b/leanblueprint/jekyll_templates/_config.yml
index ddad425..be1f3f3 100644
--- a/leanblueprint/jekyll_templates/_config.yml
+++ b/leanblueprint/jekyll_templates/_config.yml
@@ -21,14 +21,14 @@
 title: {| web_title |}
 #email: your-email@example.com
 description: {| web_subtitle |}
-baseurl: "" # the subpath of your site, e.g. /blog
+baseurl: "/{| github_projectname |}" # the subpath of your site, e.g. /blog
 url: "{| home |}" # the base hostname & protocol for your site, e.g. http://example.com
 twitter_username:
 github_username: {| github_username |}
 repository: {| github_username |}/{| github_projectname |}
 
 # Build settings
-remote_theme: {| jekyll_theme |} 
+remote_theme: {| jekyll_theme |}
 plugins:
   - jekyll-remote-theme
   - jekyll-github-metadata
diff --git a/leanblueprint/static/blueprint.css b/leanblueprint/static/blueprint.css
index c7be366..cd51ed3 100644
--- a/leanblueprint/static/blueprint.css
+++ b/leanblueprint/static/blueprint.css
@@ -5,3 +5,491 @@ a.github_link {
   color: inherit;
 }
 
+/* Wider TOC sidebar */
+@media (min-width: 1024px) {
+  nav.toc {
+    max-width: 35ch !important;
+    min-width: 30ch !important;
+  }
+}
+
+/* ============================================
+   TWO-COLUMN LAYOUT: TeX Left, Lean Right
+   ============================================
+
+   Architecture: main-text is a 2-column CSS Grid.
+   - Column 1 (left): All regular content (paragraphs, proofs, etc.)
+   - Column 2 (right): Reserved for Lean panels
+   - Theorem wrappers: Span BOTH columns, with their own internal grid
+*/
+
+/* Fix scroll issue caused by theme-white.css overflow:hidden */
+body {
+  overflow: auto !important;
+  height: auto !important;
+}
+
+div.wrapper {
+  overflow: visible !important;
+  height: auto !important;
+}
+
+/* Override content wrapper constraints for wider layout */
+div.content-wrapper {
+  max-width: none !important;
+  width: 100% !important;
+}
+
+div.content {
+  max-width: none !important;
+  padding: 1rem 2rem !important;
+  overflow: auto !important;
+}
+
+/* Main content area: 2-column grid */
+div.main-text {
+  display: grid;
+  grid-template-columns: minmax(0, 1fr) minmax(0, 1fr);
+  gap: 0 2rem; /* no row gap, 2rem column gap */
+  grid-auto-flow: row; /* Ensure items flow in rows, not filling gaps */
+}
+
+/* Default: all children go into column 1 (left) only */
+div.main-text > * {
+  grid-column: 1 / 2;  /* Explicitly column 1 only, not spanning */
+  max-width: 100%;  /* Prevent overflow */
+}
+
+/* Headings stay in column 1 (left) only */
+div.main-text > h1,
+div.main-text > h2,
+div.main-text > h3 {
+  grid-column: 1 / 2;
+}
+
+/* Theorem wrappers span BOTH columns, then use their own internal grid */
+div.main-text > .definition_thmwrapper,
+div.main-text > .theorem_thmwrapper,
+div.main-text > .lemma_thmwrapper,
+div.main-text > .proposition_thmwrapper,
+div.main-text > .corollary_thmwrapper,
+div.main-text > .remark_thmwrapper,
+div.main-text > .example_thmwrapper {
+  grid-column: 1 / -1;
+  display: grid;
+  grid-template-columns: 1fr 1fr;
+  gap: 2rem;
+  margin-top: 1rem;
+  align-items: start;
+}
+
+/* The main theorem content takes the first (left) column */
+div.definition_thmmain,
+div.theorem_thmmain,
+div.lemma_thmmain,
+div.proposition_thmmain,
+div.corollary_thmmain,
+div.remark_thmmain,
+div.example_thmmain {
+  grid-column: 1;
+  grid-row: 1;  /* Force to first row */
+  min-width: 0;
+}
+
+/* The side panel takes the second (right) column */
+.thm_side_panel {
+  grid-column: 2;
+  grid-row: 1;  /* Force to first row, same as thmmain */
+  min-width: 0;
+}
+
+/* Hide side panel when it has no real content (only empty lean-entry divs) */
+/* Uses :has() to check for actual content */
+.thm_side_panel:not(:has(.lean-decl-box)):not(:has(.lean-statement)):not(:has(.lean-decl-link)) {
+  visibility: hidden;
+  min-height: 0;
+}
+
+/* Lean side panel styling */
+.lean-side-panel {
+  padding: 0;
+  font-size: 0.9em;
+  position: sticky;
+  top: 1rem;
+  max-height: calc(100vh - 2rem);
+  overflow-y: auto;
+}
+
+.lean-entry {
+  margin: 0.75rem 0;
+}
+
+.lean-entry:first-child {
+  margin-top: 0;
+}
+
+/* Doc-gen4 style declaration box */
+.lean-decl-box {
+  background: linear-gradient(135deg, #f8fafc 0%, #f1f5f9 100%);
+  border-left: 4px solid #22c55e;
+  border-radius: 0 6px 6px 0;
+  padding: 0.75rem;
+  overflow-x: auto;
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.85em;
+  line-height: 1.5;
+  position: relative;
+}
+
+/* Docs/source links in top-right corner */
+.lean-decl-links {
+  position: absolute;
+  top: 0.5rem;
+  right: 0.5rem;
+  display: flex;
+  gap: 0.75rem;
+  font-size: 0.8em;
+}
+
+.lean-doc-link,
+.lean-src-link {
+  color: #6b7280;
+  text-decoration: none;
+}
+
+.lean-doc-link:hover,
+.lean-src-link:hover {
+  color: #3b82f6;
+  text-decoration: underline;
+}
+
+/* Doc-gen4 CSS for declaration styling */
+.lean-decl-box .decl_header {
+  text-indent: -4ex;
+  padding-left: 4ex;
+  padding-right: 5rem;
+}
+
+.lean-decl-box .decl_kind {
+  font-weight: bold;
+  color: #374151;
+}
+
+.lean-decl-box .decl_name {
+  font-weight: bold;
+  color: #1e40af;
+  overflow-wrap: break-word;
+}
+
+.lean-decl-box .decl_name a {
+  color: #1e40af;
+  text-decoration: none;
+}
+
+.lean-decl-box .decl_name a:hover {
+  text-decoration: underline;
+}
+
+.lean-decl-box .decl_name::after {
+  content: "\A";
+  white-space: pre;
+}
+
+.lean-decl-box .decl_args {
+  font-weight: normal;
+}
+
+.lean-decl-box .impl_arg {
+  font-style: italic;
+  opacity: 0.5;
+  transition: opacity 300ms ease-in;
+}
+
+.lean-decl-box:hover .impl_arg {
+  opacity: 1;
+}
+
+.lean-decl-box .decl_type {
+  margin-top: 2px;
+  margin-left: 2ex;
+  color: #374151;
+}
+
+.lean-decl-box .fn {
+  color: #1e40af;
+}
+
+.lean-decl-box a {
+  color: #2563eb;
+  text-decoration: none;
+}
+
+.lean-decl-box a:hover {
+  text-decoration: underline;
+}
+
+/* Fallback header for entries without HTML */
+.lean-entry-header {
+  display: flex;
+  align-items: center;
+  gap: 0.5rem;
+  flex-wrap: wrap;
+  margin-bottom: 0.5rem;
+}
+
+.lean-decl-link {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.95em;
+  font-weight: bold;
+  color: #1e40af;
+  text-decoration: none;
+}
+
+.lean-decl-link:hover {
+  text-decoration: underline;
+  color: #3b82f6;
+}
+
+.lean-src {
+  margin-left: auto;
+  text-decoration: none;
+  font-size: 1.1em;
+  opacity: 0.7;
+}
+
+.lean-src:hover {
+  opacity: 1;
+}
+
+/* Fallback plain text statement */
+.lean-statement {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.8em;
+  line-height: 1.4;
+  color: #334155;
+  background: #f8fafc;
+  padding: 0.5rem;
+  margin: 0.5rem 0 0 0;
+  border-radius: 3px;
+  border-left: 4px solid #22c55e;
+  overflow-x: auto;
+  white-space: pre-wrap;
+  word-break: break-word;
+}
+
+/* Equations - inside decl box, no label */
+.lean-equation {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.85em;
+  line-height: 1.4;
+  color: #065f46;
+  background: #ecfdf5;
+  padding: 0.5rem;
+  margin: 0.5rem 0 0 0;
+  border-radius: 3px;
+  border-left: 3px solid #10b981;
+  overflow-x: auto;
+  white-space: pre-wrap;
+  word-break: break-word;
+}
+
+/* Equation HTML with links (doc-gen style) */
+.lean-equations {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.85em;
+  line-height: 1.5;
+  color: #065f46;
+  background: #ecfdf5;
+  padding: 0.5rem;
+  margin: 0.5rem 0 0 0;
+  border-radius: 3px;
+  border-left: 3px solid #10b981;
+  list-style: none;
+}
+
+.lean-equations li.equation {
+  margin: 0.25rem 0;
+  white-space: pre-wrap;
+  word-break: break-word;
+}
+
+.lean-equations a {
+  color: #1e40af;
+  text-decoration: none;
+}
+
+.lean-equations a:hover {
+  text-decoration: underline;
+}
+
+.lean-equations a.blueprint-link {
+  color: #0d9488;
+  font-weight: 500;
+}
+
+.lean-equations a.blueprint-link:hover {
+  color: #0f766e;
+}
+
+/* Structure fields - styled similarly to equations */
+.lean-structure-fields {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.85em;
+  line-height: 1.5;
+  color: #1e3a5f;
+  background: #eff6ff;
+  padding: 0.5rem;
+  margin: 0.5rem 0 0 0;
+  border-radius: 3px;
+  border-left: 3px solid #3b82f6;
+  list-style: none;
+}
+
+.lean-structure-fields li.structure_field {
+  margin: 0.4rem 0;
+  padding: 0.2rem 0;
+  border-bottom: 1px solid #dbeafe;
+}
+
+.lean-structure-fields li.structure_field:last-child {
+  border-bottom: none;
+}
+
+.lean-structure-fields .structure_field_info {
+  white-space: pre-wrap;
+  word-break: break-word;
+}
+
+.lean-structure-fields .structure_field_doc,
+.lean-structure-fields .structure_field_doc p {
+  font-size: 1.05em !important;
+  font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif !important;
+  color: #6b7280;
+  margin: 0;
+  margin-top: 0.15rem;
+  font-style: italic;
+  line-height: 1.3;
+}
+
+/* Code elements within structure field documentation should match surrounding text size */
+.lean-structure-fields .structure_field_doc code,
+.lean-structure-fields .structure_field_doc .docstring_code {
+  font-size: inherit !important;
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace !important;
+  font-style: normal;
+  background: rgba(59, 130, 246, 0.1);
+  padding: 0.1em 0.3em;
+  border-radius: 3px;
+  color: #1e40af;
+}
+
+.lean-structure-fields a {
+  color: #1e40af;
+  text-decoration: none;
+}
+
+.lean-structure-fields a:hover {
+  text-decoration: underline;
+}
+
+.lean-structure-fields a.blueprint-link {
+  color: #0d9488;
+  font-weight: 500;
+}
+
+.lean-structure-fields a.blueprint-link:hover {
+  color: #0f766e;
+}
+
+/* Plain text fallback for structure fields */
+.lean-fields {
+  font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace;
+  font-size: 0.85em;
+  line-height: 1.4;
+  color: #1e3a5f;
+  background: #eff6ff;
+  padding: 0.5rem;
+  margin: 0.5rem 0 0 0;
+  border-radius: 3px;
+  border-left: 3px solid #3b82f6;
+  overflow-x: auto;
+  white-space: pre-wrap;
+  word-break: break-word;
+}
+
+/* Blueprint links in declaration body */
+.lean-decl-box a.blueprint-link {
+  color: #0d9488;
+  font-weight: 500;
+}
+
+.lean-decl-box a.blueprint-link:hover {
+  color: #0f766e;
+  text-decoration: underline;
+}
+
+/* Target theorem styling - prominent, highlighted */
+.lean-side-panel.lean-target .lean-decl-box {
+  border-left-width: 6px;
+  border-left-color: #2563eb;
+  background: linear-gradient(135deg, #eff6ff 0%, #dbeafe 100%);
+  box-shadow: 0 2px 8px rgba(37, 99, 235, 0.15);
+}
+
+.lean-side-panel.lean-target .lean-decl-box .decl_name,
+.lean-side-panel.lean-target .lean-decl-box .decl_name a {
+  color: #1d4ed8;
+  font-size: 1.05em;
+}
+
+/* Helper lemma styling - subtle, muted */
+.lean-side-panel.lean-helper .lean-decl-box {
+  border-left-width: 2px;
+  border-left-color: #9ca3af;
+  background: linear-gradient(135deg, #f9fafb 0%, #f3f4f6 100%);
+  opacity: 0.85;
+  font-size: 0.9em;
+}
+
+.lean-side-panel.lean-helper .lean-decl-box .decl_name,
+.lean-side-panel.lean-helper .lean-decl-box .decl_name a {
+  color: #4b5563;
+}
+
+.lean-side-panel.lean-helper .lean-decl-box .decl_kind {
+  color: #6b7280;
+}
+
+/* Helper can expand on hover to show full detail */
+.lean-side-panel.lean-helper .lean-decl-box:hover {
+  opacity: 1;
+}
+
+/* Responsive: single column on narrow screens */
+@media (max-width: 1200px) {
+  div.main-text {
+    display: block; /* Fall back to normal flow */
+  }
+
+  div.main-text > .definition_thmwrapper,
+  div.main-text > .theorem_thmwrapper,
+  div.main-text > .lemma_thmwrapper,
+  div.main-text > .proposition_thmwrapper,
+  div.main-text > .corollary_thmwrapper,
+  div.main-text > .remark_thmwrapper,
+  div.main-text > .example_thmwrapper {
+    display: block;
+  }
+
+  .thm_side_panel {
+    margin-top: 1rem;
+  }
+
+  .lean-side-panel {
+    margin-top: 1rem;
+    padding-top: 1rem;
+    border-top: 1px solid #e5e7eb;
+    position: static;
+    max-height: none;
+  }
+}