pattern3_injective

formal source

 123  -- Only 8 cases; compute directly.
 124  fin_cases w <;> decide
 125
 126theorem pattern3_injective : Function.Injective pattern3 := by
 127  intro a b hab
 128  apply Fin.ext
 129  have hNat : toNat3 (pattern3 a) = toNat3 (pattern3 b) := congrArg toNat3 hab
 130  simpa [toNat3_pattern3] using hNat
 131
 132theorem grayCycle3_injective : Function.Injective grayCycle3Path := by
 133  intro i j hij
 134  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
 135  exact gray8At_injective h0
 136
 137theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
 138  classical
 139  -- card(Fin 8) = 8
 140  have hFin : Fintype.card (Fin 8) = 8 := by simp
 141  -- card(Pattern 3) = 2^3 = 8
 142  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
 143    simpa using (Patterns.card_pattern 3)
 144  have hPow : (2 ^ 3 : Nat) = 8 := by decide
 145  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
 146  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
 147    -- rewrite both sides to 8
 148    calc
 149      Fintype.card (Fin 8) = 8 := hFin
 150      _ = Fintype.card (Pattern 3) := by simpa [hPat]
 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