internlm/Lean-Github huggingface dataset:
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ M ≤ M + P
Tactic:
simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N = M
Tactic:
have : M = M - N + N := by
  apply mem_leq_diff
  exact h
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P
this : M = M - N + N
⊢ M - N + N = M
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P
this : M = M - N + N
⊢ M - N + N = M
Tactic:
rw [← this]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M = M - N + N
Tactic:
apply mem_leq_diff
Proof state after:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ N ≤ M
Theorem: le_sub_add
Proof state before:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ N ≤ M
Tactic:
exact h
Proof state after:
no goals
Theorem: le_eq_sub
Proof state before:
⊢ ∀ (M N P Q : ℕ), M ≤ P → M + N = P + Q → N = Q + (P - M)
Tactic:
intros M N P Q h0 h1
Proof state after:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
⊢ N = Q + (P - M)
Theorem: le_eq_sub
Proof state before:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
⊢ N = Q + (P - M)
Tactic:
have := tsub_add_cancel_of_le h0
Proof state after:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
this : P - M + M = P
⊢ N = Q + (P - M)
Theorem: le_eq_sub
Proof state before:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
this : P - M + M = P
⊢ N = Q + (P - M)
Tactic:
linarith
Proof state after:
no goals
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P Q : Multiset α), M + N = P + Q → N = N ∩ Q + (P - M)
Tactic:
intros M N P Q h
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N = N ∩ Q + (P - M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N = N ∩ Q + (P - M)
Tactic:
ext x
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q + (P - M))
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q + (P - M))
Tactic:
rw [Multiset.count_add]
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q) + Multiset.count x (P - M)
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q) + Multiset.count x (P - M)
Tactic:
rw [Multiset.count_inter]
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + Multiset.count x (P - M)
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + Multiset.count x (P - M)
Tactic:
rw [Multiset.count_sub]
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q := by
  rw [Multiset.ext] at h
  simp_all only [Multiset.mem_add, Multiset.count_add]
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
rw [Multiset.ext] at h
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), Multiset.count a (M + N) = Multiset.count a (P + Q)
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), Multiset.count a (M + N) = Multiset.count a (P + Q)
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
simp_all only [Multiset.mem_add, Multiset.count_add]
Proof state after:
no goals
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have : Multiset.count x N ≥ Multiset.count x Q := by linarith
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x N ≥ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x N ≥ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all only [ge_iff_le, min_eq_right]
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x N = Multiset.count x Q + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x N = Multiset.count x Q + (Multiset.count x P - Multiset.count x M)
Tactic:
apply le_eq_sub (Multiset.count x M) (Multiset.count x N) (Multiset.count x P) (Multiset.count x Q)
Proof state after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M ≤ Multiset.count x P

case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N ≥ Multiset.count x Q
Tactic:
linarith
Proof state after:
no goals
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M ≤ Multiset.count x P
Tactic:
simp_all
Proof state after:
no goals
Theorem: double_split
Proof state before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
exact H0
Proof state after:
no goals
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : ¬Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all only [not_le, gt_iff_lt]
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have : Multiset.count x N ≤ Multiset.count x Q := by linarith
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this : Multiset.count x N ≤ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this : Multiset.count x N ≤ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have:= le_of_lt l_u
Proof state after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this✝ : Multiset.count x N ≤ Multiset.count x Q
this : Multiset.count x P ≤ Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this✝ : Multiset.count x N ≤ Multiset.count x Q
this : Multiset.count x P ≤ Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all
Proof state after:
no goals
Theorem: double_split
Proof state before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N ≤ Multiset.count x Q
Tactic:
linarith
Proof state after:
no goals
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (X Y : Multiset α), x ∈ X → x ∉ Y → x ∈ X - Y
Tactic:
intros x X Y x_in_X x_notin_Y
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ x ∈ X - Y
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ x ∈ X - Y
Tactic:
have : Multiset.count x X ≥ 1 := by
  rw [← Multiset.one_le_count_iff_mem] at x_in_X
  exact x_in_X
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∈ X - Y
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∈ X - Y
Tactic:
have : Multiset.count x Y = 0 := by apply Multiset.count_eq_zero_of_not_mem; exact x_notin_Y
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ x ∈ X - Y
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ x ∈ X - Y
Tactic:
rw [← Multiset.one_le_count_iff_mem]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x (X - Y)
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x (X - Y)
Tactic:
rw [Multiset.count_sub]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x X - Multiset.count x Y
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x X - Multiset.count x Y
Tactic:
aesop
Proof state after:
no goals
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
Tactic:
rw [← Multiset.one_le_count_iff_mem] at x_in_X
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : 1 ≤ Multiset.count x X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : 1 ≤ Multiset.count x X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
Tactic:
exact x_in_X
Proof state after:
no goals
Theorem: in_notin_diff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ Multiset.count x Y = 0
Tactic:
apply Multiset.count_eq_zero_of_not_mem
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∉ Y
Theorem: in_notin_diff
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∉ Y
Tactic:
exact x_notin_Y
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P : Multiset α), MultisetLT N M → MultisetLT P N → MultisetLT P M
Tactic:
intros M N P LTNM LTPN
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTNM : MultisetLT N M
LTPN : MultisetLT P N
⊢ MultisetLT P M
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTNM : MultisetLT N M
LTPN : MultisetLT P N
⊢ MultisetLT P M
Tactic:
rcases LTNM with ⟨Y1, X1, Z1, X1_ne, N1_def, M1_def, Ord1⟩
Proof state after:
case MLT
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTPN : MultisetLT P N
Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
⊢ MultisetLT P M
Theorem: LT_trans
Proof state before:
case MLT
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTPN : MultisetLT P N
Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
⊢ MultisetLT P M
Tactic:
rcases LTPN with ⟨Y2, X2, Z2, _, P2_def, N2_def, Ord2⟩
Proof state after:
case MLT.MLT
α : 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
⊢ MultisetLT P M
Theorem: LT_trans
Proof state before:
case MLT.MLT
α : 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
⊢ MultisetLT P M
Tactic:
apply MultisetLT.MLT (Y2 + (Y1 - X2)) (X1 + (X2 - Y1)) (Z1 ∩ Z2)
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
⊢ 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
⊢ 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
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) ≠ ∅

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:
. aesop
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
⊢ 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