α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
⊢ chainHeight (s ∪ t) ≤ chainHeight s + chainHeight t
refine' iSup₂_le fun l hl ↦ _
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
have hl₁ : ↑l₁.length ≤ s.chainHeight := by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
have hl₂ : ↑l₂.length ≤ t.chainHeight := by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ ↑(length l₁) + ↑(length l₂)
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
refine' le_trans _ (add_le_add hl₁ hl₂)
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card (Multiset.filter (fun b => b ∈ s) ↑l + Multiset.filter (fun b => b ∈ t) ↑l))
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ ↑(length l₁) + ↑(length l₂)
simp_rw [← Nat.cast_add, ← Multiset.coe_card, ← Multiset.card_add, ← Multiset.coe_filter]
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card ↑l) + ↑(↑Multiset.card (Multiset.filter (fun a => a ∈ s ∧ a ∈ t) ↑l))

α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ∀ (a : α), a ∈ ↑l → a ∈ s ∨ a ∈ t
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card (Multiset.filter (fun b => b ∈ s) ↑l + Multiset.filter (fun b => b ∈ t) ↑l))
rw [Multiset.filter_add_filter, Multiset.filter_eq_self.mpr, Multiset.card_add, Nat.cast_add]
no goals
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card ↑l) + ↑(↑Multiset.card (Multiset.filter (fun a => a ∈ s ∧ a ∈ t) ↑l))

α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ∀ (a : α), a ∈ ↑l → a ∈ s ∨ a ∈ t
exacts [le_add_right rfl.le, hl.2]
case hl
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ l₁ ∈ subchain s
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑(length l₁) ≤ chainHeight s
apply Set.length_le_chainHeight_of_mem_subchain
no goals
case hl
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ l₁ ∈ subchain s
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
no goals
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
i : α
h : i ∈ l₁
⊢ i ∈ s
simpa using (of_mem_filter h : _)
case hl
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ l₂ ∈ subchain t
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ ↑(length l₂) ≤ chainHeight t
apply Set.length_le_chainHeight_of_mem_subchain
no goals
case hl
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ l₂ ∈ subchain t
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
no goals
α : Type u_1
β : Type ?u.37990
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
i : α
h : i ∈ l₂
⊢ i ∈ t
simpa using (of_mem_filter h : _)