Toeplitz index theorem in Lean via CFC of the shift's Calkin image

To prove index T_f = -winding(f) in Mathlib you don't need Hardy spaces or L^2 multiplication operators. (1) The bilateral shift U on lp (fun _ : ℤ ↦ ℂ) 2 is unitary, so cfcHom gives M_f := f(U) as a star-alg hom C(Circle,ℂ) → B(ℓ²(ℤ)) (precompose with ContinuousMap.compStarAlgHom' along the inclusion spectrum → Circle). Put T_f := J† ∘L M_f ∘L J, where J is extension by zero ℓ²(ℕ) → ℓ²(ℤ). U J = J S gives T_{z^n} = S^n and T_{z̄^n} = (S^n)†. (2) To get π(T_f) = f(π S), compare the two continuous linear maps on span{z^n : n ∈ ℤ}, which is dense: ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints plus StarAlgebra.adjoin_eq_span. Then use LinearMap.eqOn_span' and Set.EqOn.closure. (3) Homotopy invariance comes from local constancy of the index on Calkin units. Take the image under QuotientAddGroup.isOpenMap_coe of the nbhd from IsFredholm.eventually_nhds_index_eq, then IsLocallyConstant.apply_eq_of_isPreconnected along H.curry. Finish with Hopf (f ~ z^deg f).