internlm/Lean-Github huggingface dataset:
Theorem: direct_subset_red
Proof state before:
case 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
⊢ N = Z + newY + {y}
Tactic:
have newY_y_Y: newY + {y} = Y := by unfold_let newY; simp [mul_cons_trivial]; apply Multiset.cons_erase claim
Proof state after:
case 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
newY_y_Y : newY + {y} = Y
⊢ N = Z + newY + {y}
Theorem: direct_subset_red
Proof state before:
case 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
newY_y_Y : newY + {y} = Y
⊢ N = Z + newY + {y}
Tactic:
have : Z + newY + {y} = Z + (newY + {y}) := by apply add_assoc
Proof state after:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + newY + {y}
Theorem: direct_subset_red
Proof state before:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + newY + {y}
Tactic:
rw [this]
Proof state after:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + (newY + {y})
Theorem: direct_subset_red
Proof state before:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + (newY + {y})
Tactic:
rw [newY_y_Y]
Proof state after:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + Y
Theorem: direct_subset_red
Proof state before:
case 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
newY_y_Y : newY + {y} = Y
this : Z + newY + {y} = Z + (newY + {y})
⊢ N = Z + Y
Tactic:
exact N_def
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 + {y} = Y
Tactic:
unfold_let newY
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
⊢ Y.erase y + {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 ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
⊢ Y.erase y + {y} = Y
Tactic:
simp [mul_cons_trivial]
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
⊢ y ::ₘ Y.erase 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 ≠ ∅
newY_sub_Y : newY < Y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
⊢ y ::ₘ Y.erase y = Y
Tactic:
apply Multiset.cons_erase 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
newY_y_Y : newY + {y} = Y
⊢ Z + newY + {y} = Z + (newY + {y})
Tactic:
apply add_assoc
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case 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
⊢ ∀ y_1 ∈ f y, y_1 < y
Tactic:
unfold_let f
Proof state after:
case 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
⊢ ∀ y_1 ∈ (fun y' => Multiset.filter (fun x => x < y') X) y, y_1 < y
Theorem: direct_subset_red
Proof state before:
case 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
⊢ ∀ y_1 ∈ (fun y' => Multiset.filter (fun x => x < y') X) y, y_1 < y
Tactic:
intro z z_in
Proof state after:
case 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
z : α
z_in : z ∈ (fun y' => Multiset.filter (fun x => x < y') X) y
⊢ z < y
Theorem: direct_subset_red
Proof state before:
case 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
z : α
z_in : z ∈ (fun y' => Multiset.filter (fun x => x < y') X) y
⊢ z < y
Tactic:
simp at z_in
Proof state after:
case 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
z : α
z_in : z ∈ X ∧ z < y
⊢ z < y
Theorem: direct_subset_red
Proof state before:
case 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
z : α
z_in : z ∈ X ∧ z < y
⊢ z < y
Tactic:
tauto
Proof state after:
no goals
Theorem: Lt_LT_equiv
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
⊢ MultisetLt = MultisetLT
Tactic:
funext X Y
Proof state after:
case h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y = MultisetLT X Y
Theorem: Lt_LT_equiv
Proof state before:
case h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y = MultisetLT X Y
Tactic:
apply propext
Proof state after:
case h.h.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y ↔ MultisetLT X Y
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y ↔ MultisetLT X Y
Tactic:
constructor
Proof state after:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y → MultisetLT X Y

case h.h.a.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLT X Y → MultisetLt X Y
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y → MultisetLT X Y
Tactic:
intros hLt
Proof state after:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
hLt : MultisetLt X Y
⊢ MultisetLT X Y
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
hLt : MultisetLt X Y
⊢ MultisetLT X Y
Tactic:
induction hLt with
| base a b hLt =>
  rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
  use X
  simp
  simp
  assumption
