← Back to lanes · Lane 1 of 6

First Contact

Your first Lean proofs. Definitions. rfl. 4 theorems. Mark each one complete as you work through it — your progress saves to your browser.

Lane 1: 0/4 complete
Theorem 1 of 4 · difficulty 1 · definition / inductive types

depth_of_const

Prove

The depth of a constant-leaf EML tree is zero. A bare constant has no `ceml` operations to count.

introduces: rfl
Informal
Formal — Lean 4
theorem depth_of_const (c : ℂ) : (EMLTree.const c).depth = 0
Starter
theorem depth_of_const (c : ℂ) : (EMLTree.const c).depth = 0 := by
  sorry  -- YOUR PROOF HERE
Mini proof assistant
step 1 of 1
Goal
(c : ℂ) ⊢ (EMLTree.const c).depth = 0
Lane 1 tactics
rflsimpunfoldexact
▸ Proof walkthrough (1 step)
theorem depth_of_const (c : ℂ) : (EMLTree.const c).depth = 0 := rfl
Step 1
rfl

The depth function is defined by pattern matching: `EMLTree.depth (EMLTree.const _) = 0`. Both sides reduce to the literal `0` by computation, so reflexivity closes the goal.

Why this tactic: When two expressions are definitionally equal — i.e. reduce to the same normal form by unfolding definitions — `rfl` is the shortest possible proof. Here both sides reduce to `0` after one unfolding step.

▸ Common mistakes
  • [step 1]Using `simp [EMLTree.depth]` works but is overkill — it loads the simp normalizer when `rfl` already suffices.
  • [step 1]Writing `by decide` fails because `EMLTree.depth` is not a `Decidable` proposition; `decide` is for decidable equality of concrete naturals.
Export to Lean ↓Export to Forge ↓source ↗
Theorem 2 of 4 · difficulty 1 · definition / inductive types

depth_of_var

Prove

The depth of the variable-leaf EML tree is zero. Like a constant, the variable node has no `ceml` operations.

Informal
Formal — Lean 4
theorem depth_of_var : EMLTree.var.depth = 0
Starter
theorem depth_of_var : EMLTree.var.depth = 0 := by
  sorry  -- YOUR PROOF HERE
Mini proof assistant
step 1 of 1
Goal
⊢ EMLTree.var.depth = 0
Lane 1 tactics
rflsimpunfoldexact
▸ Proof walkthrough (1 step)
theorem depth_of_var : EMLTree.var.depth = 0 := rfl
Step 1
rfl

By the inductive definition of `EMLTree.depth`, the `var` constructor has its own pattern equation returning `0`. Both sides of the equation reduce to `0`.

Why this tactic: Same reasoning as `depth_of_const`: pattern matching on a constructor is reduced by `rfl` automatically.

▸ Common mistakes
  • [step 1]Forgetting that `EMLTree.var` takes no arguments and writing `EMLTree.var x` instead — the variable node has no parameter, the variable's *value* enters only at evaluation time.
Export to Lean ↓Export to Forge ↓source ↗
Theorem 3 of 4 · difficulty 1 · definition / depth witness

expTree_depth

Prove

The depth of `expTree` (the explicit `ceml(var, const 1)` representation of `exp(x)`) is exactly 1.

cost class: p1-d1-w0-c0introduces: simp [..]
Informal
Formal — Lean 4
theorem expTree_depth : expTree.depth = 1
Starter
theorem expTree_depth : expTree.depth = 1 := by
  sorry  -- YOUR PROOF HERE
Mini proof assistant
step 1 of 1
Goal
⊢ expTree.depth = 1
Lane 1 tactics
rflsimpunfoldexact
▸ Proof walkthrough (1 step)
theorem expTree_depth : expTree.depth = 1 := by
  simp [expTree, EMLTree.depth]
Step 1
simp [expTree, EMLTree.depth]

Unfold the definition `expTree := ceml var (const 1)`, then unfold `EMLTree.depth` recursively. The `ceml` arm gives `1 + max var.depth (const 1).depth`. Each child has depth 0, and `1 + max 0 0 = 1`.

Why this tactic: `simp` is the right hammer when the proof is a chain of definitional unfoldings followed by a small arithmetic identity. Naming `expTree` and `EMLTree.depth` in the bracket tells `simp` exactly which definitions to unfold; without that, it would not know to expand them.

▸ Common mistakes
  • [step 1]Trying just `rfl` — the recursion through `max` is not consistently reduced automatically and `rfl` may fail.
  • [step 1]Writing `unfold expTree EMLTree.depth` works in some cases but leaves `1 + max 0 0 = 1` un-evaluated; `simp` finishes the arithmetic too.
Export to Lean ↓Export to Forge ↓source ↗depends on: depth_of_const, depth_of_var
Theorem 4 of 4 · difficulty 1 · complex analysis (Mathlib wrapper)

complex_exp_zero_eq_one

Prove

The complex exponential at zero equals one: exp(0) = 1.

cost class: p1-d1-w0-c0introduces: term-mode proof
Informal
Formal — Lean 4
theorem complex_exp_zero_eq_one : Complex.exp 0 = 1
Starter
theorem complex_exp_zero_eq_one : Complex.exp 0 = 1 := by
  sorry  -- YOUR PROOF HERE
Mini proof assistant
step 1 of 1
Goal
⊢ Complex.exp 0 = 1
Lane 1 tactics
rflsimpunfoldexact
▸ Proof walkthrough (1 step)
theorem complex_exp_zero_eq_one : Complex.exp 0 = 1 := Complex.exp_zero
Step 1
Complex.exp_zero

Mathlib already proves this fact under the name `Complex.exp_zero`. Citing the lemma by name is itself a complete proof — Lean accepts a term of the right type without any further tactic block.

Why this tactic: When the result you want is exactly a Mathlib lemma, the cleanest proof is the lemma name as a term. No `by` block is needed; the term mode entry skips the tactic engine entirely.

▸ Common mistakes
  • [step 1]Re-deriving the fact from the power-series definition — slow and fragile when Mathlib already has it.
  • [step 1]Writing `by exact Complex.exp_zero` works but is one needless layer of indirection compared to direct term-mode.
Export to Lean ↓Export to Forge ↓source ↗