Theorem: polynomial.pair_in_list₂ (Diploma/Polynomials/Groebner.lean)

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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 *
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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
Tactic:
have right := t.right
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
right : (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

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
left : y ∈ xs
right : (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:
simp [Eq.symm right, left]
State after:
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

State before:
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
State after:
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
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs

State before:
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
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs
Tactic:
simp
State after:
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
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd = x ∨ p.snd ∈ xs

State before:
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
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd = x ∨ p.snd ∈ xs
Tactic:
have res := aux xs (build_pairs xs) (by simp) p
State after:
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
in_build_pairs : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.snd ∈ xs
⊢ p.snd = x ∨ p.snd ∈ xs

State before:
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
in_build_pairs : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.snd ∈ xs
⊢ p.snd = x ∨ p.snd ∈ xs
Tactic:
simp [res in_build_pairs]
State after:
no goals

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
in_build_pairs : p ∈ build_pairs xs
⊢ build_pairs xs = build_pairs xs
Tactic:
simp
State after:
no goals