chore(CategoryTheory/Presentable): remove a backward.isDefEq set_option - #42984

Open

dennj wants to merge 6 commits into

leanprover-community:masterfrom

dennj:presentable-remove-isdefeq-setoption

Commits on Aug 20, 2026

chore(CategoryTheory/Presentable): remove a backward.isDefEq set_option
dennj
committed
ba4ca91
use aesop with Subtype.ext_iff instead of explicit proof
dennj
committed
8bb7f03
fix membership proof instead of aesop hint
dennj
committed
653422b

Commits on Aug 21, 2026

Update Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

dennj
and
YaelDillies
authored
eecb605
inline rangeFactorization_surjective at use site
dennj
committed
730bf7f
Merge branch 'master' into presentable-remove-isdefeq-setoption
dennj
authored
b67a299