Theorem: mord_wf_3 (Pdl/MultisetOrder.lean)

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (a : α), Acc LT.lt a → ∀ (M : Multiset α), AccM_1 M → AccM_1 (a ::ₘ M)
Tactic:
intro w w_a
State after:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w : α
w_a : Acc LT.lt w
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (w ::ₘ M)

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w : α
w_a : Acc LT.lt w
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (w ::ₘ M)
Tactic:
induction w_a with
| intro x _ ih =>
    intro M accM1
    apply @mord_wf_2 α _ _ _ _ _ accM1
    simp_all
State after:
no goals

State before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (x ::ₘ M)
Tactic:
intro M accM1
State after:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ AccM_1 (x ::ₘ M)

State before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ AccM_1 (x ::ₘ M)
Tactic:
apply @mord_wf_2 α _ _ _ _ _ accM1
State after:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ ∀ (b : α) (M : Multiset α), b < x → AccM_1 M → AccM_1 (b ::ₘ M)

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ ∀ (b : α) (M : Multiset α), b < x → AccM_1 M → AccM_1 (b ::ₘ M)
Tactic:
simp_all
State after:
no goals