internlm/Lean-Github huggingface dataset:
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
⊢ False
Tactic:
let neg_f : α → Multiset α := fun y' => X.filter (fun x => ¬ x < y')
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
⊢ False
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
⊢ False
Tactic:
have : X - f y = neg_f y := by
  have fy_negfy_X : f y + neg_f y = X := by
    rw [Multiset.filter_add_not]
  have fy_le_X : f y ≤ X := Multiset.filter_le _ X
  have : X - f y + f y = neg_f y + f y := by
    have : X = X - f y + f y := by
      apply mem_leq_diff
      exact fy_le_X
    rw [← this]
    rw [← fy_negfy_X]
    apply add_comm
  rw [← fy_negfy_X]; simp
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
⊢ False
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
⊢ False
Tactic:
have x_in_neg_fy : x ∈ neg_f y := by rw [this] at x_in; exact x_in
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
x_in_neg_fy : x ∈ neg_f y
⊢ False
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
x_in_neg_fy : x ∈ neg_f y
⊢ False
Tactic:
subst_eqs
Proof state after:
case refl.refl.refl
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
X Z : Multiset α
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
x_in_neg_fy : x ∈ neg_f y
t_in_Y : y ∈ Y
x_lt_t : x < y
t_in_newY : y ∉ newY
⊢ False
Theorem: direct_subset_red
Proof state before:
case refl.refl.refl
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
X Z : Multiset α
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = neg_f y
x_in_neg_fy : x ∈ neg_f y
t_in_Y : y ∈ Y
x_lt_t : x < y
t_in_newY : y ∉ newY
⊢ False
Tactic:
unfold_let neg_f at *
Proof state after:
case refl.refl.refl
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
X Z : Multiset α
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = (fun y' => Multiset.filter (fun x => ¬x < y') X) y
x_in_neg_fy : x ∈ (fun y' => Multiset.filter (fun x => ¬x < y') X) y
t_in_Y : y ∈ Y
x_lt_t : x < y
t_in_newY : y ∉ newY
⊢ False
Theorem: direct_subset_red
Proof state before:
case refl.refl.refl
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
X Z : Multiset α
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
this : X - f y = (fun y' => Multiset.filter (fun x => ¬x < y') X) y
x_in_neg_fy : x ∈ (fun y' => Multiset.filter (fun x => ¬x < y') X) y
t_in_Y : y ∈ Y
x_lt_t : x < y
t_in_newY : y ∉ newY
⊢ False
Tactic:
simp_all only [Multiset.empty_eq_zero, ne_eq, Multiset.card_eq_zero,
  not_false_eq_true, Multiset.mem_filter, not_true_eq_false, and_false]
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
⊢ X - f y = neg_f y
Tactic:
have fy_negfy_X : f y + neg_f y = X := by
  rw [Multiset.filter_add_not]
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
⊢ X - f y = neg_f y
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
⊢ X - f y = neg_f y
Tactic:
have fy_le_X : f y ≤ X := Multiset.filter_le _ X
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
⊢ X - f y = neg_f y
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
⊢ X - f y = neg_f y
Tactic:
have : X - f y + f y = neg_f y + f y := by
  have : X = X - f y + f y := by
    apply mem_leq_diff
    exact fy_le_X
  rw [← this]
  rw [← fy_negfy_X]
  apply add_comm
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
this : X - f y + f y = neg_f y + f y
⊢ X - f y = neg_f y
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
this : X - f y + f y = neg_f y + f y
⊢ X - f y = neg_f y
Tactic:
rw [← fy_negfy_X]
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
this : X - f y + f y = neg_f y + f y
⊢ f y + neg_f y - f y = neg_f y
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
this : X - f y + f y = neg_f y + f y
⊢ f y + neg_f y - f y = neg_f y
Tactic:
simp
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
⊢ f y + neg_f y = X
Tactic:
rw [Multiset.filter_add_not]
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
⊢ X - f y + f y = neg_f y + f y
Tactic:
have : X = X - f y + f y := by
  apply mem_leq_diff
  exact fy_le_X
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
IH : ∀ t < Y, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : Y ≠ ∅
M N X Z : Multiset α
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y✝ : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
hyp : ¬Multiset.card Y = 1
y : α
claim : y ∈ Y
newY : Multiset α := Y.erase y
newY_nonEmpty : newY ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
x : α
x_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this✝¹ : x ∈ X
t : α
t_in_Y : t ∈ Y
x_lt_t : x < t
t_in_newY : t ∉ newY
this✝ : t = y
x_in_fy : x ∈ f y
a✝ : x ∈ X - f y
neg_f : α → Multiset α := fun y' => Multiset.filter (fun x => ¬x < y') X
fy_negfy_X : f y + neg_f y = X
fy_le_X : f y ≤ X
this : X = X - f y + f y
⊢ X - f y + f y = neg_f y + f y