Theorem: mord_wf_1 (Pdl/MultisetOrder.lean)

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
⊢ AccM_1 (a ::ₘ M0)
Tactic:
constructor
State after:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
⊢ ∀ (y : Multiset α), MultisetRedLt y (a ::ₘ M0) → Acc MultisetRedLt y

State before:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
⊢ ∀ (y : Multiset α), MultisetRedLt y (a ::ₘ M0) → Acc MultisetRedLt y
Tactic:
intros N N_lt
State after:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
⊢ Acc MultisetRedLt N

State before:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
⊢ Acc MultisetRedLt N
Tactic:
change AccM_1 N
State after:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
⊢ AccM_1 N

State before:
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
⊢ AccM_1 N
Tactic:
rcases (red_insert N_lt) with ⟨x, H, H0⟩
State after:
case h.intro.inl.intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = a ::ₘ x
H0 : MultisetRedLt x M0
⊢ AccM_1 N

case h.intro.inr
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
h✝ : N = M0 + x ∧ ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
h : N = M0 + x ∧ ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N
Tactic:
case h.intro.inr h =>
  rcases h with ⟨H, H0⟩
  rw [H]
  clear H induction x using Multiset.induction with
  | empty =>
    simpa
  | cons h =>
    simp_all only [Multiset.mem_cons, or_true, implies_true, true_implies, forall_eq_or_imp, Multiset.add_cons]
State after:
no goals

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = a ::ₘ x
H0 : MultisetRedLt x M0
⊢ AccM_1 N
Tactic:
case h.intro.inl.intro =>
  simp_all
State after:
no goals

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
h : N = M0 + x ∧ ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N
Tactic:
rcases h with ⟨H, H0⟩
State after:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = M0 + x
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N

State before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = M0 + x
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N
Tactic:
rw [H]
State after:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = M0 + x
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 (M0 + x)

State before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = M0 + x
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 (M0 + x)
Tactic:
clear H
State after:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 (M0 + x)

State before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H0 : ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 (M0 + x)
Tactic:
induction x using Multiset.induction with
| empty =>
  simpa
| cons h =>
  simp_all only [Multiset.mem_cons, or_true, implies_true, true_implies, forall_eq_or_imp, Multiset.add_cons]
State after:
no goals

State before:
case intro.empty
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
H0 : ∀ x ∈ 0, x < a
⊢ AccM_1 (M0 + 0)
Tactic:
simpa
State after:
no goals

State before:
case intro.cons
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
h : α
s✝ : Multiset α
a✝ : (∀ x ∈ s✝, x < a) → AccM_1 (M0 + s✝)
H0 : ∀ x ∈ h ::ₘ s✝, x < a
⊢ AccM_1 (M0 + h ::ₘ s✝)
Tactic:
simp_all only [Multiset.mem_cons, or_true, implies_true, true_implies, forall_eq_or_imp, Multiset.add_cons]
State after:
no goals

State before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
H : N = a ::ₘ x
H0 : MultisetRedLt x M0
⊢ AccM_1 N
Tactic:
simp_all
State after:
no goals