 151  -- injective + card equality ⇒ bijective
 152  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩
 153
 154theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
 155  (grayCycle3_bijective).2
 156
 157theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
 158  intro i
 159  -- 8 explicit cases; each step flips exactly one of the three bits.
 160  fin_cases i
 161  · -- 0 -> 1 (flip bit 0)
 162    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 163    · simp [grayCycle3Path, gray8At, pattern3]
 164    · intro k hk
 165      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 166  · -- 1 -> 3 (flip bit 1)
 167    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
 168    · simp [grayCycle3Path, gray8At, pattern3]
 169    · intro k hk
 170      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 171  · -- 2 -> 3?  (i=2 means gray8At 2 = 3, next is gray8At 3 = 2; flip bit 0)
 172    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 173    · simp [grayCycle3Path, gray8At, pattern3]
 174    · intro k hk
 175      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 176  · -- i=3: 2 -> 6 (flip bit 2)
 177    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
 178    · simp [grayCycle3Path, gray8At, pattern3]
 179    · intro k hk
 180      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 181  · -- i=4: 6 -> 7 (flip bit 0)
 182    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 183    · simp [grayCycle3Path, gray8At, pattern3]
 184    · intro k hk

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.