-- Mathlib/Order/Height.lean
theorem chainHeight_union_le : (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
i : α
h : i ∈ l₂
⊢ i ∈ t

Tactic:
simpa using (of_mem_filter h :)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
⊢ ↑l₂.length ≤ t.chainHeight

Tactic:
apply Set.length_le_chainHeight_of_mem_subchain

Result:
case hl
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
⊢ l₂ ∈ t.subchain

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Tactic:
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 :)⟩

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Tactic:
refine le_trans ?_ (add_le_add hl₁ hl₂)

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑l.length ≤ ↑l₁.length + ↑l₂.length

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑l.length ≤ ↑l₁.length + ↑l₂.length

Tactic:
simp_rw [l₁, l₂, ← Nat.cast_add, ← Multiset.coe_card, ← Multiset.card_add,
  ← Multiset.filter_coe]

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑(↑l).card ≤ ↑(Multiset.filter (Membership.mem s) ↑l + Multiset.filter (Membership.mem t) ↑l).card

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Tactic:
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 :)⟩

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
⊢ (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight

Tactic:
refine iSup₂_le fun l hl ↦ ?_

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
⊢ ↑l.length ≤ s.chainHeight + t.chainHeight

Proof state:
case hl
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
⊢ l₂ ∈ t.subchain

Tactic:
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h :)⟩

Result:
no goals

Proof state:
case hl
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ l₁ ∈ s.subchain

Tactic:
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h :)⟩

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑(↑l).card ≤ ↑(Multiset.filter (Membership.mem s) ↑l + Multiset.filter (Membership.mem t) ↑l).card

Tactic:
rw [Multiset.filter_add_filter, Multiset.filter_eq_self.mpr, Multiset.card_add, Nat.cast_add]

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑(↑l).card ≤ ↑(↑l).card + ↑(Multiset.filter (fun a => a ∈ s ∧ a ∈ t) ↑l).card

α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ∀ a ∈ ↑l, a ∈ s ∨ a ∈ t

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
i : α
h : i ∈ l₁
⊢ i ∈ s

Tactic:
simpa using (of_mem_filter h :)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑l₁.length ≤ s.chainHeight

Tactic:
apply Set.length_le_chainHeight_of_mem_subchain

Result:
case hl
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ l₁ ∈ s.subchain

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ↑(↑l).card ≤ ↑(↑l).card + ↑(Multiset.filter (fun a => a ∈ s ∧ a ∈ t) ↑l).card

α : Type u_1
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ (s ∪ t).subchain
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑l₁.length ≤ s.chainHeight
hl₂ : ↑l₂.length ≤ t.chainHeight
⊢ ∀ a ∈ ↑l, a ∈ s ∨ a ∈ t

Tactic:
exacts [le_add_right rfl.le, hl.2]

Result:
no goals