| trans Z W A _ _ aih bih => exact LT_trans _ _ _ bih aih
Proof state after:
no goals
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mp.base
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y a b : Multiset α
hLt : MultisetRedLt a b
⊢ MultisetLT a b
Tactic:
rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
Proof state after:
case h.h.a.mp.base.RedLt
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ MultisetLT a b
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mp.base.RedLt
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ MultisetLT a b
Tactic:
use X
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ {y} ≠ ∅

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Theorem: Lt_LT_equiv
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ {y} ≠ ∅

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Tactic:
simp
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Theorem: Lt_LT_equiv
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, ∃ y_1 ∈ {y}, x < y_1
Tactic:
simp
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, x < y
Theorem: Lt_LT_equiv
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ ∀ x ∈ X, x < y
Tactic:
assumption
Proof state after:
no goals
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mp.trans
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y Z W A : Multiset α
a✝¹ : TC MultisetRedLt Z W
a✝ : TC MultisetRedLt W A
aih : MultisetLT Z W
bih : MultisetLT W A
⊢ MultisetLT Z A
Tactic:
exact LT_trans _ _ _ bih aih
Proof state after:
no goals
Theorem: Lt_LT_equiv
Proof state before:
case h.h.a.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLT X Y → MultisetLt X Y
Tactic:
apply direct_subset_red
Proof state after:
no goals
Theorem: equiv_r_wf
Proof state before:
α : Type u_1
r1 r2 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
h2 : r1 = r2
⊢ WellFounded r2
Tactic:
subst h2
Proof state after:
α : Type u_1
r1 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
⊢ WellFounded r1
Theorem: equiv_r_wf
Proof state before:
α : Type u_1
r1 : Multiset α → Multiset α → Prop
inst✝¹ : DecidableEq α
inst✝ : LT α
h1 : WellFounded r1
⊢ WellFounded r1
Tactic:
simp_all only
Proof state after:
no goals
Theorem: mytaut1
Proof state before:
p : ℕ
⊢ tautology (~(·p)⋀(~·p))
Tactic:
unfold tautology
Proof state after:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(·p)⋀(~·p))
Theorem: mytaut1
Proof state before:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(·p)⋀(~·p))
Tactic:
intro W M w
Proof state after:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(·p)⋀(~·p))
Theorem: mytaut1
Proof state before:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(·p)⋀(~·p))
Tactic:
simp
Proof state after:
no goals
Theorem: mytaut2
Proof state before:
p : ℕ
⊢ tautology (~(~~·p)⋀(~·p))
Tactic:
unfold tautology evaluate
Proof state after:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ((~~·p)⋀(~·p))
Theorem: mytaut2
Proof state before:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ((~~·p)⋀(~·p))
Tactic:
intro W M w
Proof state after:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w ((~~·p)⋀(~·p))
Theorem: mytaut2
Proof state before:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w ((~~·p)⋀(~·p))
Tactic:
simp
Proof state after:
no goals
Theorem: mysat
Proof state before:
p : ℕ
⊢ satisfiable (·p)
Tactic:
use ℕ, myModel, 1
Proof state after:
case h
p : ℕ
⊢ evaluate myModel 1 (·p)
Theorem: mysat
Proof state before:
case h
p : ℕ
⊢ evaluate myModel 1 (·p)
Tactic:
unfold myModel
Proof state after:
case h
p : ℕ
⊢ evaluate { val := fun x x => True, Rel := fun x x v => HEq v 1 } 1 (·p)
Theorem: mysat
Proof state before:
case h
p : ℕ
⊢ evaluate { val := fun x x => True, Rel := fun x x v => HEq v 1 } 1 (·p)
Tactic:
simp
Proof state after:
no goals
Theorem: A2
Proof state before:
a : Program
⊢ tautology (⌈a⌉⊤)
Tactic:
unfold tautology
Proof state after:
a : Program
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (⌈a⌉⊤)
Theorem: A2
Proof state before:
a : Program
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (⌈a⌉⊤)
Tactic:
simp
Proof state after:
no goals
Theorem: A3
Proof state before:
a : Program
X Y : Formula
⊢ tautology (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))
Tactic:
unfold tautology
Proof state after:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))
Theorem: A3
Proof state before:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))
Tactic:
simp
Proof state after:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    (∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y) →
      (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M a w x → evaluate M x Y