-- Mathlib/Logic/Hydra.lean
theorem _root_.Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) {a}

Proof state:
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}

Tactic:
refine Acc.intro _ fun s ↦ ?_

Result:
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

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ 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'}

Tactic:
exact ih a' ∘ hr a'

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ 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) ({a}.erase a + t)

Tactic:
refine acc_of_singleton fun a' ↦ ?_

Result:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ {a}.erase a + t → Acc (CutExpand r) {a'}

Proof state:
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

Tactic:
simp only [cutExpand_iff, mem_singleton]

Result:
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' ∈ t, r a' a_1) ∧ a_1 = a ∧ s = {a}.erase a_1 + t) → Acc (CutExpand r) s

Proof state:
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

Tactic:
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'

Result:
no goals

Proof state:
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' ∈ t, r a' a_1) ∧ a_1 = a ∧ s = {a}.erase a_1 + t) → Acc (CutExpand r) s

Tactic:
rintro ⟨t, a, hr, rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ 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) ({a}.erase a + t)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
hacc : Acc r a
⊢ Acc (CutExpand r) {a}

Tactic:
induction' hacc with a h ih

Result:
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}

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ {a}.erase a + t → Acc (CutExpand r) {a'}

Tactic:
rw [erase_singleton, zero_add]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ 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'}