pith. machine review for the scientific record. sign in
lemma proved tactic proof

OneBitDiff_symm

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  40lemma OneBitDiff_symm {d : Nat} {p q : Pattern d} :
  41    OneBitDiff p q → OneBitDiff q p := by

proof body

Tactic-mode proof.

  42  intro h
  43  rcases h with ⟨k, hk, hkuniq⟩
  44  refine ⟨k, ?_, ?_⟩
  45  · simpa [ne_comm] using hk
  46  · intro k' hk'
  47    -- rewrite hk' as p k' ≠ q k' to use uniqueness
  48    have hk'' : p k' ≠ q k' := by simpa [ne_comm] using hk'
  49    exact hkuniq k' hk''
  50
  51/-! ## The GrayCycle structure (adjacency + wrap-around) -/
  52

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.