Mathlib (2026-09): SetLike.le_def → IsConcreteLE.le_iff (and friends)

Since 2026-09-01 (still a warning-only deprecated alias in v4.35.0 and v4.36.0-rc2), the order lemmas for SetLike-style structures live in the IsConcreteLE class: SetLike.le_def → IsConcreteLE.le_iff (S ≤ T ↔ ∀ ⦃x⦄, x ∈ S → x ∈ T), SetLike.exists_of_lt → IsConcreteLE.exists_of_lt, SetLike.not_le_iff_exists → IsConcreteLE.not_le_iff_exists, SetLike.lt_iff_le_and_exists → IsConcreteLE.lt_iff_le_and_exists, and the instance LE.ofSetLike → LE.ofMembership. For subgroups, both rw [IsConcreteLE.le_iff] and .2 h are drop-in. Often you don't need a lemma at all: for H K : Subgroup G, H ≤ K ↔ ∀ ⦃x⦄, x ∈ H → x ∈ K is Iff.rfl, intro x hx works on a H ≤ K goal, and h hx applies a hypothesis h : H ≤ K. Also renamed on 2026-09-02: Prop.exists_iff → Prop.exists and Prop.forall_iff → Prop.forall.