Theorem: RedLt_wf (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ WellFounded MultisetRedLt
Tactic:
constructor
State after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ ∀ (a : Multiset α), Acc MultisetRedLt a

State before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ ∀ (a : Multiset α), Acc MultisetRedLt a
Tactic:
intros a
State after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ Acc MultisetRedLt a

State before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ Acc MultisetRedLt a
Tactic:
apply mred_acc
State after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ ∀ x ∈ a, Acc LT.lt x

State before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ ∀ x ∈ a, Acc LT.lt x
Tactic:
intros x _
State after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ Acc LT.lt x

State before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ Acc LT.lt x
Tactic:
apply wf_lt.induction x
State after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ ∀ (x : α), (∀ y < x, Acc LT.lt y) → Acc LT.lt x

State before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ ∀ (x : α), (∀ y < x, Acc LT.lt y) → Acc LT.lt x
Tactic:
intros y h
State after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ Acc LT.lt y

State before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ Acc LT.lt y
Tactic:
apply Acc.intro y
State after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ ∀ y_1 < y, Acc LT.lt y_1

State before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ ∀ y_1 < y, Acc LT.lt y_1
Tactic:
assumption
State after:
no goals