Theorem: Finset.Colex.insert_le_insert (LeanCamCombi/Mathlib/Combinatorics/Colex.lean)

State before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := insert a s } ≤ { ofColex := insert b s } ↔ a ≤ b
Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]
State after:
no goals