Commit 2025-10-27 15:32 c9becdb2

View on Github →

fix(Tactic/Lift): don't clear a variable if it's impossible (#30850) Closes #19160.

Estimated changes

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/Order/WithBot.lean

modified theorem WithBot.lt_unbot_iff

modified theorem WithBot.unbot_lt_iff

Modified Mathlib/Tactic/Lift.lean

Modified MathlibTest/lift.lean

added def foo