internlm/Lean-Github huggingface dataset:
Theorem: direct_subset_red
Proof state before:
case intro.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
y : α
Y'_def : Y = {y}
⊢ MultisetRedLt M N
Tactic:
rw [Y'_def] at N_def
Proof state after:
case intro.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
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
⊢ MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro.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
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
⊢ MultisetRedLt M N
Tactic:
apply @MultisetRedLt.RedLt α _ _ M N Z X y M_def N_def
Proof state after:
case intro.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
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
⊢ ∀ y_1 ∈ X, y_1 < y
Theorem: direct_subset_red
Proof state before:
case intro.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
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
⊢ ∀ y_1 ∈ X, y_1 < y
Tactic:
simp [Y'_def] at X_lt_Y
Proof state after:
case intro.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
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
X_lt_Y : ∀ x ∈ X, x < y
⊢ ∀ y_1 ∈ X, y_1 < y
Theorem: direct_subset_red
Proof state before:
case intro.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
hyp' : ¬Multiset.card Y = 0
y : α
N_def : N = Z + {y}
Y'_def : Y = {y}
X_lt_Y : ∀ x ∈ X, x < y
⊢ ∀ y_1 ∈ X, y_1 < y
Tactic:
exact X_lt_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
⊢ TC MultisetRedLt M N
Tactic:
have : ∃ a, a ∈ Y := by
  rw [← Y.card_pos_iff_exists_mem]
  cases foo : Multiset.card Y
  tauto
  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
this : ∃ a, a ∈ Y
⊢ TC MultisetRedLt M N
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
this : ∃ a, a ∈ Y
⊢ TC MultisetRedLt M N
Tactic:
rcases this with ⟨y,claim⟩
Proof state after:
case intro
α : 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
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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
⊢ TC MultisetRedLt M N
Tactic:
let newY := Y.erase y
Proof state after:
case intro
α : 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
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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
⊢ TC MultisetRedLt M N
Tactic:
have newY_nonEmpty : newY ≠ ∅ := by
  have card_Y_ge_2 : Multiset.card Y ≥ 2 := nat_not_0_not_1 _ hyp' hyp
  have : Multiset.card (Multiset.erase Y y) ≥ 1 := by
    rw [Multiset.card_erase_eq_ite]
    simp_all?
    have card_Y_g_1 : 1 < Multiset.card Y := by aesop
    exact Nat.pred_le_pred card_Y_g_1
  have : 0 < Multiset.card (Multiset.erase Y y) := by aesop
  rw [Multiset.card_pos] at this
  aesop
Proof state after:
case intro
α : 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 ≠ ∅
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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 ≠ ∅
⊢ TC MultisetRedLt M N
Tactic:
have newY_sub_Y : newY < Y := by simp (config := {zetaDelta := true}); exact claim
Proof state after:
case intro
α : 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
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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
⊢ TC MultisetRedLt M N
Tactic:
let f : α → Multiset α := fun y' => X.filter (fun x => x < y')
Proof state after:
case intro
α : 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
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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
⊢ TC MultisetRedLt M N
Tactic:
let N' := Z + newY + f y
Proof state after:
case intro
α : 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
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case intro
α : 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
⊢ TC MultisetRedLt M N
Tactic:
apply TC.trans
Proof state after:
case intro.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
⊢ TC MultisetRedLt M ?intro.b

case intro.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
⊢ TC MultisetRedLt ?intro.b N

case intro.b
α : 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 α
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:
case intro.b => exact N'
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
⊢ ∃ a, a ∈ Y
Tactic:
rw [← Y.card_pos_iff_exists_mem]
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
⊢ 0 < Multiset.card 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
⊢ 0 < Multiset.card Y
Tactic:
cases foo : Multiset.card Y
Proof state after:
case zero
α : 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
foo : Multiset.card Y = 0
⊢ 0 < 0

case succ
α : 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
n✝ : ℕ
foo : Multiset.card Y = n✝ + 1
⊢ 0 < n✝ + 1
Theorem: direct_subset_red
Proof state before:
case zero
α : 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
foo : Multiset.card Y = 0
⊢ 0 < 0

case succ
α : 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
n✝ : ℕ
foo : Multiset.card Y = n✝ + 1
⊢ 0 < n✝ + 1
Tactic:
tauto
Proof state after:
case succ
α : 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
n✝ : ℕ
foo : Multiset.card Y = n✝ + 1
⊢ 0 < n✝ + 1
Theorem: direct_subset_red
Proof state before:
case succ
α : 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
n✝ : ℕ
foo : Multiset.card Y = n✝ + 1
⊢ 0 < n✝ + 1
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 ≠ ∅
Tactic:
have card_Y_ge_2 : Multiset.card Y ≥ 2 := nat_not_0_not_1 _ hyp' hyp
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
⊢ 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
card_Y_ge_2 : Multiset.card Y ≥ 2
⊢ newY ≠ ∅
Tactic:
have : Multiset.card (Multiset.erase Y y) ≥ 1 := by
  rw [Multiset.card_erase_eq_ite]
  simp_all?
  have card_Y_g_1 : 1 < Multiset.card Y := by aesop
  exact Nat.pred_le_pred card_Y_g_1
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
this : Multiset.card (Y.erase y) ≥ 1
⊢ 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
card_Y_ge_2 : Multiset.card Y ≥ 2
this : Multiset.card (Y.erase y) ≥ 1
⊢ newY ≠ ∅
Tactic:
have : 0 < Multiset.card (Multiset.erase Y y) := by aesop
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
this✝ : Multiset.card (Y.erase y) ≥ 1
this : 0 < Multiset.card (Y.erase 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
card_Y_ge_2 : Multiset.card Y ≥ 2
this✝ : Multiset.card (Y.erase y) ≥ 1
this : 0 < Multiset.card (Y.erase y)
⊢ newY ≠ ∅
Tactic:
rw [Multiset.card_pos] at 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
card_Y_ge_2 : Multiset.card Y ≥ 2
this✝ : Multiset.card (Y.erase y) ≥ 1
this : Y.erase y ≠ 0
⊢ newY ≠ ∅