Theorem: MultisetLT.iff_MultisetLT' (Pdl/LocalTableau.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ MultisetLT' M N
Tactic:
unfold MultisetLT'
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N → ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ (∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y) → MultisetLT M N

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N → ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
intro M_LT_N
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT_N : MultisetLT M N
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT_N : MultisetLT M N
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
cases M_LT_N
State after:
case mp.MLT
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

State before:
case mp.MLT
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
aesop
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ (∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y) → MultisetLT M N
Tactic:
intro M_LT'_N
State after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT'_N : ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT'_N : ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Tactic:
rcases M_LT'_N with ⟨X,Y,Z,claim⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N

State before:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Tactic:
apply MultisetLT.MLT X Y Z
State after:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ Y ≠ ∅

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ M = Z + X

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ N = Z + Y

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y

State before:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ Y ≠ ∅

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ M = Z + X

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ N = Z + Y

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
all_goals tauto
State after:
no goals

State before:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
tauto
State after:
no goals