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.fst ∈ l ∧ p.snd ∈ l
Tactic:
intros p in_pairs
State after:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l ∧ p.snd ∈ l

State before:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l ∧ p.snd ∈ l
Tactic:
constructor
State after:
case left
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l

case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l

State before:
case left
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l

case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Tactic:
exact pair_in_list₁ l pairs h p in_pairs
State after:
case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l

State before:
case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Tactic:
exact pair_in_list₂ l pairs h p in_pairs
State after:
no goals