theorem
proved
tactic proof
realizationLift_unique_fun
show as:
view Lean formalization →
formal statement (Lean)
150private theorem realizationLift_unique_fun (R : LogicRealization) (B : PeanoObject)
151 (f : PeanoObject.Hom (realizationPeano R) B) :
152 f.toFun = (realizationLift R B).toFun := by
proof body
Tactic-mode proof.
153 funext n
154 have hlogic :
155 (f.toFun ∘ R.orbitEquivLogicNat.symm) =
156 (logicNatLift B).toFun := by
157 exact logicNatLift_unique_fun B
158 { toFun := f.toFun ∘ R.orbitEquivLogicNat.symm
159 map_zero := by
160 simp [Function.comp_def]
161 have hz := f.map_zero
162 have hsymm0 : R.orbitEquivLogicNat.symm LogicNat.zero = R.orbitZero := by
163 apply R.orbitEquivLogicNat.injective
164 simp [R.orbitEquiv_zero]
165 change f.toFun (R.orbitEquivLogicNat.symm LogicNat.zero) = B.zero
166 rw [hsymm0]
167 exact hz
168 map_step := by
169 intro k
170 simp [Function.comp_def]
171 change f.toFun (R.orbitEquivLogicNat.symm (LogicNat.succ k)) =
172 B.step (f.toFun (R.orbitEquivLogicNat.symm k))
173 have hstep_symm :
174 R.orbitEquivLogicNat.symm (LogicNat.succ k) =
175 R.orbitStep (R.orbitEquivLogicNat.symm k) := by
176 apply R.orbitEquivLogicNat.injective
177 rw [R.orbitEquiv_step]
178 simp
179 rw [hstep_symm]
180 simpa [realizationPeano] using f.map_step (R.orbitEquivLogicNat.symm k) }
181 have hn : R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat n) = n := by simp
182 calc
183 f.toFun n = (f.toFun ∘ R.orbitEquivLogicNat.symm) (R.orbitEquivLogicNat n) := by
184 simp [Function.comp_def, hn]
185 _ = (logicNatLift B).toFun (R.orbitEquivLogicNat n) := by rw [hlogic]
186 _ = (realizationLift R B).toFun n := rfl
187
188/-- The extracted realization orbit is initial. -/