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
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.fst ∈ 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.fst ∈ 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.fst ∈ 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.fst ∈ 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.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]
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.fst ∈ []
Tactic:
simp [build_pairs] at in_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 (x :: xs)
in_pairs : p ∈ build_pairs (x :: xs)
⊢ p.fst ∈ x :: xs
Tactic:
simp [build_pairs, build_pairs.pairs] at 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 (x :: xs)
in_pairs : (∃ a, a ∈ xs ∧ (x, a) = p) ∨ p ∈ build_pairs xs
⊢ p.fst ∈ 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 (x :: xs)
in_pairs : (∃ a, a ∈ xs ∧ (x, a) = p) ∨ p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
Tactic:
cases in_pairs
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

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

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

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

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

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

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

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

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

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

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

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