theorem
proved
tactic proof
brgcPath_injective
show as:
view Lean formalization →
formal statement (Lean)
72theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
73 | 0 => by
74 intro i j _
75 -- `Fin 1` is a subsingleton (only `0`)
76 simpa [Fin.eq_zero i, Fin.eq_zero j]
77 | (d + 1) => by
78 intro i j hij
79 -- unfold the `d+1` definition and reduce to injectivity of the appended halves
80 classical
81 let T : Nat := 2 ^ d
proof body
Tactic-mode proof.
82 have hTT : 2 ^ (d + 1) = T + T := by
83 simpa [T, twoPow_succ_eq_add d]
84 let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
85 let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
86 have hij' :
87 Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
88 simpa [brgcPath, T, hTT, left, right] using hij
89
90 have hleft_inj : Function.Injective left := by
91 intro a b hab
92 have hab' : brgcPath d a = brgcPath d b := by
93 funext k
94 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
95 simpa [left, snocBit] using this
96 exact (brgcPath_injective d) hab'
97
98 have hright_inj : Function.Injective right := by
99 intro a b hab
100 have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
101 funext k
102 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
103 simpa [right, snocBit] using this
104 have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
105 exact Fin.rev_injective this
106
107 have hdis : ∀ a b : Fin T, left a ≠ right b := by
108 intro a b hab
109 have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
110 -- last coordinate is the appended bit: false on left, true on right
111 simpa [left, right] using this
112
113 have happ_inj : Function.Injective (Fin.append left right) :=
114 (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩
115
116 have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
117 -- cast back along the inverse equality
118 have := congrArg (Fin.cast hTT.symm) hcast
119 simpa [hTT] using this
120
121/-! ## One-bit adjacency -/
122