internlm/Lean-Github huggingface dataset:
Theorem: direct_subset_red
Proof state before:
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
⊢ z + x = z + fx + (x - fx)
Tactic:
change fx ≤ x at count_lt
Proof state after:
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
⊢ z + x = z + fx + (x - fx)
Theorem: direct_subset_red
Proof state before:
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
⊢ z + x = z + fx + (x - fx)
Tactic:
have : x = fx + (x - fx) := by aesop
Proof state after:
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this✝ : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
this : x = fx + (x - fx)
⊢ z + x = z + fx + (x - fx)
Theorem: direct_subset_red
Proof state before:
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this✝ : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
this : x = fx + (x - fx)
⊢ z + x = z + fx + (x - fx)
Tactic:
linarith
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 M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
⊢ x = fx + (x - fx)
Tactic:
aesop
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case intro.a.NZY
α : 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
⊢ N' = Z + f y + newY
Tactic:
have : Z + newY + f y = Z + f y + newY := by
  have : newY + f y = f y + newY := by apply add_comm
  have : Z + newY + f y = Z + (newY + f y) := by apply add_assoc
  rw [this]
  clear this
  have : Z + f y + newY = Z + (f y + newY) := by apply add_assoc
  rw [this]
  simp (config := { zetaDelta := true }) only [gt_iff_lt, add_right_inj]
  assumption
Proof state after:
case intro.a.NZY
α : 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
this : Z + newY + f y = Z + f y + newY
⊢ N' = Z + f y + newY
Theorem: direct_subset_red
Proof state before:
case intro.a.NZY
α : 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
this : Z + newY + f y = Z + f y + newY
⊢ N' = Z + f y + newY
Tactic:
unfold_let N'
Proof state after:
case intro.a.NZY
α : 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
this : Z + newY + f y = Z + f y + newY
⊢ Z + newY + f y = Z + f y + newY
Theorem: direct_subset_red
Proof state before:
case intro.a.NZY
α : 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
this : Z + newY + f y = Z + f y + newY
⊢ Z + newY + f y = Z + f y + newY
Tactic:
rw [add_assoc, add_assoc, add_comm newY (f y)]
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
⊢ Z + newY + f y = Z + f y + newY
Tactic:
have : newY + f y = f y + newY := by 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
this : newY + f y = f y + newY
⊢ Z + newY + f y = Z + f y + newY
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
this : newY + f y = f y + newY
⊢ Z + newY + f y = Z + f y + newY
Tactic:
have : Z + newY + f y = Z + (newY + f y) := by apply add_assoc
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
this✝ : newY + f y = f y + newY
this : Z + newY + f y = Z + (newY + f y)
⊢ Z + newY + f y = Z + f y + newY
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
this✝ : newY + f y = f y + newY
this : Z + newY + f y = Z + (newY + f y)
⊢ Z + newY + f y = Z + f y + newY
Tactic:
rw [this]
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
this✝ : newY + f y = f y + newY
this : Z + newY + f y = Z + (newY + f y)
⊢ Z + (newY + f y) = Z + f y + newY
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
this✝ : newY + f y = f y + newY
this : Z + newY + f y = Z + (newY + f y)
⊢ Z + (newY + f y) = Z + f y + newY
Tactic:
clear this
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
this : newY + f y = f y + newY
⊢ Z + (newY + f y) = Z + f y + newY
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
this : newY + f y = f y + newY
⊢ Z + (newY + f y) = Z + f y + newY
Tactic:
have : Z + f y + newY = Z + (f y + newY) := by apply add_assoc
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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Z + (newY + f y) = Z + f y + newY
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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Z + (newY + f y) = Z + f y + newY
Tactic:
rw [this]
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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Z + (newY + f y) = Z + (f y + newY)
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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Z + (newY + f y) = Z + (f y + newY)
Tactic:
simp (config := { zetaDelta := true }) only [gt_iff_lt, add_right_inj]
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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Y.erase y + Multiset.filter (fun x => x < y) X = Multiset.filter (fun x => x < y) X + Y.erase 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
this✝ : newY + f y = f y + newY
this : Z + f y + newY = Z + (f y + newY)
⊢ Y.erase y + Multiset.filter (fun x => x < y) X = Multiset.filter (fun x => x < y) X + Y.erase y
Tactic:
assumption
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
⊢ newY + f y = f y + newY
Tactic:
apply add_comm
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
this : newY + f y = f y + newY
⊢ Z + newY + f y = Z + (newY + f y)
Tactic:
apply add_assoc
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
this : newY + f y = f y + newY
⊢ Z + f y + newY = Z + (f y + newY)
Tactic:
apply add_assoc
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case intro.a.h
α : 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 - f y, ∃ y ∈ newY, x < y
Tactic:
intro x x_in
Proof state after:
case intro.a.h
α : 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
⊢ ∃ y ∈ newY, x < y