Commit 2025-06-04 12:09 391de5f9

View on Github →

chore(Topology): remove @[simp] when simp can prove, improve SNF (#25419) Found by the incoming improvements to the simpNF linter. Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simpNF.20lint.20with.20hyps/with/522275029

Estimated changes

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

modified theorem Pretrivialization.coe_coe_fst

Modified Mathlib/Topology/VectorBundle/Basic.lean

modified theorem VectorBundleCore.localTriv_continuousLinearMapAt

modified theorem VectorBundleCore.localTriv_coordChange_eq

modified theorem VectorBundleCore.localTriv_symmL

modified theorem VectorBundleCore.localTriv_symm_apply

Modified Mathlib/Topology/VectorBundle/Constructions.lean