.lean-learning-studio {
  margin: 2.2rem 0 2.6rem;
  border: 1px solid color-mix(in srgb, var(--lean) 35%, var(--line));
  background:
    linear-gradient(145deg, color-mix(in srgb, var(--surface) 95%, var(--lean) 5%), var(--surface));
  border-radius: calc(var(--radius) + 5px);
  box-shadow: var(--shadow);
  overflow: hidden;
}

.lean-learning-studio > header {
  display: grid;
  grid-template-columns: minmax(0, 1fr) auto;
  gap: 1.25rem;
  align-items: start;
  padding: 1.5rem 1.6rem 1.25rem;
  border-bottom: 1px solid var(--line);
}

.lean-learning-studio .studio-kicker {
  display: block;
  margin-bottom: 0.35rem;
  color: var(--lean);
  font-size: 0.72rem;
  font-weight: 750;
  letter-spacing: 0.1em;
  text-transform: uppercase;
}

.lean-learning-studio h2 {
  margin-bottom: 0.45rem;
  font-family: var(--font-display);
  font-size: 2.05rem;
}

.lean-learning-studio header p {
  max-width: 68ch;
  margin: 0;
  color: var(--muted);
}

.lean-language-toggle {
  white-space: nowrap;
  color: var(--lean);
  border-color: color-mix(in srgb, var(--lean) 35%, var(--line));
}

.reading-mode-strip,
.graph-mode-strip {
  display: flex;
  flex-wrap: wrap;
  gap: 0.45rem;
}

.reading-mode-strip {
  padding: 1rem 1.6rem;
  border-bottom: 1px solid var(--line);
  background: color-mix(in srgb, var(--surface-2) 72%, transparent);
}

.reading-mode-strip::before {
  content: "Reading depth";
  display: inline-flex;
  align-items: center;
  margin-right: 0.35rem;
  color: var(--muted);
  font-size: 0.72rem;
  font-weight: 700;
  letter-spacing: 0.05em;
  text-transform: uppercase;
}

.mode-button,
.graph-mode-button {
  padding: 0.42rem 0.72rem;
  color: var(--muted);
  background: var(--surface);
  border: 1px solid var(--line);
  border-radius: 999px;
  font-size: 0.75rem;
  font-weight: 700;
}

.mode-button.active,
.graph-mode-button.active {
  color: white;
  background: var(--lean);
  border-color: var(--lean);
}

.mode-explanation {
  display: grid;
  grid-template-columns: repeat(3, minmax(0, 1fr));
  gap: 1px;
  background: var(--line);
  border-bottom: 1px solid var(--line);
}

.mode-explanation > div {
  padding: 0.9rem 1.1rem;
  background: var(--surface);
}

.mode-explanation strong,
.mode-explanation span {
  display: block;
}

.mode-explanation strong {
  margin-bottom: 0.2rem;
  font-size: 0.78rem;
}

.mode-explanation span {
  color: var(--muted);
  font-size: 0.72rem;
}

.lean-studio-workbench {
  padding: 1.35rem 1.6rem 1.6rem;
}

.lean-studio-workbench > section + section {
  margin-top: 1.6rem;
  padding-top: 1.5rem;
  border-top: 1px solid var(--line);
}

.lean-studio-workbench h3 {
  margin-bottom: 0.4rem;
  font-size: 1.15rem;
}

.lean-studio-intro {
  max-width: 78ch;
  color: var(--muted);
}

.graph-toolbar {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 1rem;
  margin: 0.9rem 0 0.65rem;
}

.lean-graph-stats {
  color: var(--muted);
  font-size: 0.72rem;
}

.lean-graph-frame {
  overflow-x: auto;
  border: 1px solid var(--line);
  background:
    radial-gradient(circle at 1px 1px, color-mix(in srgb, var(--line) 80%, transparent) 1px, transparent 0) 0 0 / 20px 20px,
    var(--surface);
  border-radius: var(--radius);
}

.lean-proof-graph {
  display: block;
  width: 100%;
  min-width: 760px;
  min-height: 320px;
}

.graph-edges line {
  stroke: color-mix(in srgb, var(--muted) 55%, transparent);
  stroke-width: 1.5;
}

.graph-node rect {
  fill: var(--surface);
  stroke: var(--line);
  stroke-width: 1.5;
  transition: 140ms ease;
}

.graph-node text {
  fill: var(--ink);
  font: 600 12px var(--font-code);
  pointer-events: none;
}

.graph-node .graph-node-kind {
  fill: var(--muted);
  font: 600 10px var(--font-body);
  text-transform: uppercase;
}

.graph-node.prerequisite rect {
  stroke: color-mix(in srgb, var(--rigorous) 65%, var(--line));
}

.graph-node.consumer rect {
  stroke: color-mix(in srgb, var(--accent) 65%, var(--line));
}

.graph-node.current rect {
  fill: color-mix(in srgb, var(--lean) 12%, var(--surface));
  stroke: var(--lean);
  stroke-width: 2.6;
}

.graph-node:hover rect {
  fill: var(--surface-2);
  stroke-width: 2.6;
}

.lean-reading-recipe {
  display: grid;
  grid-template-columns: repeat(4, minmax(0, 1fr));
  gap: 0.65rem;
  margin: 1rem 0;
  padding: 0;
  list-style: none;
  counter-reset: leanread;
}

