realizationLift_unique_fun

formal source

 147    rw [R.orbitEquiv_step]
 148    rfl
 149
 150private theorem realizationLift_unique_fun (R : LogicRealization) (B : PeanoObject)
 151    (f : PeanoObject.Hom (realizationPeano R) B) :
 152    f.toFun = (realizationLift R B).toFun := by
 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) }