index(transpose) = -index for Fredholm maps in Lean via FredholmPackage, no Hahn–Banach

Mathlib's IsFredholm.nonempty_fredholmPackage gives topological splittings X = X₁ ⊕ X₀ (X₀ = ker T, pkg.ker_eq) and Y = Y₁ ⊕ Y₀ (Y₁ = range T, pkg.range_eq), with T = Y₁.subtypeL ∘L equiv ∘L decDom.proj. With these, the transpose Tᵗ = (compL 𝕜 X Y 𝕜).flip T (so Tᵗ f = f ∘L T by rfl) needs no extension theorem. Define restriction p.restrictDual f := f ∘L p.subtypeL (a LinearMap; map_add'/map_smul' are rfl). Two generic lemmas for IsTopCompl p q: (a) restrictDual is surjective via g ∘L p.projectionOntoL q h, so codim ker = dim p; (b) ker(restrictDual p) ≃ StrongDual q via restriction (inverse g ∘L q.projectionOntoL p h.symm). Use finrank (StrongDual 𝕜 V) = finrank V from LinearMap.toContinuousLinearMap.finrank_eq.symm.trans Subspace.dual_finrank_eq. Then ker Tᵗ = ann(Y₁) and range Tᵗ = ann(X₀). For the latter, the preimage is g ∘ X₁.subtypeL ∘ equiv.symm ∘ decCodom.proj, and x - proj x ∈ X₀ follows from projectionOntoL_apply_eq_zero_iff, projectionOntoL_apply_left. Transport finranks across equal submodules with Submodule.quotEquivOfEq. It works for normed (not necessarily complete) spaces over RCLike.