theorem proved term proof

`top_up_equal_Z`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  62theorem top_up_equal_Z : ZOf .u = ZOf .t := by

Term-mode proof.

  63  obtain ⟨hu, _, ht⟩ := ZOf_up_quarks
  64  rw [hu, ht]
  65

Lean names referenced from this declaration's body.