internlm/Lean-Github huggingface dataset:
Theorem: LT_trans
Proof state before:
case MLT.MLT.a.x.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
this : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
⊢ Z2 + X2 = X2 + Z2
Tactic:
apply add_comm
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
⊢ Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
Tactic:
have : (X1 + (X2 - Y1)) = (X2 - Y1) + X1 := by rw [add_comm]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
this : X1 + (X2 - Y1) = X2 - Y1 + X1
⊢ Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
this : X1 + (X2 - Y1) = X2 - Y1 + X1
⊢ Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
Tactic:
rw [this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
this : X1 + (X2 - Y1) = X2 - Y1 + X1
⊢ Z1 ∩ Z2 + (X2 - Y1 + X1) = Z1 ∩ Z2 + (X2 - Y1) + X1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
this : X1 + (X2 - Y1) = X2 - Y1 + X1
⊢ Z1 ∩ Z2 + (X2 - Y1 + X1) = Z1 ∩ Z2 + (X2 - Y1) + X1
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
⊢ X1 + (X2 - Y1) = X2 - Y1 + X1
Tactic:
rw [add_comm]
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
case MLT.MLT.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
⊢ ∀ x ∈ Y2 + (Y1 - X2), ∃ y ∈ X1 + (X2 - Y1), x < y
Tactic:
intros y y_in_union
Proof state after:
case MLT.MLT.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
case MLT.MLT.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
if y_in : y ∈ Y2 then
  rcases (Ord2 y y_in) with ⟨x, x_in_X2, y_lt_x⟩
  if x_in : x ∈ Y1 then
    rcases (Ord1 x x_in) with ⟨x', x'_in_X1, x_lt_x'⟩
    use x'
    constructor
    . rw [Multiset.mem_add]
      constructor
      exact x'_in_X1
    . exact lt_trans y_lt_x x_lt_x'
    else
      use x
      constructor
      . rw [add_comm]
        rw [Multiset.mem_add]
        constructor
        apply in_notin_diff
        exact x_in_X2
        exact x_in
      . exact y_lt_x
  else
    have y_in : y ∈ (Y1 - X2) := by aesop
    let h := (Ord1 y)
    have y_in_Y1 : y ∈ Y1 := by
      have : Y1 - X2 ≤ Y1 := by aesop
      apply Multiset.mem_of_le
      exact this
      exact y_in
    let _ := h y_in_Y1
    aesop
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
rcases (Ord2 y y_in) with ⟨x, x_in_X2, y_lt_x⟩
Proof state after:
case intro.intro
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
case intro.intro
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
if x_in : x ∈ Y1 then
  rcases (Ord1 x x_in) with ⟨x', x'_in_X1, x_lt_x'⟩
  use x'
  constructor
  . rw [Multiset.mem_add]
    constructor
    exact x'_in_X1
  . exact lt_trans y_lt_x x_lt_x'
  else
    use x
    constructor
    . rw [add_comm]
      rw [Multiset.mem_add]
      constructor
      apply in_notin_diff
      exact x_in_X2
      exact x_in
    . exact y_lt_x
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
rcases (Ord1 x x_in) with ⟨x', x'_in_X1, x_lt_x'⟩
Proof state after:
case intro.intro
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
case intro.intro
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
use x'
Proof state after:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 + (X2 - Y1) ∧ y < x'
Theorem: LT_trans
Proof state before:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 + (X2 - Y1) ∧ y < x'
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 + (X2 - Y1)

case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ y < x'
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 + (X2 - Y1)

case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ y < x'
Tactic:
. rw [Multiset.mem_add]
  constructor
  exact x'_in_X1
Proof state after:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ y < x'
Theorem: LT_trans
Proof state before:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ y < x'
Tactic:
. exact lt_trans y_lt_x x_lt_x'
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 + (X2 - Y1)
Tactic:
rw [Multiset.mem_add]
Proof state after:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 ∨ x' ∈ X2 - Y1
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 ∨ x' ∈ X2 - Y1
Tactic:
constructor
Proof state after:
case h.left.h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1
Theorem: LT_trans
Proof state before:
case h.left.h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1
Tactic:
exact x'_in_X1
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ y < x'
Tactic:
exact lt_trans y_lt_x x_lt_x'
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
use x
Proof state after:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X1 + (X2 - Y1) ∧ y < x
Theorem: LT_trans
Proof state before:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X1 + (X2 - Y1) ∧ y < x
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X1 + (X2 - Y1)

case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ y < x
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X1 + (X2 - Y1)

case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ y < x
Tactic:
. rw [add_comm]
  rw [Multiset.mem_add]
  constructor
  apply in_notin_diff
  exact x_in_X2
  exact x_in
Proof state after:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ y < x
Theorem: LT_trans
Proof state before:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ y < x
Tactic:
. exact y_lt_x
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X1 + (X2 - Y1)
Tactic:
rw [add_comm]
Proof state after:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1 + X1
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1 + X1
Tactic:
rw [Multiset.mem_add]
Proof state after:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1 ∨ x ∈ X1
Theorem: LT_trans
Proof state before:
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1 ∨ x ∈ X1
Tactic:
constructor
Proof state after:
case h.left.h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1
Theorem: LT_trans
Proof state before:
case h.left.h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2 - Y1
Tactic:
apply in_notin_diff
Proof state after:
case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2

case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∉ Y1