Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
import Pretty.Defs.Basic

/-!
## Various lemmas about size of `Doc`

These will be helpful for termination proofs. 
They will be used implicitly, as we mark them with `@[simp]`.
-/

@[simp]
lemma 
Doc.size_choice₁: ∀ {d₁ d₂ : Doc}, size d₁ < size (choice d₁ d₂)
Doc.size_choice₁ : 
Doc.size: Doc → ℕ
Doc.size 
d₁: ?m.4
d₁ < 
Doc.size: Doc → ℕ
Doc.size (
Doc.choice: Doc → Doc → Doc
Doc.choice 
d₁: ?m.4
d₁ 
d₂: ?m.9
d₂) := 
Goals accomplished! 🐙
d₁, d₂: Doc

size d₁ < size (choice d₁ d₂)
Goals accomplished! 🐙


@[simp]
lemma 
Doc.size_choice₂: ∀ {d₂ d₁ : Doc}, size d₂ < size (choice d₁ d₂)
Doc.size_choice₂ : 
Doc.size: Doc → ℕ
Doc.size 
d₂: ?m.1291
d₂ < 
Doc.size: Doc → ℕ
Doc.size (
Doc.choice: Doc → Doc → Doc
Doc.choice 
d₁: ?m.1296
d₁ 
d₂: ?m.1291
d₂) := 
Goals accomplished! 🐙
d₂, d₁: Doc

size d₂ < size (choice d₁ d₂)
Goals accomplished! 🐙


@[simp]
lemma 
Doc.size_align: ∀ {d' : Doc}, size d' < size (align d')
Doc.size_align : 
Doc.size: Doc → ℕ
Doc.size 
d': ?m.1753
d' < 
Doc.size: Doc → ℕ
Doc.size (
Doc.align: Doc → Doc
Doc.align 
d': ?m.1753
d') := 
Goals accomplished! 🐙
d': Doc

size d' < size (align d')
Goals accomplished! 🐙


@[simp]
lemma 
Doc.size_nest: ∀ {d' : Doc} {n : ℕ}, size d' < size (nest n d')
Doc.size_nest : 
Doc.size: Doc → ℕ
Doc.size 
d': ?m.2497
d' < 
Doc.size: Doc → ℕ
Doc.size (
Doc.nest: ℕ → Doc → Doc
Doc.nest 
n: ?m.2502
n 
d': ?m.2497
d') := 
Goals accomplished! 🐙
d': Doc

n: ℕ

size d' < size (nest n d')
Goals accomplished! 🐙


@[simp]
lemma 
Doc.size_concat₁: ∀ {d₁ d₂ : Doc}, size d₁ < size (concat d₁ d₂)
Doc.size_concat₁ : 
d₁: ?m.3255
d₁.
size: Doc → ℕ
size < (
Doc.concat: Doc → Doc → Doc
Doc.concat 
d₁: ?m.3255
d₁ 
d₂: ?m.3263
d₂).
size: Doc → ℕ
size := 
Goals accomplished! 🐙
d₁, d₂: Doc

size d₁ < size (concat d₁ d₂)
Goals accomplished! 🐙


@[simp]
lemma 
Doc.size_concat₂: ∀ {d₁ d₂ : Doc}, size d₂ < size (concat d₁ d₂)
Doc.size_concat₂ : 
d₂: ?m.3734
d₂.
size: Doc → ℕ
size < (
Doc.concat: Doc → Doc → Doc
Doc.concat 
d₁: ?m.3727
d₁ 
d₂: ?m.3734
d₂).
size: Doc → ℕ
size := 
Goals accomplished! 🐙
d₁, d₂: Doc

size d₂ < size (concat d₁ d₂)
Goals accomplished! 🐙