internlm/Lean-Github huggingface dataset:
Theorem: mord_wf_1
Proof 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
Proof 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
Theorem: mord_wf_1
Proof 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
Proof 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
Theorem: mord_wf_1
Proof 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
Proof 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
Theorem: mord_wf_1
Proof 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⟩
Proof 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
Theorem: mord_wf_1
Proof 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]
Proof state after:
no goals
Theorem: mord_wf_1
Proof 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
Proof state after:
no goals
Theorem: mord_wf_1
Proof 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⟩
Proof 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
Theorem: mord_wf_1
Proof 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]
Proof 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)
Theorem: mord_wf_1
Proof 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
Proof 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)
Theorem: mord_wf_1
Proof 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]
Proof state after:
no goals
Theorem: mord_wf_1
Proof 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
Proof state after:
no goals
Theorem: mord_wf_1
Proof 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]
Proof state after:
no goals
Theorem: mord_wf_1
Proof 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
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (a ::ₘ M)
Tactic:
unfold AccM_1
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), Acc MultisetRedLt M → Acc MultisetRedLt (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
⊢ ∀ (M : Multiset α), Acc MultisetRedLt M → Acc MultisetRedLt (a ::ₘ M)
Tactic:
intros M H0
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M : Multiset α
H0 : Acc MultisetRedLt M
⊢ Acc MultisetRedLt (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M : Multiset α
H0 : Acc MultisetRedLt M
⊢ Acc MultisetRedLt (a ::ₘ M)
Tactic:
induction H0 with
| intro x wfH wfH2 =>
  apply mord_wf_1
  . simpa
  . intros b x a
    unfold AccM_1
    apply H
    assumption
  . constructor
    simpa
  . simpa
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Acc MultisetRedLt (a ::ₘ x)
Tactic:
apply mord_wf_1
Proof state after:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α

case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α

case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. simpa
Proof state after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. intros b x a
  unfold AccM_1
  apply H
  assumption
Proof state after:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x

case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. constructor
  simpa
Proof state after:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Theorem: mord_wf_2
Proof state before:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
. simpa
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
case intro.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ Multiset α
Tactic:
simpa
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
Tactic:
intros b x a
Proof state after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ AccM_1 x → AccM_1 (b ::ₘ x)
Theorem: mord_wf_2
Proof state before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ AccM_1 x → AccM_1 (b ::ₘ x)
Tactic:
unfold AccM_1
Proof state after:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ Acc MultisetRedLt x → Acc MultisetRedLt (b ::ₘ x)
Theorem: mord_wf_2
Proof state before:
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ Acc MultisetRedLt x → Acc MultisetRedLt (b ::ₘ x)
Tactic:
apply H
Proof state after:
case intro.H1.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ b < a✝
Theorem: mord_wf_2
Proof state before:
case intro.H1.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ b < a✝
Tactic:
assumption
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
case intro.H2
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ AccM_1 x
Tactic:
constructor
Proof state after:
case intro.H2.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
Theorem: mord_wf_2
Proof state before:
case intro.H2.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
Tactic:
simpa
Proof state after:
no goals
Theorem: mord_wf_2
Proof state before:
case intro.H3
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M x : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x → Acc MultisetRedLt (a ::ₘ y)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)
Tactic:
simpa
Proof state after:
no goals
Theorem: mord_wf_3
Proof 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
Proof 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)
Theorem: mord_wf_3
Proof 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
Proof state after:
no goals
Theorem: mord_wf_3
Proof 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
Proof 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)