Commit 2025-09-21 18:06 409aebc0

View on Github →

chore: reduce open Fin.NatCast (#29840) Removing the type cast to Fin allowed me to golf IsPathConnected.exists_path_through_family.

Estimated changes

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/Path.lean

added theorem Path.bijective_cast

added theorem Path.exists_congr

added theorem Path.source_mem_range

added theorem Path.target_mem_range