internlm/Lean-Github huggingface dataset:
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
⊢ P = Z1 ∩ Z2 + (Y2 + (Y1 - X2))

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
⊢ M = Z1 ∩ Z2 + (X1 + (X2 - Y1))

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:
. rw [P2_def]
  have : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2 := by
    have : (Y2 + (Y1 - X2)) = (Y1 - X2) + Y2 := by rw [add_comm]
    rw [this]
    rw [add_assoc]
  rw [this]
  apply meq_union_meq_reverse
  have : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2) := by
    rw [Multiset.inter_comm]
  rw [this]
  rw [← double_split]
  rw [add_comm]
  rw [← N2_def]
  rw [N1_def]
  apply add_comm
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
⊢ M = Z1 ∩ Z2 + (X1 + (X2 - Y1))

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
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
⊢ M = Z1 ∩ Z2 + (X1 + (X2 - Y1))

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:
. rw [M1_def]
  have : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1 := by
    have : (X1 + (X2 - Y1)) = (X2 - Y1) + X1 := by rw [add_comm]
    rw [this]
    rw [add_assoc]
  rw [this]
  apply meq_union_meq_reverse
  apply double_split
  rw [add_comm]
  rw [← N1_def]
  rw [N2_def]
  apply add_comm
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
⊢ ∀ x ∈ Y2 + (Y1 - X2), ∃ y ∈ X1 + (X2 - Y1), x < y
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
  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:
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
⊢ X1 + (X2 - Y1) ≠ ∅
Tactic:
aesop
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
⊢ P = Z1 ∩ Z2 + (Y2 + (Y1 - X2))
Tactic:
rw [P2_def]
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
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y2 + (Y1 - X2))
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
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y2 + (Y1 - X2))
Tactic:
have : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2 := by
  have : (Y2 + (Y1 - X2)) = (Y1 - X2) + Y2 := by rw [add_comm]
  rw [this]
  rw [add_assoc]
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
this : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y2 + (Y1 - X2))
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
this : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y2 + (Y1 - X2))
Tactic:
rw [this]
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
this : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y1 - X2) + Y2
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
this : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 + Y2 = Z1 ∩ Z2 + (Y1 - X2) + Y2
Tactic:
apply meq_union_meq_reverse
Proof state after:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 = Z1 ∩ Z2 + (Y1 - X2)
Theorem: LT_trans
Proof state before:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z2 = Z1 ∩ Z2 + (Y1 - X2)
Tactic:
have : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2) := by
  rw [Multiset.inter_comm]
Proof state after:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 = Z1 ∩ Z2 + (Y1 - X2)
Theorem: LT_trans
Proof state before:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 = Z1 ∩ Z2 + (Y1 - X2)
Tactic:
rw [this]
Proof state after:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 = Z2 ∩ Z1 + (Y1 - X2)
Theorem: LT_trans
Proof state before:
case MLT.MLT.a.x
α : 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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 = Z2 ∩ Z1 + (Y1 - X2)
Tactic:
rw [← double_split]
Proof state after:
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ X2 + Z2 = Y1 + Z1
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ X2 + Z2 = Y1 + Z1
Tactic:
rw [add_comm]
Proof state after:
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 + X2 = Y1 + Z1
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z2 + X2 = Y1 + Z1
Tactic:
rw [← N2_def]
Proof state after:
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ N = Y1 + Z1
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ N = Y1 + Z1
Tactic:
rw [N1_def]
Proof state after:
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z1 + Y1 = Y1 + Z1
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z1 + Y1 = Y1 + Z1
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 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
Tactic:
have : (Y2 + (Y1 - X2)) = (Y1 - X2) + Y2 := 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 : Y2 + (Y1 - X2) = Y1 - X2 + Y2
⊢ Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
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 : Y2 + (Y1 - X2) = Y1 - X2 + Y2
⊢ Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
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 : Y2 + (Y1 - X2) = Y1 - X2 + Y2
⊢ Z1 ∩ Z2 + (Y1 - X2 + Y2) = Z1 ∩ Z2 + (Y1 - X2) + Y2
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 : Y2 + (Y1 - X2) = Y1 - X2 + Y2
⊢ Z1 ∩ Z2 + (Y1 - X2 + Y2) = Z1 ∩ Z2 + (Y1 - X2) + Y2
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
⊢ Y2 + (Y1 - X2) = Y1 - X2 + Y2
Tactic:
rw [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
this : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
⊢ Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
Tactic:
rw [Multiset.inter_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
⊢ M = Z1 ∩ Z2 + (X1 + (X2 - Y1))
Tactic:
rw [M1_def]
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
⊢ Z1 + X1 = Z1 ∩ Z2 + (X1 + (X2 - Y1))
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
⊢ Z1 + X1 = Z1 ∩ Z2 + (X1 + (X2 - Y1))
Tactic:
have : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1 := by
  have : (X1 + (X2 - Y1)) = (X2 - Y1) + X1 := by rw [add_comm]
  rw [this]
  rw [add_assoc]
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
this : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
⊢ Z1 + X1 = Z1 ∩ Z2 + (X1 + (X2 - Y1))
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
this : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
⊢ Z1 + X1 = Z1 ∩ Z2 + (X1 + (X2 - Y1))
Tactic:
rw [this]
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
this : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
⊢ Z1 + X1 = Z1 ∩ Z2 + (X2 - Y1) + X1
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
this : Z1 ∩ Z2 + (X1 + (X2 - Y1)) = Z1 ∩ Z2 + (X2 - Y1) + X1
⊢ Z1 + X1 = Z1 ∩ Z2 + (X2 - Y1) + X1
Tactic:
apply meq_union_meq_reverse
Proof state after:
case MLT.MLT.a.x
α : 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
⊢ Z1 = Z1 ∩ Z2 + (X2 - Y1)
Theorem: LT_trans
Proof state before:
case MLT.MLT.a.x
α : 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
⊢ Z1 = Z1 ∩ Z2 + (X2 - Y1)
Tactic:
apply double_split
Proof state after:
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
⊢ Y1 + Z1 = X2 + Z2
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
⊢ Y1 + Z1 = X2 + Z2
Tactic:
rw [add_comm]
Proof state after:
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
⊢ Z1 + Y1 = X2 + Z2
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
⊢ Z1 + Y1 = X2 + Z2
Tactic:
rw [← N1_def]
Proof state after:
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
⊢ N = X2 + Z2
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
⊢ N = X2 + Z2
Tactic:
rw [N2_def]
Proof state after:
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