.lean-reading-recipe li {
  counter-increment: leanread;
  min-height: 105px;
  margin: 0;
  padding: 0.85rem;
  border: 1px solid var(--line);
  background: var(--surface);
  border-radius: var(--radius);
  font-size: 0.75rem;
}

.lean-reading-recipe li::before {
  content: "0" counter(leanread);
  display: block;
  margin-bottom: 0.45rem;
  color: var(--lean);
  font: 700 0.72rem var(--font-code);
}

.lean-reading-recipe strong {
  display: block;
  margin-bottom: 0.2rem;
}

.lean-reading-recipe span {
  color: var(--muted);
}

.lean-line-tutor {
  border: 1px solid var(--line);
  border-radius: var(--radius);
  overflow: hidden;
}

.lean-line-explanation {
  display: grid;
  grid-template-columns: 42px minmax(280px, 0.95fr) minmax(300px, 1.05fr);
  align-items: stretch;
  margin: 0;
  border-bottom: 1px solid var(--line);
  background: var(--surface);
}

.lean-line-explanation:last-of-type {
  border-bottom: 0;
}

.lean-line-number {
  display: grid;
  place-items: start center;
  padding-top: 0.75rem;
  color: var(--muted);
  background: var(--surface-2);
  font: 500 0.7rem var(--font-code);
}

.lean-line-explanation pre {
  margin: 0;
  padding: 0.72rem 0.85rem;
  overflow-x: auto;
  border-right: 1px solid var(--line);
  background: color-mix(in srgb, var(--surface) 93%, var(--lean) 7%);
  font-size: 0.72rem;
  line-height: 1.55;
}

.lean-line-natural {
  padding: 0.65rem 0.8rem;
}

.lean-line-natural p {
  margin: 0 0 0.45rem;
  font-size: 0.75rem;
}

.syntax-chips {
  display: flex;
  flex-wrap: wrap;
  gap: 0.3rem;
}

.syntax-chip {
  padding: 0.18rem 0.42rem;
  color: var(--lean);
  border: 1px solid color-mix(in srgb, var(--lean) 28%, var(--line));
  background: color-mix(in srgb, var(--lean) 7%, var(--surface));
  border-radius: 999px;
  font: 600 0.64rem var(--font-code);
}

.syntax-chip:hover,
.syntax-chip:focus-visible {
  border-color: var(--lean);
  background: color-mix(in srgb, var(--lean) 13%, var(--surface));
}

.lean-show-all {
  display: block;
  margin: 1rem auto;
}

.lean-syntax-glossary {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 0.55rem;
}

.lean-syntax-entry {
  border: 1px solid var(--line);
  background: var(--surface);
  border-radius: var(--radius);
}

.lean-syntax-entry summary {
  cursor: pointer;
  padding: 0.65rem 0.75rem;
}

.lean-syntax-entry p {
  margin: 0;
  padding: 0 0.75rem 0.75rem;
  color: var(--muted);
  font-size: 0.75rem;
}

.prerequisite-decl-links {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(230px, 1fr));
  gap: 0.55rem;
}

.prerequisite-decl-links a {
  display: flex;
  flex-direction: column;
  gap: 0.2rem;
  padding: 0.7rem;
  border: 1px solid var(--line);
  background: var(--surface);
  border-radius: var(--radius);
  text-decoration: none;
}

.prerequisite-decl-links a span {
  color: var(--muted);
  font-size: 0.66rem;
}

body[data-reading-mode="beginner"] .rigorous-lesson-panel,
body[data-reading-mode="beginner"] .rigorous-reference-panel,
body[data-reading-mode="beginner"] details.formalization-lens,
body[data-reading-mode="beginner"] .lean-studio-workbench {
  display: none !important;
}

body[data-reading-mode="rigorous"] details.formalization-lens,
body[data-reading-mode="rigorous"] .lean-tutor-section {
  display: none !important;
}

body[data-reading-mode="lean"] .rigorous-lesson-panel,
body[data-reading-mode="lean"] .rigorous-reference-panel,
body[data-reading-mode="lean"] details.formalization-lens,
body[data-reading-mode="lean"] .lean-studio-workbench {
  display: block;
}

@media (max-width: 900px) {
  .lean-learning-studio > header {
    grid-template-columns: 1fr;
  }

  .mode-explanation,
  .lean-reading-recipe,
  .lean-syntax-glossary {
    grid-template-columns: 1fr 1fr;
  }

  .lean-line-explanation {
    grid-template-columns: 36px minmax(0, 1fr);
  }

  .lean-line-explanation pre {
    border-right: 0;
  }

  .lean-line-natural {
    grid-column: 2;
    border-top: 1px solid var(--line);
  }
}

@media (max-width: 620px) {
  .mode-explanation,
  .lean-reading-recipe,
  .lean-syntax-glossary {
    grid-template-columns: 1fr;
  }

  .reading-mode-strip,
  .lean-studio-workbench,
  .lean-learning-studio > header {
    padding-left: 1rem;
    padding-right: 1rem;
  }

  .graph-toolbar {
    align-items: flex-start;
    flex-direction: column;
  }
}