internlm/Lean-Github huggingface dataset:
Theorem: LT_trans
Proof state before:
case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∈ X2

case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∉ Y1
Tactic:
exact x_in_X2
Proof state after:
case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∉ Y1
Theorem: LT_trans
Proof state before:
case h.left.h.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ x ∉ Y1
Tactic:
exact x_in
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
case h.right
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∉ Y1
⊢ y < x
Tactic:
exact y_lt_x
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∉ Y2
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
have y_in : y ∈ (Y1 - X2) := by aesop
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
let h := (Ord1 y)
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
have y_in_Y1 : y ∈ Y1 := by
  have : Y1 - X2 ≤ Y1 := by aesop
  apply Multiset.mem_of_le
  exact this
  exact y_in
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
y_in_Y1 : y ∈ Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
y_in_Y1 : y ∈ Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
let _ := h y_in_Y1
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
y_in_Y1 : y ∈ Y1
x✝ : ∃ y_1 ∈ X1, y < y_1 := h y_in_Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
y_in_Y1 : y ∈ Y1
x✝ : ∃ y_1 ∈ X1, y < y_1 := h y_in_Y1
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
Tactic:
aesop
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∉ Y2
⊢ y ∈ Y1 - X2
Tactic:
aesop
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
⊢ y ∈ Y1
Tactic:
have : Y1 - X2 ≤ Y1 := by aesop
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ Y1
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ Y1
Tactic:
apply Multiset.mem_of_le
Proof state after:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ ?s ≤ Y1

case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ ?s

case s
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ Multiset α
Theorem: LT_trans
Proof state before:
case h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ ?s ≤ Y1

case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ ?s

case s
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ Multiset α
Tactic:
exact this
Proof state after:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ Y1 - X2
Theorem: LT_trans
Proof state before:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
this : Y1 - X2 ≤ Y1
⊢ y ∈ Y1 - X2
Tactic:
exact y_in
Proof state after:
no goals
Theorem: LT_trans
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in✝ : y ∉ Y2
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
⊢ Y1 - X2 ≤ Y1
Tactic:
aesop
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
⊢ ∀ (n : ℕ), n ≠ 0 → n ≠ 1 → n ≥ 2
Tactic:
intros n h0 h1
Proof state after:
n : ℕ
h0 : n ≠ 0
h1 : n ≠ 1
⊢ n ≥ 2
Theorem: nat_not_0_not_1
Proof state before:
n : ℕ
h0 : n ≠ 0
h1 : n ≠ 1
⊢ n ≥ 2
Tactic:
cases n
Proof state after:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
⊢ n✝ + 1 ≥ 2
Theorem: nat_not_0_not_1
Proof state before:
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2
Tactic:
case zero => contradiction
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ m + 1 ≥ 2
Tactic:
case succ m =>
  cases m
  case zero => contradiction
  case succ n=>
    apply Nat.succ_le_succ
    aesop
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2
Tactic:
contradiction
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ m + 1 ≥ 2
Tactic:
cases m
Proof state after:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ n✝ + 1 + 1 ≥ 2
Theorem: nat_not_0_not_1
Proof state before:
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2
Tactic:
case zero => contradiction
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ n + 1 + 1 ≥ 2
Tactic:
case succ n=>
  apply Nat.succ_le_succ
  aesop
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2
Tactic:
contradiction
Proof state after:
no goals
Theorem: nat_not_0_not_1
Proof state before:
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ n + 1 + 1 ≥ 2
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ 1 ≤ n + 1
Theorem: nat_not_0_not_1
Proof state before:
case a
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ 1 ≤ n + 1
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
M N : Multiset α
LTMN : MultisetLT M N
⊢ MultisetLt M N
Tactic:
cases LTMN
Proof state after:
case MLT
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ MultisetLt M N
Theorem: direct_subset_red
Proof state before:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X Y Z : Multiset α
Y_not_empty : Y ≠ ∅
MZX : M = Z + X
NZY : N = Z + Y
h : ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLt M N
Tactic:
unfold MultisetLt
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X Y Z : Multiset α
Y_not_empty : Y ≠ ∅
MZX : M = Z + X
NZY : N = Z + Y
h : ∀ x ∈ X, ∃ y ∈ Y, x < 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
M N X Y Z : Multiset α
Y_not_empty : Y ≠ ∅
MZX : M = Z + X
NZY : N = Z + Y
h : ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ TC MultisetRedLt M N
Tactic:
revert Z X M N
Proof state after:
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
Y_not_empty : Y ≠ ∅
⊢ ∀ (M N X Z : Multiset α), M = Z + X → N = Z + Y → (∀ x ∈ X, ∃ y ∈ Y, x < 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 α
Y_not_empty : Y ≠ ∅
⊢ ∀ (M N X Z : Multiset α), M = Z + X → N = Z + Y → (∀ x ∈ X, ∃ y ∈ Y, x < y) → TC MultisetRedLt M N
Tactic:
induction Y using Multiset.strongInductionOn
Proof state after:
case ih
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
s✝ : Multiset α
a✝ :
  ∀ t < s✝, 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 : s✝ ≠ ∅
⊢ ∀ (M N X Z : Multiset α), M = Z + X → N = Z + s✝ → (∀ x ∈ X, ∃ y ∈ s✝, x < 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 = Z + X → N = Z + Y → (∀ x ∈ X, ∃ y ∈ Y, x < y) → TC MultisetRedLt M N
Tactic:
intro M N X Z M_def N_def X_lt_Y
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
⊢ 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
⊢ TC MultisetRedLt M N
Tactic:
cases em (Multiset.card Y = 0)
Proof state after:
case inl
α : 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
h✝ : Multiset.card Y = 0
⊢ TC MultisetRedLt M N

case inr
α : 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
h✝ : ¬Multiset.card Y = 0
⊢ TC MultisetRedLt M N
Theorem: direct_subset_red
Proof state before:
case inr
α : 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
h✝ : ¬Multiset.card Y = 0
⊢ TC MultisetRedLt M N
Tactic:
cases em (Multiset.card Y = 1)
Proof state after:
case inr.inl
α : 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
h✝¹ : ¬Multiset.card Y = 0
h✝ : Multiset.card Y = 1
⊢ TC MultisetRedLt M N

case inr.inr
α : 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
h✝¹ : ¬Multiset.card Y = 0
h✝ : ¬Multiset.card Y = 1
⊢ 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
⊢ TC MultisetRedLt M N
Tactic:
case inl hyp' hyp=>
  rw [Multiset.card_eq_one] at hyp
  rcases hyp with ⟨y,Y'_def⟩
  apply TC.base
  rw [Y'_def] at N_def
  apply @MultisetRedLt.RedLt α _ _ M N Z X y M_def N_def
  simp [Y'_def] at X_lt_Y
  exact X_lt_Y
Proof state after:
no goals
Theorem: direct_subset_red
Proof state before:
case inl
α : 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
h✝ : Multiset.card Y = 0
⊢ TC MultisetRedLt M N
Tactic:
simp_all
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:
rw [Multiset.card_eq_one] at 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 : ∃ a, Y = {a}
⊢ 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 : ∃ a, Y = {a}
⊢ TC MultisetRedLt M N
Tactic:
rcases hyp with ⟨y,Y'_def⟩
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
y : α
Y'_def : 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
y : α
Y'_def : Y = {y}
⊢ TC MultisetRedLt M N
Tactic:
apply TC.base
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
y : α
Y'_def : Y = {y}
⊢ MultisetRedLt M N