Theorem: Finset.Colex.cons_le_cons (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 : α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
obtain rfl | hab := eq_or_ne a b
State after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b

State before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
classical
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
 singleton_le_singleton]
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a
Tactic:
simp
State after:
no goals

State before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
 singleton_le_singleton]
State after:
no goals