theorem
proved
tactic proof
oneBitDiff_snocBit_same
show as:
view Lean formalization →
formal statement (Lean)
123private theorem oneBitDiff_snocBit_same {d : Nat} {p q : Pattern d} (b : Bool) :
124 OneBitDiff p q → OneBitDiff (snocBit p b) (snocBit q b) := by
proof body
Tactic-mode proof.
125 intro h
126 classical
127 rcases h with ⟨k, hk, hkuniq⟩
128 refine ⟨k.castSucc, ?_, ?_⟩
129 · simpa using hk
130 · intro j hj
131 -- any differing coordinate cannot be the new last coordinate (since it is fixed to `b`)
132 induction j using Fin.lastCases with
133 | last =>
134 have : False := by
135 simpa [snocBit] using hj
136 exact this.elim
137 | cast j =>
138 have hj' : p j ≠ q j := by
139 simpa [snocBit] using hj
140 have : j = k := hkuniq j hj'
141 simpa [this]
142