no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
classical
rw [cutExpand_iff]
rintro ⟨_, _, _, ⟨⟩, _⟩
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ 0 ∧ s = erase 0 a + t
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
rw [cutExpand_iff]
no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ 0 ∧ s = erase 0 a + t
rintro ⟨_, _, _, ⟨⟩, _⟩