[GOAL]
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
⊢ CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) ↑toFinsupp
[PROOFSTEP]
rintro s t ⟨u, a, hr, he⟩
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ u → r a' a
he : s + {a} = t + u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
replace hr := fun a' ↦ mt (hr a')
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
classical
refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
· apply_fun count b at he 
  simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)] using he
· apply_fun count a at he 
  simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)), add_zero] at he 
  exact he ▸ Nat.lt_succ_self _
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
refine ⟨a, fun b h ↦ ?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
⊢ ↑(↑toFinsupp s) b = ↑(↑toFinsupp t) b
[PROOFSTEP]
simp_rw [toFinsupp_apply]
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ (fun {i} x x_1 => x < x_1) (↑(↑toFinsupp s) a) (↑(↑toFinsupp t) a)
[PROOFSTEP]
simp_rw [toFinsupp_apply]
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
⊢ count b s = count b t
[PROOFSTEP]
apply_fun count b at he 
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t
[PROOFSTEP]
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)] using he
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ count a s < count a t
[PROOFSTEP]
apply_fun count a at he 
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
he : count a (s + {a}) = count a (t + u)
⊢ count a s < count a t
[PROOFSTEP]
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)), add_zero] at he 
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
he : count a s + 1 = count a t
⊢ count a s < count a t
[PROOFSTEP]
exact he ▸ Nat.lt_succ_self _
[GOAL]
α : Type u_1
r : α → α → Prop
x' x : α
h✝ : r x' x
a : α
h : a ∈ {x'}
⊢ r a x
[PROOFSTEP]
rwa [mem_singleton.1 h]
[GOAL]
α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹
[PROOFSTEP]
rw [add_assoc, add_assoc, add_left_cancel_iff]
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [CutExpand, add_singleton_eq_iff]
[GOAL]
α : 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
[PROOFSTEP]
refine' exists₂_congr fun t a ↦ ⟨_, _⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨ht, ha, rfl⟩
[GOAL]
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
[PROOFSTEP]
obtain h | h := mem_add.1 ha
[GOAL]
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
[PROOFSTEP]
exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
[GOAL]
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
[PROOFSTEP]
rintro ⟨ht, h, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
[PROOFSTEP]
classical
rw [cutExpand_iff]
rintro ⟨_, _, _, ⟨⟩, _⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
[PROOFSTEP]
rw [cutExpand_iff]
[GOAL]
α : 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
[PROOFSTEP]
rintro ⟨_, _, _, ⟨⟩, _⟩
[GOAL]
α : Type u_1
r✝ r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s => s.fst + s.snd
[PROOFSTEP]
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = (fun s => s.fst + s.snd) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.fst + s.snd) a' = s
[PROOFSTEP]
dsimp at he ⊢
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
classical
  -- Porting note: Originally `obtain ⟨ha, rfl⟩`
    -- This is https://github.com/leanprover/std4/issues/62
obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
rw [hb]
rw [add_assoc, mem_add] at ha 
obtain h | h := ha
· refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
  · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
  · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
· refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
  · rw [add_comm, singleton_add, cons_erase h]
  · rw [add_assoc, erase_add_right_pos _ h]
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
rw [hb]
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc, mem_add] at ha 
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ ∨ a ∈ s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
obtain h | h := ha
[GOAL]
case mk.intro.intro.intro.intro.inl
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
[GOAL]
case mk.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ erase s₁ a + t + {a} = s₁ + t
[PROOFSTEP]
rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
[GOAL]
case mk.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ (erase s₁ a + t, s₂).fst + (erase s₁ a + t, s₂).snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
[GOAL]
case mk.intro.intro.intro.intro.inr
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
[GOAL]
case mk.intro.intro.intro.intro.inr.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ erase (s₂ + t) a + {a} = s₂ + t
[PROOFSTEP]
rw [add_comm, singleton_add, cons_erase h]
[GOAL]
case mk.intro.intro.intro.intro.inr.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ (s₁, erase (s₂ + t) a).fst + (s₁, erase (s₂ + t) a).snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc, erase_add_right_pos _ h]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
hs : ∀ (a : α), a ∈ s → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) s
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
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✝)
[PROOFSTEP]
case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
[PROOFSTEP]
case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
[PROOFSTEP]
exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
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✝)
[PROOFSTEP]
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)
[GOAL]
α : 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)
[PROOFSTEP]
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)
[GOAL]
α : 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)
[PROOFSTEP]
rw [← s.singleton_add a]
[GOAL]
α : 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)
[PROOFSTEP]
rw [forall_mem_cons] at hs 
[GOAL]
α : 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)
[PROOFSTEP]
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
hacc : Acc r a
⊢ Acc (CutExpand r) {a}
[PROOFSTEP]
induction' hacc with a h ih
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) {a}
[PROOFSTEP]
refine' Acc.intro _ fun s ↦ _
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
[PROOFSTEP]
classical
simp only [cutExpand_iff, mem_singleton]
rintro ⟨t, a, hr, rfl, rfl⟩
refine' acc_of_singleton fun a' ↦ _
rw [erase_singleton, zero_add]
exact ih a' ∘ hr a'
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
[PROOFSTEP]
simp only [cutExpand_iff, mem_singleton]
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ (∃ t a_1, (∀ (a' : α), a' ∈ t → r a' a_1) ∧ a_1 = a ∧ s = erase {a} a_1 + t) → Acc (CutExpand r) s
[PROOFSTEP]
rintro ⟨t, a, hr, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) (erase {a} a + t)
[PROOFSTEP]
refine' acc_of_singleton fun a' ↦ _
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ erase {a} a + t → Acc (CutExpand r) {a'}
[PROOFSTEP]
rw [erase_singleton, zero_add]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}
[PROOFSTEP]
exact ih a' ∘ hr a'
