case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0

case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
hs : ∀ (a : α), a ∈ s → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) s
induction s using Multiset.induction
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0

case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
no goals
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
case cons a s ihs =>
  rw [← s.singleton_add a]
  rw [forall_mem_cons] at hs
  exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)
rw [← s.singleton_add a]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ (x : α), x ∈ s → Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
rw [forall_mem_cons] at hs
no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ (x : α), x ∈ s → Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)