Theorem: List.Nodup.product (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
la : List α
lb : List β
la_nodup : Nodup la
lb_nodup : Nodup lb
⊢ Nodup (List.product la lb)
Tactic:
induction la with
| nil => exact .nil
| cons a la IH =>
  specialize IH la_nodup.tail
  conv =>
    arg 1
    dsimp [List.product, List.bind]
    change lb.map (Prod.mk a) ++ la.product lb
  refine Nodup.append ?_ IH ?_
  . apply lb_nodup.map
    intro b₁ b₂; exact congrArg Prod.snd
  . intro x
    let ⟨_,b⟩ := x
    simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
    intro _ ha h; cases ha
    exact la_nodup.head h.1
State after:
no goals

State before:
case nil
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
la_nodup : Nodup []
⊢ Nodup (List.product [] lb)
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
IH : Nodup la → Nodup (List.product la lb)
la_nodup : Nodup (a :: la)
⊢ Nodup (List.product (a :: la) lb)
Tactic:
specialize IH la_nodup.tail
State after:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.product (a :: la) lb)

State before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.product (a :: la) lb)
Tactic:
conv =>
  arg 1
  dsimp [List.product, List.bind]
  change lb.map (Prod.mk a) ++ la.product lb
State after:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb ++ List.product la lb)

State before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb ++ List.product la lb)
Tactic:
refine Nodup.append ?_ IH ?_
State after:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)

case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb

State before:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)

case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
. apply lb_nodup.map
  intro b₁ b₂; exact congrArg Prod.snd
State after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
. intro x
  let ⟨_,b⟩ := x
  simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
  intro _ ha h; cases ha
  exact la_nodup.head h.1
State after:
no goals

State before:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)
Tactic:
apply lb_nodup.map
State after:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a₁ a₂ : β), (a, a₁) = (a, a₂) → a₁ = a₂

State before:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a₁ a₂ : β), (a, a₁) = (a, a₂) → a₁ = a₂
Tactic:
intro b₁ b₂
State after:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂

State before:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂
Tactic:
exact congrArg Prod.snd
State after:
no goals

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
intro x
State after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
⊢ x ∈ List.map (Prod.mk a) lb → ¬x ∈ List.product la lb

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
⊢ x ∈ List.map (Prod.mk a) lb → ¬x ∈ List.product la lb
Tactic:
let ⟨_,b⟩ := x
State after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ (fst✝, b) ∈ List.map (Prod.mk a) lb → ¬(fst✝, b) ∈ List.product la lb

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ (fst✝, b) ∈ List.map (Prod.mk a) lb → ¬(fst✝, b) ∈ List.product la lb
Tactic:
simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
State after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ b ∈ lb → a = fst✝ → ¬(fst✝ ∈ la ∧ b ∈ lb)

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ b ∈ lb → a = fst✝ → ¬(fst✝ ∈ la ∧ b ∈ lb)
Tactic:
intro _ ha h
State after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
a✝ : b ∈ lb
ha : a = fst✝
h : fst✝ ∈ la ∧ b ∈ lb
⊢ False

State before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
a✝ : b ∈ lb
ha : a = fst✝
h : fst✝ ∈ la ∧ b ∈ lb
⊢ False
Tactic:
cases ha
State after:
case cons.refine_2.refl
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
b : β
a✝ : b ∈ lb
h : a ∈ la ∧ b ∈ lb
⊢ False

State before:
case cons.refine_2.refl
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
b : β
a✝ : b ∈ lb
h : a ∈ la ∧ b ∈ lb
⊢ False
Tactic:
exact la_nodup.head h.1
State after:
no goals