Created
July 11, 2025 22:38
-
-
Save lakesare/65c96aee46e2eaf96a55d96751084e6b to your computer and use it in GitHub Desktop.
Paperproof in html form
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html lang="en"> | |
| <head> | |
| <meta charset="UTF-8"> | |
| <meta name="viewport" content="width=device-width, initial-scale=1.0"> | |
| <title>Paperproof Snapshot</title> | |
| <style> | |
| @import url('https://fonts.googleapis.com/css2?family=Roboto+Mono:ital,wght@0,100..700;1,100..700&display=swap'); | |
| </style> | |
| <style> | |
| .proof-tree.-isSingleTacticModeON{ | |
| #box-1{ width: 100vw !important; } | |
| /* This is so that unfolded theorems don't take up excessive space for no reason */ | |
| .tactic.-hypothesis-tactic{ | |
| display: block; | |
| } | |
| /* Makes yellow hypothesis color correct */ | |
| header div.row-1 > div{ | |
| flex-wrap: wrap; | |
| } | |
| .hypothesis.-highlighted, .hypothesis.data.-highlighted{ | |
| border-color: #72787C; | |
| } | |
| .hypothesis-table .hypothesis.-highlighted{ | |
| border-color: rgb(152 214 179) !important; | |
| } | |
| .single-tactic-hyp-row{ | |
| padding-top: 1px; | |
| display: block !important; | |
| .hypothesis{ | |
| display: block; | |
| width: fit-content; | |
| margin-top: 2px; | |
| } | |
| } | |
| .fancy-substring-theorem{ | |
| text-decoration: underline; | |
| text-decoration-color: #72787c; | |
| cursor: pointer; | |
| text-underline-offset: 2px; | |
| &:hover{ | |
| opacity: 0.8; | |
| } | |
| } | |
| .fancy-substring-hypothesis{ | |
| color: #d0005b; | |
| } | |
| } | |
| .tactic{ | |
| /* font-family: var(--vscode-editor-font-family); */ | |
| } | |
| .proof-tree.-we-are-on-ellipsis-tactic{ | |
| .hypothesis.-highlighted, .goal.-highlighted{ border-color: #72787C; } | |
| } | |
| /* This is for folding/unfolding `have`s */ | |
| .tactic.-hypothesis-tactic{ | |
| display: flex; | |
| justify-content: space-between; | |
| /* cursor: pointer; */ | |
| transition: background-color 0.5s ease; | |
| &.-highlight{ | |
| background-color: rgb(255, 146, 250) !important; | |
| } | |
| &:hover button{ | |
| background: none; | |
| opacity: 0.6; | |
| cursor: pointer; /* We do need { cursor: pointer } here too! */ | |
| } | |
| .text{ cursor: default; } | |
| button{ | |
| background: transparent; | |
| border: none; | |
| color: #6c8a97; | |
| padding: 0; | |
| padding-left: 10px; | |
| } | |
| .show-boxes{ | |
| margin-top: -6px; | |
| } | |
| .hide-boxes{ | |
| margin-top: -2px; | |
| } | |
| } | |
| /*______________________ BODY: prettiness ______________________*/ | |
| body *{ | |
| box-sizing: border-box; | |
| } | |
| .hypothesis span.name{ | |
| color: #d0005b; | |
| } | |
| /* | |
| Hides scrollbars - we can still scroll, but we don't want to show scrollbars. | |
| Notice we need both of these rules - one for ubuntu, another for osx. | |
| */ | |
| html{ scrollbar-width: none; } | |
| body::-webkit-scrollbar{ display: none; } | |
| body{ | |
| background: white; | |
| color: #3a505a; | |
| font-weight: 500; | |
| /* Make tldraw bg dark for dark vscode themes */ | |
| &.vscode-dark{ | |
| background-color: var(--vscode-editor-background); | |
| } | |
| .proof-tree{ | |
| border-radius: 3px; | |
| background: white; | |
| } | |
| /* | |
| Same font-family as InfoView's. | |
| Most importantly, makes symbols such as "∀ x ∈ A ∩ B, x ∈ A" render nicely. | |
| */ | |
| .hypothesis, .goal{ | |
| font-family: var(--vscode-editor-font-family); | |
| } | |
| } | |
| /*______________________ BODY: widths for zooming ______________________*/ | |
| body{ | |
| padding: 70vh 70vw; | |
| width: fit-content; | |
| .proof-tree{ | |
| width: max-content; | |
| transform-origin: 0% 0% 0px; | |
| } | |
| } | |
| /*______________________ ARROWS ______________________*/ | |
| .proof-tree{ | |
| position: relative; | |
| } | |
| .perfect-arrow{ | |
| position: absolute; | |
| top: 0; left: 0; | |
| z-index: 0; | |
| pointer-events: none; | |
| stroke-width: 2px; | |
| stroke: #a0ceb0; | |
| fill: #a0ceb0; | |
| } | |
| .tactic{ | |
| .perfect-arrow{ | |
| display: none; | |
| } | |
| &:hover .perfect-arrow, | |
| &.-success .perfect-arrow{ | |
| display: block; | |
| } | |
| } | |
| .proof-tree.-isSingleTacticModeON{ | |
| .tactic .perfect-arrow{ z-index: 5; display: block; } | |
| } | |
| /*______________________ PROOF-TREE: colors ______________________*/ | |
| /* This would be really easy to achieve with opacities, however various nodes goalUsernames must *cover* tactic borders to make them look good, which means they must be solid-color. */ | |
| .box{ | |
| --color: color-mix(in srgb, rgba(132, 147, 171), white calc(90% - var(--level) * 7%)); | |
| background: var(--color); | |
| /* This is necessary because otherwise the border-right will get swallowed up a bit (becomes too thin) in some tactic nodes */ | |
| .tactic{ background-color: var(--color); } | |
| } | |
| .box > .goal-username{ | |
| background: color-mix(in srgb, rgba(132, 147, 171), white calc(80% - var(--level) * 7%)); | |
| } | |
| /* We can also adjust node colors in the future */ | |
| /* .hypothesis{ | |
| background: color-mix(in srgb, #a4dabc, rgba(132, 147, 171) calc(var(--level) * 7%)) !important; | |
| border-color: color-mix(in srgb, rgb(124 211 158), rgba(132, 147, 171) calc(var(--level) * 7%)) !important; | |
| } */ | |
| .box { --level: 0; | |
| & .box{ --level: 1; | |
| & .box{ --level: 2; | |
| & .box{ --level: 3; | |
| & .box{ --level: 4; | |
| & .box{ --level: 5; | |
| & .box{ --level: 6; | |
| & .box{ --level: 7; | |
| & .box{ --level: 8; | |
| }}}}}}}}} | |
| /*______________________ PROOF-TREE: prettiness ______________________*/ | |
| .box{ | |
| font-size: 12px; | |
| border-radius: 3px; | |
| flex-grow: 1; | |
| .child-boxes, .byBoxes{ | |
| display: flex; | |
| justify-content: space-between; | |
| align-items: flex-end; | |
| gap: 10px; | |
| } | |
| table.hypothesis-table{ | |
| border-spacing: 0; | |
| td{ | |
| padding: 0; | |
| padding-right: 2px; | |
| vertical-align: top; | |
| } | |
| td:last-child { | |
| padding-right: 0; | |
| } | |
| } | |
| .goal-username{ | |
| width: 100%; | |
| text-align: center; | |
| color: #9c9797; | |
| padding: 0 10px; | |
| padding-bottom: 1px; | |
| } | |
| } | |
| .hypothesis, .goal, .tactic{ | |
| flex-wrap: wrap; | |
| padding: 5px 12px; | |
| border-radius: 3px; | |
| /* exactly 3 lines */ | |
| line-height: 1.3em; | |
| /* max-height: calc(1.3em * 3 + 12px); */ | |
| /* overflow-y: auto; */ | |
| word-break: break-word; | |
| } | |
| /* We need this to make sure <goal>s and <hyp>s stay on top of <tactic>s */ | |
| .goal, .hypothesis{ position: relative; } | |
| /* We need this to make sure <hyp>s stay on top of <tactic>s and arrows */ | |
| .hypothesis{ z-index: 1; } | |
| /* We need this to make sure <hyp>s stay on top of <tactic>s, but below arrows */ | |
| .goal{ z-index: 0; } | |
| .tactic{ | |
| margin-top: -2px; margin-bottom: -2px; | |
| padding-top: 7px; padding-bottom: 7px; | |
| color: #72787c; | |
| background-image: url("data:image/svg+xml,%3csvg width='100%25' height='100%25' xmlns='http://www.w3.org/2000/svg'%3e%3crect width='100%25' height='100%25' fill='none' stroke='%23c7ccce' stroke-width='3' stroke-dasharray='4%2c 6' stroke-dashoffset='0' stroke-linecap='square'/%3e%3c/svg%3e"); | |
| &.-position-matches{ | |
| font-weight: bold; | |
| color: #363d59; | |
| } | |
| &.-success{ | |
| /* center text */ | |
| display: flex; | |
| justify-content: center; | |
| align-items: center; | |
| text-align: center; | |
| gap: 7px; | |
| background: rgb(0 213 255 / 12%); | |
| background-image: url("data:image/svg+xml,%3csvg width='100%25' height='100%25' xmlns='http://www.w3.org/2000/svg'%3e%3crect width='100%25' height='100%25' fill='none' stroke='%239ed6e1' stroke-width='3' stroke-dasharray='4%2c 5' stroke-dashoffset='0' stroke-linecap='square'/%3e%3c/svg%3e"); | |
| } | |
| &.-with-theorem{ | |
| background-color: transparent !important; | |
| } | |
| &.-sorried{ | |
| text-align: center; | |
| background: #f2ded94f; | |
| background-image: url("data:image/svg+xml,%3csvg width='100%25' height='100%25' xmlns='http://www.w3.org/2000/svg'%3e%3crect width='100%25' height='100%25' fill='none' stroke='%23f0cac196' stroke-width='3' stroke-dasharray='4%2c 6' stroke-dashoffset='0' stroke-linecap='square'/%3e%3c/svg%3e"); | |
| } | |
| &.-ellipsis{ | |
| text-align: center; | |
| font-weight: bold; | |
| color: #363d59; | |
| letter-spacing: 2px; | |
| background: rgba(82, 95, 98, 0.049); | |
| background-image: url("data:image/svg+xml,%3csvg width='100%25' height='100%25' xmlns='http://www.w3.org/2000/svg'%3e%3crect width='100%25' height='100%25' fill='none' stroke='%23c7ccce' stroke-width='3' stroke-dasharray='4%2c 6' stroke-dashoffset='0' stroke-linecap='square'/%3e%3c/svg%3e"); | |
| } | |
| &.-sorried, &.-success, &.-ellipsis{ | |
| /* increase padding by 1px, looks better this way */ | |
| padding-top: 8px; | |
| padding-bottom: 8px; | |
| } | |
| } | |
| .hypothesis{ | |
| background: #a4dabc; | |
| border: 2px solid rgb(152 214 179); | |
| .name{ color: #d0005b; } | |
| &.-hidden{ cursor: pointer; } | |
| } | |
| .-isGreenHypothesesOFF{ | |
| .hypothesis.data{ | |
| background: #f9e9b5; | |
| border: 2px solid rgb(239, 227, 152); | |
| } | |
| } | |
| .goal{ | |
| background: rgb(249, 195, 195); | |
| border: 2px solid rgb(246, 185, 185); | |
| color: #5a5656; | |
| } | |
| .proof-tree.-isHiddenGoalNamesON{ | |
| .goal-username{ | |
| display: none; | |
| } | |
| } | |
| /*______________________ PROOF-TREE: paddings ______________________*/ | |
| /* This is the easiest way to acommodate for our nice negative-margin <tactic>s */ | |
| .box-insides{ padding-top: 2px; } | |
| /* .data-hypotheses{ margin-top: -2px; } */ | |
| .box-insides{ | |
| padding: 10px; | |
| padding-top: 12px; | |
| padding-bottom: 0; | |
| } | |
| table.hypothesis-table{ | |
| margin-bottom: 12px; | |
| } | |
| table.hypothesis-table + .goals{ | |
| margin-top: 30px; | |
| } | |
| .proof-tree.-isCompactModeON{ | |
| #box-1 .child-boxes { | |
| header, .box-insides{ | |
| padding-left: 0px; | |
| padding-right: 0px; | |
| } | |
| } | |
| } | |
| /* This might be our "symmetrical mode" */ | |
| /* .proof-tree.-isSymmetricalModeON{ | |
| .box-insides{ | |
| padding-left: 1px; | |
| padding-right: 1px; | |
| } | |
| } */ | |
| /*______________________ PROOF-TREE: widths ______________________*/ | |
| .box{ | |
| width: max-content; | |
| } | |
| header, footer{ | |
| background: rgb(230, 233, 238); | |
| .title{ | |
| text-transform: uppercase; | |
| font-size: 10px; | |
| padding: 4px 10px; | |
| width: 100%; | |
| text-align: center; | |
| color: rgb(156, 151, 151); | |
| } | |
| } | |
| /* All of this header logic is just to make the paddings look pretty */ | |
| header{ | |
| padding-left: 10px; | |
| padding-right: 10px; | |
| border-top-left-radius: 3px; | |
| border-top-right-radius: 3px; | |
| width: 0; | |
| min-width: 100%; | |
| --hypNodeHeight: 30px; | |
| --bigPaddingBottom: 5px; | |
| &.-hoistAndPaddingBottomSmall, &.-hoistAndPaddingBottomBig{ | |
| position: relative; | |
| div.row-1{ | |
| padding-bottom: 2px; | |
| } | |
| div.row-2{ | |
| height: calc(var(--hypNodeHeight) + var(--bigPaddingBottom)); | |
| position: absolute; | |
| top: 100%; left: 0; | |
| width: 100%; | |
| background: rgb(230, 233, 238); | |
| } | |
| &+.box-insides{ | |
| padding-top: 0; | |
| /* | |
| This makes sure header hypotheses not exceed 30px in height [in most cases!] | |
| TODO remove this when vscode switches to Chrome 125, and we can switch to anchor tags, | |
| see a related TODO in <Header/> | |
| */ | |
| .hypothesis-table:first-child tr:nth-child(2) div.hypothesis { | |
| max-width: 300px !important; | |
| } | |
| } | |
| } | |
| &.-hoistAndPaddingBottomBig +.box-insides{ | |
| > .hypothesis-table:first-child tr:nth-child(3) td{ | |
| padding-top: 20px; | |
| } | |
| } | |
| &.-hoistAndPaddingBottomSmall{ | |
| div.row-2{ | |
| height: var(--hypNodeHeight); | |
| } | |
| } | |
| &.-row2Absent{ | |
| div.row-1{ | |
| padding-bottom: 5px; | |
| } | |
| } | |
| div.row-1 > div{ | |
| width: 100%; | |
| display: flex; | |
| flex-wrap: wrap-reverse; | |
| column-gap: 2px; | |
| row-gap: 2px; | |
| } | |
| } | |
| footer{ | |
| border-bottom-left-radius: 3px; | |
| border-bottom-right-radius: 3px; | |
| } | |
| .hypothesis-table{ | |
| .hypothesis{ | |
| width: fit-content; | |
| max-width: 200px; | |
| min-width: 100%; | |
| } | |
| } | |
| /* tactics will just follow hyp widths */ | |
| .proof-tree.-isCompactTacticsON .tactic.-hypothesis-tactic{ | |
| width: min-content; | |
| max-width: 100%; | |
| min-width: 100%; | |
| word-break: break-all; | |
| } | |
| /* tactics will have self-respect */ | |
| .proof-tree.-isCompactTacticsOFF .tactic.-hypothesis-tactic, | |
| .proof-tree.-isCompactTacticsON .tactic.-hypothesis-tactic.-with-self-respect{ | |
| width: 100% ; | |
| min-width: min-content ; | |
| } | |
| .goals{ | |
| .goal{ | |
| max-width: 200px; | |
| min-width: 100%; | |
| } | |
| .tactic{ | |
| max-width: 200px; | |
| min-width: 100%; | |
| } | |
| } | |
| #box-1 > .box-insides > .goals{ | |
| min-width: 200px; | |
| } | |
| /*______________________ DEVELOPMENT ______________________*/ | |
| .-hint pre{ | |
| display: none; | |
| position: fixed; | |
| bottom: 0; right: 0; | |
| margin: 0; | |
| padding: 10px; | |
| background: rgba(255, 255, 255, 0.95); | |
| z-index: 1000; | |
| border-radius: 3px; | |
| } | |
| .-hint:hover pre{ | |
| display: block; | |
| } | |
| /* Snapshot-specific overrides */ | |
| .proof-tree { | |
| transform: none !important; | |
| } | |
| .perfect-arrow { | |
| display: none !important; | |
| } | |
| /* Disable interactive elements in snapshot */ | |
| button { pointer-events: none; } | |
| .MuiMenu-root { display: none !important; } | |
| body{ | |
| font-family: monospace; | |
| --vscode-editor-font-family: monospace; | |
| padding: 0 !important; | |
| } | |
| *{ | |
| font-family: monospace !important; | |
| } | |
| </style> | |
| </head> | |
| <body> | |
| <div class=" | |
| proof-tree | |
| -isCompactTacticsOFF | |
| -isHiddenGoalNamesON | |
| -isGreenHypothesesOFF | |
| " style="transform: scale(0.772376);"><section class="box " id="box-1"><header class=" | |
| -hoistAndPaddingBottomSmall | |
| "><div class="title">hypotheses</div><div class="row-1"><div><div id="hypothesis-_uniq.27069" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">inst✝¹</span>: <span class="text">DecidableEq α</span></div><div id="hypothesis-_uniq.28459" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">M</span>: <span class="text">Matroid α</span></div></div></div><div class="row-2"></div></header><div class="box-insides"><table class="hypothesis-table"><tbody><tr><td colspan="6"></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.28460" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">inst✝</span>: <span class="text">M.RankFinite</span></div></td><td colspan="5"><div id="hypothesis-_uniq.28461" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hM</span>: <span class="text">M.IsRegular</span></div></td></tr><tr><td></td><td colspan="5"><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| " id="tactic-2-0"><div class="text">obtain ⟨X, Y, A, hA_TU, hA_eq⟩ := <span class="fancy-substring-hypothesis">hM</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M535.7733641316293,80.60155732876134 Q535.7733641316293,80.60155732876134 535.7733641316293,80.60155732876134" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(535.7733641316293,80.60155732876134) rotate(-90)"></polygon></svg></div></td></tr><tr><td></td><td colspan="1"><div id="hypothesis-_uniq.28483" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">X</span>: <span class="text">Set α</span></div></td><td colspan="1"><div id="hypothesis-_uniq.28501" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">Y</span>: <span class="text">Set α</span></div></td><td colspan="1"><div id="hypothesis-_uniq.28519" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">A</span>: <span class="text">Matrix ↑X ↑Y ℚ</span></div></td><td colspan="1"><div id="hypothesis-_uniq.28541" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hA_TU</span>: <span class="text">A.IsTotallyUnimodular</span></div></td><td colspan="1"><div id="hypothesis-_uniq.28542" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hA_eq</span>: <span class="text">A.toMatroid = M</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="2"><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| " id="tactic-3-0"><div class="text">obtain ⟨⟨G, hG_base⟩⟩ := (inferInstance : Nonempty {B // <span class="fancy-substring-hypothesis">M</span>.IsBase B})</div></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.28633" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">G</span>: <span class="text">Set α</span></div></td><td colspan="1"><div id="hypothesis-_uniq.28634" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hG_base</span>: <span class="text">M.IsBase G</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-2"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-6"><div class="text"><span>🎉</span> <span>exact <span class="fancy-substring-hypothesis">hG_base</span></span> <span>🎉</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M276.3124409252363,218.60930494172771 Q254.56097578465446,228.28442519333612 232.80951064407265,237.95954544494452" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(232.80951064407265,237.95954544494452) rotate(156.02035098058482)"></polygon></svg></div><div class="goal -hint "><div class="text">M.IsBase G</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-5"><div class="text">rw [<span class="fancy-substring-hypothesis">hA_eq</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M801.2106401272259,135.80464847168832 Q517.2047136395397,216.02204097007206 233.1987871518536,296.2394334684558" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(233.1987871518536,296.2394334684558) rotate(164.2276823531978)"></polygon></svg></div><div class="goal -hint "><div class="text">A.toMatroid.IsBase G</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-4-0"><div class="text">have hAG_base : <span class="fancy-substring-hypothesis">A</span>.toMatroid.IsBase <span class="fancy-substring-hypothesis">G</span> := by rw [<span class="fancy-substring-hypothesis">hA_eq</span>]; exact <span class="fancy-substring-hypothesis">hG_base</span></div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.28657" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hAG_base</span>: <span class="text">A.toMatroid.IsBase G</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-3"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-8"><div class="text"><span>🎉</span> <span>exact (IsBase.finite <span class="fancy-substring-hypothesis">hG_base</span>).fintype</span> <span>🎉</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M92.4999958442017,80.60155732876134 Q148.26825369447894,252.9052241394609 204.03651154475617,425.2088909501605" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(204.03651154475617,425.2088909501605) rotate(72.06517093481133)"></polygon></svg><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M276.3124409252363,218.60930494172771 Q242.64567421979257,321.91160457413105 208.97890751434883,425.2139042065343" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(208.97890751434883,425.2139042065343) rotate(108.05106351305334)"></polygon></svg></div><div class="goal -hint "><div class="text">Fintype ↑G</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-7-0"><div class="text">have wow : Fintype <span class="fancy-substring-hypothesis">G</span> := by exact (IsBase.finite <span class="fancy-substring-hypothesis">hG_base</span>).fintype</div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.28856" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">wow</span>: <span class="text">Fintype ↑G</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="4"><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| " id="tactic-9-0"><div class="text">obtain ⟨S, _, hS_eq, hS_TU⟩ := <span class="fancy-substring-hypothesis">A</span>.exists_standardRepr_isBase_isTotallyUnimodular <span class="fancy-substring-hypothesis">hAG_base</span> <span class="fancy-substring-hypothesis">hA_TU</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M225.4999958442017,410.21859275388545 Q290.0499031074969,480.7712758057576 354.59981037079206,551.3239588576298" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(354.59981037079206,551.3239588576298) rotate(47.544049385428075)"></polygon></svg><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M605.7107502505864,150.80464847168832 Q484.9248494085589,350.5924402757411 364.1389485665313,550.3802320797939" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(364.1389485665313,550.3802320797939) rotate(121.15594015748974)"></polygon></svg></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.29069" class=" | |
| hypothesis | |
| -hint | |
| data | |
| "><span class="name">S</span>: <span class="text">StandardRepr α ℚ</span></div></td><td colspan="1"><div id="hypothesis-_uniq.29087" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">left✝</span>: <span class="text">S.X = G</span></div></td><td colspan="1"><div id="hypothesis-_uniq.29105" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hS_eq</span>: <span class="text">S.toMatroid = A.toMatroid</span></div></td><td colspan="1"><div id="hypothesis-_uniq.29106" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hS_TU</span>: <span class="text">S.B.IsTotallyUnimodular</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-10-0"><div class="text">have h_dual_eq : <span class="fancy-substring-hypothesis">S</span>.toMatroid✶ = <span class="fancy-substring-hypothesis">S</span>✶.toMatroid := StandardRepr.toMatroid_dual_eq <span class="fancy-substring-hypothesis">S</span></div></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.31650" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">h_dual_eq</span>: <span class="text">S.toMatroid✶ = S✶.toMatroid</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-4"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-14"><div class="text"><span>🎉</span> <span>rw [rfl]</span> <span>🎉</span></div></div><div class="goal -hint "><div class="text">M = M</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-13"><div class="text">rw [<span class="fancy-substring-hypothesis">hA_eq</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M801.2106401272259,135.80464847168832 Q497.86886646151726,453.22908745678853 194.52709279580858,770.6535264418887" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(194.52709279580858,770.6535264418887) rotate(133.70041427340104)"></polygon></svg></div><div class="goal -hint "><div class="text">A.toMatroid = M</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-12"><div class="text">rw [<span class="fancy-substring-hypothesis">hS_eq</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M408.42957613250786,628.8278963225165 Q301.6522490524301,727.5190722568726 194.87492197235235,826.2102481912287" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(194.87492197235235,826.2102481912287) rotate(137.25369515042465)"></polygon></svg></div><div class="goal -hint "><div class="text">S.toMatroid = M</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-11-0"><div class="text">have h_M_eq_S : <span class="fancy-substring-hypothesis">S</span>.toMatroid = <span class="fancy-substring-hypothesis">M</span> := by rw [<span class="fancy-substring-hypothesis">hS_eq</span>, <span class="fancy-substring-hypothesis">hA_eq</span>]</div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.31668" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">h_M_eq_S</span>: <span class="text">S.toMatroid = M</span></div></td></tr></tbody></table><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-5"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-18"><div class="text"><span>🎉</span> <span>rw [rfl]</span> <span>🎉</span></div></div><div class="goal -hint "><div class="text">S✶.toMatroid = S✶.toMatroid</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-17"><div class="text">rw [<span class="fancy-substring-hypothesis">h_dual_eq</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M253.9999958442017,696.6325923038537 Q240.34164993812504,855.9557152800337 226.6833040320484,1015.2788382562136" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(226.6833040320484,1015.2788382562136) rotate(94.89983437244253)"></polygon></svg></div><div class="goal -hint "><div class="text">S.toMatroid✶ = S✶.toMatroid</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-16"><div class="text">rw [←<span class="fancy-substring-hypothesis">h_M_eq_S</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M188.9999958442017,943.4449712589384 Q206.4427457156682,1007.0911033591865 223.88549558713467,1070.7372354594347" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(223.88549558713467,1070.7372354594347) rotate(74.67392350534193)"></polygon></svg></div><div class="goal -hint "><div class="text">M✶ = S✶.toMatroid</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-15-0"><div class="text">have h_M_dual : <span class="fancy-substring-hypothesis">M</span>✶ = <span class="fancy-substring-hypothesis">S</span>✶.toMatroid := by rw [←<span class="fancy-substring-hypothesis">h_M_eq_S</span>, <span class="fancy-substring-hypothesis">h_dual_eq</span>]</div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.34201" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">h_M_dual</span>: <span class="text">M✶ = S✶.toMatroid</span></div></td></tr></tbody></table><div class="child-boxes"><section class="box " id="box-6"><div class="box-insides"><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-8"><div class="box-insides"><table class="hypothesis-table"><tbody><tr><td colspan="1"><div class="child-boxes"><section class="box " id="box-9"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-24"><div class="text"><span>🎉</span> <span>exact Matrix.IsTotallyUnimodular.transpose <span class="fancy-substring-hypothesis">hS_TU</span></span> <span>🎉</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M610.4295055204452,628.8278963225165 Q403.4823617020561,929.5482633395704 196.535217883667,1230.2686303566243" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(196.535217883667,1230.2686303566243) rotate(124.53463499756687)"></polygon></svg></div><div class="goal -hint "><div class="text">S.Bᵀ.IsTotallyUnimodular</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-23-0"><div class="text">have hB_transpose : <span class="fancy-substring-hypothesis">S</span>.Bᵀ.IsTotallyUnimodular := by</div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.41374" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hB_transpose</span>: <span class="text">S.Bᵀ.IsTotallyUnimodular</span></div></td></tr></tbody></table><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-26"><div class="text"><span>🎉</span> <span>exact Matrix.IsTotallyUnimodular.neg <span class="fancy-substring-hypothesis">hB_transpose</span></span> <span>🎉</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M191.99999000206122,1366.265088455542 Q191.99999000206122,1376.5659006925143 191.99999000206122,1386.8667129294865" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(191.99999000206122,1386.8667129294865) rotate(90)"></polygon></svg></div><div class="goal -hint "><div class="text">(StandardRepr.mk S.Y S.X ⋯ (-S.Bᵀ) S.decmemY S.decmemX).B.IsTotallyUnimodular</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-25"><div class="text">rw [StandardRepr.dual]</div></div><div class="goal -hint "><div class="text">S✶.B.IsTotallyUnimodular</div></div></div></div><div class="goal-username">[anonymous]</div></section></div><div class=" | |
| tactic -hint | |
| -hypothesis-tactic | |
| -with-self-respect | |
| " id="tactic-22-0"><div class="text">have hS_B_TU : <span class="fancy-substring-hypothesis">S</span>✶.B.IsTotallyUnimodular := by</div><button type="button" class="hide-boxes">▬</button></div></td></tr><tr><td colspan="1"><div id="hypothesis-_uniq.41339" class=" | |
| hypothesis | |
| -hint | |
| proof | |
| "><span class="name">hS_B_TU</span>: <span class="text">S✶.B.IsTotallyUnimodular</span></div></td></tr></tbody></table><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-28"><div class="text"><span>🎉</span> <span>exact <span class="fancy-substring-hypothesis">hS_B_TU</span></span> <span>🎉</span></div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M191.9999916884034,1610.6791316360977 Q224.52907369979982,1623.511951596196 257.05815571119626,1636.3447715562943" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(257.05815571119626,1636.3447715562943) rotate(21.529382318239122)"></polygon></svg></div><div class="goal -hint "><div class="text">S✶.B.IsTotallyUnimodular</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-27"><div class="text">rw [StandardRepr.toFull_isTotallyUnimodular_iff]</div></div><div class="goal -hint "><div class="text">S✶.toFull.IsTotallyUnimodular</div></div></div></div><div class="goal-username">h.left</div></section><section class="box " id="box-7"><div class="box-insides"><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| -success | |
| " id="tactic-29"><div class="text"><span>🎉</span> <span>rfl</span> <span>🎉</span></div></div><div class="goal -hint "><div class="text">S✶.toFull.toMatroid = S✶.toMatroid</div></div></div></div><div class="goal-username">h.right</div></section></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-21"><div class="text">constructor</div></div><div class="goal -hint "><div class="text">S✶.toFull.IsTotallyUnimodular ∧ S✶.toFull.toMatroid = S✶.toMatroid</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-20"><div class="text">use <span class="fancy-substring-hypothesis">S</span>✶.X, <span class="fancy-substring-hypothesis">S</span>✶.X ∪ <span class="fancy-substring-hypothesis">S</span>✶.Y, <span class="fancy-substring-hypothesis">S</span>✶.toFull</div></div><div class="goal -hint "><div class="text">S✶.toMatroid.IsRegular</div></div></div><div class="goals"><div class="byBoxes"></div><div class=" | |
| tactic -hint | |
| " id="tactic-19"><div class="text">rw [<span class="fancy-substring-hypothesis">h_M_dual</span>]</div><svg class="perfect-arrow" viewBox="0 0 10000 10000" style="width: 10000px; height: 10000px;"><path d="M225.9999958442017,1190.257350214023 Q337.9721199096966,1522.384800439575 449.94424397519145,1854.5122506651269" fill="none"></path><polygon points="0,-3 6,0, 0,3" transform="translate(449.94424397519145,1854.5122506651269) rotate(71.3691856871637)"></polygon></svg></div><div class="goal -hint "><div class="text">M✶.IsRegular</div></div></div></div><footer><div class="title">theorem</div></footer></section></div> | |
| </body> | |
| </html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment