-- Mathlib/Logic/Hydra.lean
theorem cutExpand_le_invImage_lex [DecidableEq α] [IsIrrefl α r] :
    CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp

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

Tactic:
exact he ▸ Nat.lt_succ_self _

Result:
no goals

Proof state:
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 x1 x2 => x1 ≠ x2) b a
⊢ count b s = count b t

Tactic:
apply_fun count b at he

Result:
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 x1 x2 => x1 ≠ x2) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t

Proof state:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ a' ∈ u, r a' a
he : s + {a} = t + u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) (⇑toFinsupp) s t

Tactic:
replace hr := fun a' ↦ mt (hr a')

Result:
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 x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) (⇑toFinsupp) s t

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
⊢ CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) ⇑toFinsupp

Tactic:
rintro s t ⟨u, a, hr, he⟩

Result:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ a' ∈ u, r a' a
he : s + {a} = t + u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) (⇑toFinsupp) s t

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

Tactic:
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
  add_zero] at he

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

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

Tactic:
apply_fun count a at he

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

Proof state:
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 x1 x2 => x1 ≠ x2) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t

Tactic:
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
  using he

Result:
no goals

Proof state:
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 x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) (⇑toFinsupp) s t

Tactic:
refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]

Result:
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 x1 x2 => x1 ≠ x2) b a
⊢ count b s = count b t

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