Theorem: Lt_LT_equiv (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
⊢ MultisetLt = MultisetLT
Tactic:
funext X Y
State after:
case h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y = MultisetLT X Y

State before:
case h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y = MultisetLT X Y
Tactic:
apply propext
State after:
case h.h.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y ↔ MultisetLT X Y

State before:
case h.h.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y ↔ MultisetLT X Y
Tactic:
constructor
State after:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y → MultisetLT X Y

case h.h.a.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLT X Y → MultisetLt X Y

State before:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y → MultisetLT X Y
Tactic:
intros hLt
State after:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
hLt : MultisetLt X Y
⊢ MultisetLT X Y

State before:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
hLt : MultisetLt X Y
⊢ MultisetLT X Y
Tactic:
induction hLt with
| base a b hLt =>
  rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
  use X
  simp
  simp
  assumption
| trans Z W A _ _ aih bih => exact LT_trans _ _ _ bih aih
State after:
no goals

State before:
case h.h.a.mp.base
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y a b : Multiset α
hLt : MultisetRedLt a b
⊢ MultisetLT a b
Tactic:
rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
State after:
case h.h.a.mp.base.RedLt
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ MultisetLT a b

State before:
case h.h.a.mp.base.RedLt
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ MultisetLT a b
Tactic:
use X
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ {y} ≠ ∅

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ {y} ≠ ∅

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Tactic:
simp
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Tactic:
simp
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, x < y

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, x < y
Tactic:
assumption
State after:
no goals

State before:
case h.h.a.mp.trans
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y Z W A : Multiset α
a✝¹ : TC MultisetRedLt Z W
a✝ : TC MultisetRedLt W A
aih : MultisetLT Z W
bih : MultisetLT W A
⊢ MultisetLT Z A
Tactic:
exact LT_trans _ _ _ bih aih
State after:
no goals

State before:
case h.h.a.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLT X Y → MultisetLt X Y
Tactic:
apply direct_subset_red
State after:
no goals