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
card_Y_ge_2 : Multiset.card Y ≥ 2
this✝ : Multiset.card (Y.erase y) ≥ 1
this : Y.erase y ≠ 0
⊢ newY ≠ ∅
Tactic:
aesop
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
card_Y_ge_2 : Multiset.card Y ≥ 2
⊢ Multiset.card (Y.erase y) ≥ 1
Tactic:
rw [Multiset.card_erase_eq_ite]
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
card_Y_ge_2 : Multiset.card Y ≥ 2
⊢ (if y ∈ Y then (Multiset.card Y).pred else Multiset.card Y) ≥ 1
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
card_Y_ge_2 : Multiset.card Y ≥ 2
⊢ (if y ∈ Y then (Multiset.card Y).pred else Multiset.card Y) ≥ 1
Tactic:
simp_all?
Proof state after:
α : 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
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
card_Y_ge_2 : 2 ≤ Multiset.card Y
⊢ 1 ≤ Multiset.card Y - 1
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
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
card_Y_ge_2 : 2 ≤ Multiset.card Y
⊢ 1 ≤ Multiset.card Y - 1
Tactic:
have card_Y_g_1 : 1 < Multiset.card Y := by aesop
Proof state after:
α : 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
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
card_Y_ge_2 : 2 ≤ Multiset.card Y
card_Y_g_1 : 1 < Multiset.card Y
⊢ 1 ≤ Multiset.card Y - 1
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
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
card_Y_ge_2 : 2 ≤ Multiset.card Y
card_Y_g_1 : 1 < Multiset.card Y
⊢ 1 ≤ Multiset.card Y - 1
Tactic:
exact Nat.pred_le_pred card_Y_g_1
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
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
card_Y_ge_2 : 2 ≤ Multiset.card Y
⊢ 1 < Multiset.card Y
Tactic:
aesop
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
card_Y_ge_2 : Multiset.card Y ≥ 2
this : Multiset.card (Y.erase y) ≥ 1
⊢ 0 < Multiset.card (Y.erase y)
Tactic:
aesop
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 < Y
Tactic:
simp (config := {zetaDelta := true})
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 ≠ ∅
⊢ y ∈ 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 ≠ ∅
⊢ y ∈ Y
Tactic:
exact claim
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
⊢ Multiset α
Tactic:
exact N'
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case intro.a.MZX
α : 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
⊢ M = Z + f y + (X - f y)
Tactic:
have : f y ≤ X := Multiset.filter_le (fun x => x < y) X
Proof state after:
case intro.a.MZX
α : 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 : f y ≤ X
⊢ M = Z + f y + (X - f y)
Theorem: direct_subset_red
Proof state before:
case intro.a.MZX
α : 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 : f y ≤ X
⊢ M = Z + f y + (X - f y)
Tactic:
ext a
Proof state after:
case intro.a.MZX.a
α : 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 : f y ≤ X
a : α
⊢ Multiset.count a M = Multiset.count a (Z + f y + (X - f y))
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 : 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 : f y ≤ X
a : α
⊢ Multiset.count a M = Multiset.count a (Z + f y + (X - f y))
Tactic:
have count_lt := Multiset.count_le_of_le a this
Proof state after:
case intro.a.MZX.a
α : 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 : f y ≤ X
a : α
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
⊢ Multiset.count a M = Multiset.count a (Z + f y + (X - f y))
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 : 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 : f y ≤ X
a : α
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
⊢ Multiset.count a M = Multiset.count a (Z + f y + (X - f y))
Tactic:
rw [M_def]
Proof state after:
case intro.a.MZX.a
α : 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 : f y ≤ X
a : α
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
⊢ Multiset.count a (Z + X) = Multiset.count a (Z + f y + (X - f y))
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 : 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 : f y ≤ X
a : α
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
⊢ Multiset.count a (Z + X) = Multiset.count a (Z + f y + (X - f y))
Tactic:
simp_all
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
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
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
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
Tactic:
let x := Multiset.count a X
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
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
x : ℕ := Multiset.count a X
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
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
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
Tactic:
let z := Multiset.count a Z
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
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
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
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
Tactic:
let fx := Multiset.count a (Multiset.filter (fun x => x < y) X)
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
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)
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
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)
⊢ Multiset.count a Z + Multiset.count a X =
    Multiset.count a Z + Multiset.count a (f y) + (Multiset.count a X - Multiset.count a (f y))
Tactic:
change z + x = z + fx + (x - fx)
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
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)