α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s : Multiset α
⊢ (∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a) ↔
    ∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s : Multiset α
⊢ CutExpand r s' s ↔ ∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
simp_rw [CutExpand, add_singleton_eq_iff]
case refine'_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t

case refine'_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s : Multiset α
⊢ (∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a) ↔
    ∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
refine' exists₂_congr fun t a ↦ ⟨_, _⟩
case refine'_1.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
case refine'_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
rintro ⟨ht, ha, rfl⟩
case refine'_1.intro.intro.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t

case refine'_1.intro.intro.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
case refine'_1.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
obtain h | h := mem_add.1 ha
no goals
case refine'_1.intro.intro.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t

case refine'_1.intro.intro.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
case refine'_2.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ erase s a + t = erase (s + t) a
case refine'_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a
rintro ⟨ht, h, rfl⟩
no goals
case refine'_2.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ erase s a + t = erase (s + t) a
exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