Theorem: mred_acc (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M : Multiset α), (∀ x ∈ M, Acc LT.lt x) → AccM_1 M
Tactic:
intros M wf_el
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M
Tactic:
induction M using Multiset.induction_on with | empty =>
  constructor
  intro y y_lt
  absurd y_lt
  apply not_MultisetRedLt_0
| cons _ _ ih =>
  apply mord_wf_3
  . assumption
  . apply wf_el
    simp_all
  . apply ih
    intros
    apply wf_el
    simp_all
State after:
no goals

State before:
case empty
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ AccM_1 0
Tactic:
constructor
State after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), MultisetRedLt y 0 → Acc MultisetRedLt y

State before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), MultisetRedLt y 0 → Acc MultisetRedLt y
Tactic:
intro y y_lt
State after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ Acc MultisetRedLt y

State before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ Acc MultisetRedLt y
Tactic:
absurd y_lt
State after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ ¬MultisetRedLt y 0

State before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ ¬MultisetRedLt y 0
Tactic:
apply not_MultisetRedLt_0
State after:
no goals

State before:
case cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 (a✝ ::ₘ s✝)
Tactic:
apply mord_wf_3
State after:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝

State before:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. assumption
State after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. apply wf_el
  simp_all
State after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. apply ih
  intros
  apply wf_el
  simp_all
State after:
no goals

State before:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α
Tactic:
assumption
State after:
no goals

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝
Tactic:
apply wf_el
State after:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ a✝ ∈ a✝ ::ₘ s✝

State before:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ a✝ ∈ a✝ ::ₘ s✝
Tactic:
simp_all
State after:
no goals

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
apply ih
State after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ ∀ x ∈ s✝, Acc LT.lt x

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ ∀ x ∈ s✝, Acc LT.lt x
Tactic:
intros
State after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ Acc LT.lt x✝

State before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ Acc LT.lt x✝
Tactic:
apply wf_el
State after:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ x✝ ∈ a✝¹ ::ₘ s✝

State before:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ x✝ ∈ a✝¹ ::ₘ s✝
Tactic:
simp_all
State after:
no goals