internlm/Lean-Github huggingface dataset:
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_in : x ∈ X - f y
⊢ ∃ y ∈ newY, x < y
Tactic:
let X_lt_Y := X_lt_Y x
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
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
⊢ ∃ y ∈ newY, x < y
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_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
⊢ ∃ y ∈ newY, x < y
Tactic:
have : x ∈ X := by
  have Xfy_le_X : X - f y ≤ X:= by simp (config := {zetaDelta := true})
  apply Multiset.mem_of_le Xfy_le_X
  exact 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
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this : x ∈ X
⊢ ∃ y ∈ newY, x < y
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_in : x ∈ X - f y
X_lt_Y : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝ x
this : x ∈ X
⊢ ∃ y ∈ newY, x < y
Tactic:
let X_lt_Y := X_lt_Y this
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
X_lt_Y✝ : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝¹ x
this : x ∈ X
X_lt_Y : ∃ y ∈ Y, x < y := X_lt_Y✝ this
⊢ ∃ y ∈ newY, x < y
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_in : x ∈ X - f y
X_lt_Y✝ : x ∈ X → ∃ y ∈ Y, x < y := X_lt_Y✝¹ x
this : x ∈ X
X_lt_Y : ∃ y ∈ Y, x < y := X_lt_Y✝ this
⊢ ∃ y ∈ newY, x < y
Tactic:
rcases X_lt_Y with ⟨t, t_in_Y, x_lt_t⟩
Proof state after:
case intro.a.h.intro.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
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
⊢ ∃ y ∈ newY, x < y
Theorem: direct_subset_red
Proof state before:
case intro.a.h.intro.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
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
⊢ ∃ y ∈ newY, x < y
Tactic:
use t
Proof state after:
case 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
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 ∈ newY ∧ x < t
Theorem: direct_subset_red
Proof state before:
case 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
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 ∈ newY ∧ x < t
Tactic:
constructor
Proof state after:
case h.left
α : 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 ∈ newY

case h.right
α : 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
⊢ x < t
Theorem: direct_subset_red
Proof state before:
case h.right
α : 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
⊢ x < t
Tactic:
. exact x_lt_t
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
⊢ x ∈ X
Tactic:
have Xfy_le_X : X - f y ≤ X:= by 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 ≠ ∅
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
Xfy_le_X : X - f y ≤ X
⊢ x ∈ X
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
Xfy_le_X : X - f y ≤ X
⊢ x ∈ X
Tactic:
apply Multiset.mem_of_le Xfy_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
Xfy_le_X : X - f y ≤ X
⊢ x ∈ X - 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
Xfy_le_X : X - f y ≤ X
⊢ x ∈ X - f y
Tactic:
exact x_in
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
⊢ X - f y ≤ X
Tactic:
simp (config := {zetaDelta := true})
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case h.left
α : 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 ∈ newY
Tactic:
if t_in_newY : t ∈ newY then
  exact t_in_newY
  else
    exfalso
    have : t = y := by
      have : Y = newY + {y} := by
        unfold_let newY
        simp [mul_cons_trivial, Multiset.cons_erase claim]
      rw [this] at t_in_Y
      rw [Multiset.mem_add] at t_in_Y
      have : t ∈ ( {y} : Multiset α) := by exact Or.resolve_left t_in_Y t_in_newY
      rw [← Multiset.mem_singleton]
      assumption
    have x_in_fy : x ∈ f y := by unfold_let f; simp; rw [← this]; tauto
    have x_notin_Xfy : x ∉ X - f y := by
      by_contra
      let neg_f : α → Multiset α := fun y' => X.filter (fun x => ¬ x < y')
      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
      have x_in_neg_fy : x ∈ neg_f y := by rw [this] at x_in; exact x_in
      subst_eqs
      unfold_let neg_f at *
      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]
    exact x_notin_Xfy x_in
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
⊢ t ∈ newY
Tactic:
exact t_in_newY
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
⊢ t ∈ newY
Tactic:
exfalso
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
⊢ 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
⊢ False
Tactic:
have : t = y := by
  have : Y = newY + {y} := by
    unfold_let newY
    simp [mul_cons_trivial, Multiset.cons_erase claim]
  rw [this] at t_in_Y
  rw [Multiset.mem_add] at t_in_Y
  have : t ∈ ( {y} : Multiset α) := by exact Or.resolve_left t_in_Y t_in_newY
  rw [← Multiset.mem_singleton]
  assumption
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
⊢ 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
⊢ False
Tactic:
have x_in_fy : x ∈ f y := by unfold_let f; simp; rw [← this]; tauto
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
⊢ False