internlm/Lean-Github huggingface dataset:
Theorem: polynomial.minus_lt
Proof state before:
case inl
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))) == Ordering.lt) = true

case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
Tactic:
sorry
Proof state after:
case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
Theorem: polynomial.minus_lt
Proof state before:
case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
Tactic:
sorry
Proof state after:
no goals
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.fst ∈ l
Tactic:
exact aux l pairs h
Proof state after:
no goals
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.fst ∈ l
Tactic:
intros p in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l
Tactic:
rw [h] at in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ build_pairs l
⊢ p.fst ∈ l
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ build_pairs l
⊢ p.fst ∈ l
Tactic:
match l with
  | []    => simp [build_pairs] at in_pairs
  | x::xs => simp [build_pairs, build_pairs.pairs] at in_pairs
             cases in_pairs
             rename_i hh
             let ⟨y, t⟩ := hh
             simp
             have right := Eq.symm t.right
             constructor
             simp [right]
             simp [build_pairs, build_pairs.pairs] at h
             simp
             have res := aux xs (build_pairs xs) (by simp) p
             rename_i rr
             simp [res rr]
Proof state after:
no goals
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
h : pairs = build_pairs []
in_pairs : p ∈ build_pairs []
⊢ p.fst ∈ []
Tactic:
simp [build_pairs] at in_pairs
Proof state after:
no goals
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
in_pairs : p ∈ build_pairs (x :: xs)
⊢ p.fst ∈ x :: xs
Tactic:
simp [build_pairs, build_pairs.pairs] at in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
in_pairs : (∃ a, a ∈ xs ∧ (x, a) = p) ∨ p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
in_pairs : (∃ a, a ∈ xs ∧ (x, a) = p) ∨ p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
cases in_pairs
Proof state after:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
rename_i hh
Proof state after:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
let ⟨y, t⟩ := hh
Proof state after:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
simp
Proof state after:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.fst = x ∨ p.fst ∈ xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.fst = x ∨ p.fst ∈ xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
have right := Eq.symm t.right
Proof state after:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
right : p = (x, y)
⊢ p.fst = x ∨ p.fst ∈ xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
right : p = (x, y)
⊢ p.fst = x ∨ p.fst ∈ xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
constructor
Proof state after:
case inl.h
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
right : p = (x, y)
⊢ p.fst = x

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inl.h
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
hh : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
right : p = (x, y)
⊢ p.fst = x

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
simp [right]
Proof state after:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
simp [build_pairs, build_pairs.pairs] at h
Proof state after:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
simp
Proof state after:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
⊢ p.fst = x ∨ p.fst ∈ xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
⊢ p.fst = x ∨ p.fst ∈ xs
Tactic:
have res := aux xs (build_pairs xs) (by simp) p
Proof state after:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.fst ∈ xs
⊢ p.fst = x ∨ p.fst ∈ xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.fst ∈ xs
⊢ p.fst = x ∨ p.fst ∈ xs
Tactic:
rename_i rr
Proof state after:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
rr : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.fst ∈ xs
⊢ p.fst = x ∨ p.fst ∈ xs
Theorem: polynomial.pair_in_list₁
Proof state before:
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
rr : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.fst ∈ xs
⊢ p.fst = x ∨ p.fst ∈ xs
Tactic:
simp [res rr]
Proof state after:
no goals
Theorem: polynomial.pair_in_list₁
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
h✝ : p ∈ build_pairs xs
⊢ build_pairs xs = build_pairs xs
Tactic:
simp
Proof state after:
no goals
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.snd ∈ l
Tactic:
exact aux l pairs h
Proof state after:
no goals
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.snd ∈ l
Tactic:
intros p in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Tactic:
rw [h] at in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ build_pairs l
⊢ p.snd ∈ l
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ build_pairs l
⊢ p.snd ∈ l
Tactic:
match l with
  | []    => simp [build_pairs] at *
  | x::xs => simp [build_pairs] at h in_pairs
             apply Or.elim in_pairs
             intros in_build_pairs
             simp [build_pairs.pairs] at in_build_pairs
             let ⟨y, t⟩ := in_build_pairs
             have left := t.left
             have right := t.right
             simp [Eq.symm right, left]             
             intros in_build_pairs
             simp
             have res := aux xs (build_pairs xs) (by simp) p
             simp [res in_build_pairs]
Proof state after:
no goals
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
h : pairs = build_pairs []
in_pairs : p ∈ build_pairs []
⊢ p.snd ∈ []
Tactic:
simp [build_pairs] at *
Proof state after:
no goals
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
in_pairs : p ∈ build_pairs (x :: xs)
⊢ p.snd ∈ x :: xs
Tactic:
simp [build_pairs] at h in_pairs
Proof state after:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs
Tactic:
apply Or.elim in_pairs
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs.pairs x xs → p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs.pairs x xs → p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
intros in_build_pairs
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs.pairs x xs
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs.pairs x xs
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
simp [build_pairs.pairs] at in_build_pairs
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
let ⟨y, t⟩ := in_build_pairs
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
have left := t.left
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
left : y ∈ xs
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs