[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
l : List α
⊢ Nodup (a :: l) ↔ ¬a ∈ l ∧ Nodup l
[PROOFSTEP]
simp only [Nodup, pairwise_cons, forall_mem_ne]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun x x_1 => x ↔ x_1) (Nodup []) (Nodup [])
[PROOFSTEP]
simp only [nodup_nil]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x x_1 => x ↔ x_1) (Nodup (a✝ :: l₁✝)) (Nodup (b✝ :: l₂✝))
[PROOFSTEP]
simpa only [nodup_cons] using Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → Nodup l
[PROOFSTEP]
induction' l with a l IH
[GOAL]
case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
⊢ (∀ (a : α), ¬[a, a] <+ []) → Nodup []
[PROOFSTEP]
intro h
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → Nodup l
⊢ (∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l) → Nodup (a :: l)
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
h : ∀ (a : α), ¬[a, a] <+ []
⊢ Nodup []
[PROOFSTEP]
exact nodup_nil
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → Nodup l
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ Nodup (a :: l)
[PROOFSTEP]
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons fun al => h a <| (singleton_sublist.2 al).cons_cons _
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : Fin (length l)
hg : get l i = get l j
⊢ i = j
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
j : Fin (length l)
i : ℕ
hi : i < length l
hg : get l { val := i, isLt := hi } = get l j
⊢ { val := i, isLt := hi } = j
[PROOFSTEP]
cases' j with j hj
[GOAL]
case mk.mk
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
[PROOFSTEP]
rcases lt_trichotomy i j with (hij | rfl | hji)
[GOAL]
case mk.mk.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hij : i < j
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
[PROOFSTEP]
exact (h ⟨i, hi⟩ ⟨j, hj⟩ hij hg).elim
[GOAL]
case mk.mk.inr.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
[PROOFSTEP]
exact (h ⟨j, hj⟩ ⟨i, hi⟩ hji hg.symm).elim
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : Nodup l
i j : ℕ
hi : i < length l
hj : j < length l
⊢ i = j → nthLe l i hi = nthLe l j hj
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ Nodup l ↔ ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
[PROOFSTEP]
rw [Nodup, pairwise_iff_get]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) ↔ ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) → ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
[PROOFSTEP]
intro h i j hij hj
[GOAL]
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ get? l i ≠ get? l j
[PROOFSTEP]
rw [get?_eq_get (lt_trans hij hj), get?_eq_get hj, Ne.def, Option.some_inj]
[GOAL]
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ ¬get l { val := i, isLt := (_ : i < length l) } = get l { val := j, isLt := hj }
[PROOFSTEP]
exact h _ _ hij
[GOAL]
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
[PROOFSTEP]
intro h i j hij
[GOAL]
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ get l i ≠ get l j
[PROOFSTEP]
rw [Ne.def, ← Option.some_inj, ← get?_eq_get, ← get?_eq_get]
[GOAL]
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ ¬get? l ↑i = get? l ↑j
[PROOFSTEP]
exact h i j hij j.2
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : Nodup l
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y, y ∈ l ∧ y ≠ x
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x : α
h : Nodup []
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
hl : Nodup tl → (tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x)
h : Nodup (hd :: tl)
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
specialize hl h.of_cons
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
by_cases hx : tl = [x]
[GOAL]
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
simpa [hx, and_comm, and_or_left] using h
[GOAL]
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
rw [← Ne.def, hl] at hx
[GOAL]
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
rcases hx with (rfl | ⟨y, hy, hx⟩)
[GOAL]
case neg.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
h : Nodup [hd]
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x
[PROOFSTEP]
simp
[GOAL]
case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
suffices ∃ (y : α) (_ : y ∈ hd :: tl), y ≠ x by simpa [ne_nil_of_mem hy]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
this : ∃ y x_1, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
[PROOFSTEP]
simpa [ne_nil_of_mem hy]
[GOAL]
case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ y x_1, y ≠ x
[PROOFSTEP]
exact ⟨y, mem_cons_of_mem _ hy, hx⟩
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : Fin (length xs)
h : get xs n = get xs m
hne : n ≠ m
⊢ ¬Nodup xs
[PROOFSTEP]
rw [nodup_iff_injective_get]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : Fin (length xs)
h : get xs n = get xs m
hne : n ≠ m
⊢ ¬Injective (get xs)
[PROOFSTEP]
exact fun hinj => hne (hinj h)
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ¬Nodup xs
[PROOFSTEP]
rw [nodup_iff_nthLe_inj]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ¬∀ (i j : ℕ) (h₁ : i < length xs) (h₂ : j < length xs), nthLe xs i h₁ = nthLe xs j h₂ → i = j
[PROOFSTEP]
simp only [exists_prop, exists_and_right, not_forall]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ∃ x x_1, (∃ x_2 x_3, nthLe xs x (_ : x < length xs) = nthLe xs x_1 (_ : x_1 < length xs)) ∧ ¬x = x_1
[PROOFSTEP]
exact ⟨n, m, ⟨hn, hm, h⟩, hne⟩
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
H : Nodup l
i : Fin (length l)
⊢ get l { val := indexOf (get l i) l, isLt := (_ : indexOf (get l i) l < length l) } = get l i
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
⊢ Nodup (replicate 0 a) ↔ 0 ≤ 1
[PROOFSTEP]
simp [Nat.zero_le]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
⊢ Nodup (replicate 1 a) ↔ 1 ≤ 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
⊢ count a l = if a ∈ l then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : a ∈ l
⊢ count a l = 1
[PROOFSTEP]
exact count_eq_one_of_mem d h
[GOAL]
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : ¬a ∈ l
⊢ count a l = 0
[PROOFSTEP]
exact count_eq_zero_of_not_mem h
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ Nodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂
[PROOFSTEP]
simp only [Nodup, pairwise_append, disjoint_iff_ne]
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁)
[PROOFSTEP]
simp only [nodup_append, and_left_comm, disjoint_comm]
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b a : α
l₁ l₂ : List α
⊢ Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂))
[PROOFSTEP]
simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append, disjoint_cons_right]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d : Nodup (map f l)
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
[PROOFSTEP]
induction' l with hd tl ih
[GOAL]
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
d : Nodup (map f [])
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → f x = f y → x = y
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : Nodup (map f (hd :: tl))
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
[PROOFSTEP]
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.def] at d
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
[PROOFSTEP]
simp only [mem_cons]
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
[PROOFSTEP]
rintro _ (rfl | h₁) _ (rfl | h₂) h₃
[GOAL]
case cons.inl.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f y✝ = f y✝
⊢ y✝ = y✝
[PROOFSTEP]
rfl
[GOAL]
case cons.inl.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ Nodup (map f tl)
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
[PROOFSTEP]
apply (d.1 _ h₂ h₃.symm).elim
[GOAL]
case cons.inr.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
[PROOFSTEP]
apply (d.1 _ h₁ h₃).elim
[GOAL]
case cons.inr.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
[PROOFSTEP]
apply ih d.2 h₁ h₂ h₃
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : Nodup l
⊢ Nodup (List.pmap f l H)
[PROOFSTEP]
rw [pmap_eq_map_attach]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : Nodup l
⊢ Nodup (map (fun x => f ↑x (_ : p ↑x)) (List.attach l))
[PROOFSTEP]
exact h.attach.map fun ⟨a, ha⟩ ⟨b, hb⟩ h => by congr; exact hf a (H _ ha) b (H _ hb) h
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : Nodup l
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h :
  f ↑{ val := a, property := ha } (_ : p ↑{ val := a, property := ha }) =
    f ↑{ val := b, property := hb } (_ : p ↑{ val := b, property := hb })
⊢ { val := a, property := ha } = { val := b, property := hb }
[PROOFSTEP]
congr
[GOAL]
case e_val
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : Nodup l
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h :
  f ↑{ val := a, property := ha } (_ : p ↑{ val := a, property := ha }) =
    f ↑{ val := b, property := hb } (_ : p ↑{ val := b, property := hb })
⊢ a = b
[PROOFSTEP]
exact hf a (H _ ha) b (H _ hb) h
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Bool
l : List α
⊢ Nodup l → Nodup (List.filter p l)
[PROOFSTEP]
simpa using Pairwise.filter (fun a ↦ p a)
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ Pairwise (fun a b => b ≠ a) l ↔ Nodup l
[PROOFSTEP]
simp only [Nodup, Ne.def, eq_comm]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l : List α
d : Nodup l
a : α
⊢ List.erase l a = List.filter (fun x => decide (x ≠ a)) l
[PROOFSTEP]
induction' d with b l m _ IH
[GOAL]
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l : List α
a : α
⊢ List.erase [] a = List.filter (fun x => decide (x ≠ a)) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.erase (b :: l) b = List.filter (fun x => decide (x ≠ b)) (b :: l)
[PROOFSTEP]
rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
[GOAL]
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ ¬decide (b ≠ b) = true
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ l = List.filter (fun x => decide (x ≠ b)) l
[PROOFSTEP]
symm
[GOAL]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ List.filter (fun x => decide (x ≠ b)) l = l
[PROOFSTEP]
rw [filter_eq_self]
[GOAL]
case pos
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l b = List.filter (fun x => decide (x ≠ b)) l
⊢ ∀ (a : α), a ∈ l → decide (a ≠ b) = true
[PROOFSTEP]
simpa [@eq_comm α] using m
[GOAL]
case neg
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ List.erase (b :: l) a = List.filter (fun x => decide (x ≠ a)) (b :: l)
[PROOFSTEP]
rw [erase_cons_tail _ h, filter_cons_of_pos, IH]
[GOAL]
case neg.pa
α : Type u
β : Type v
l✝¹ l₁ l₂ : List α
r : α → α → Prop
a✝¹ b✝ : α
inst✝ : DecidableEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : List.erase l a = List.filter (fun x => decide (x ≠ a)) l
h : ¬b = a
⊢ decide (b ≠ a) = true
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
d : Nodup l
⊢ a ∈ List.erase l b ↔ a ≠ b ∧ a ∈ l
[PROOFSTEP]
rw [d.erase_eq_filter, mem_filter, and_comm, decide_eq_true_iff]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
L : List (List α)
⊢ Nodup (join L) ↔ (∀ (l : List α), l ∈ L → Nodup l) ∧ Pairwise Disjoint L
[PROOFSTEP]
simp only [Nodup, pairwise_join, disjoint_left.symm, forall_mem_ne]
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
l₁ : List α
f : α → List β
⊢ Nodup (List.bind l₁ f) ↔ (∀ (x : α), x ∈ l₁ → Nodup (f x)) ∧ Pairwise (fun a b => Disjoint (f a) (f b)) l₁
[PROOFSTEP]
simp only [List.bind, nodup_join, pairwise_map, and_comm, and_left_comm, mem_map, exists_imp, and_imp]
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔
    Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → Nodup (f x)
[PROOFSTEP]
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x) from
    forall_swap.trans <| forall_congr' fun _ => forall_eq']
[GOAL]
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ map (Prod.mk a₁) l₂
h₂ : x ∈ map (Prod.mk a₂) l₂
⊢ False
[PROOFSTEP]
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
h₂ : (a₁, b₁) ∈ map (Prod.mk a₂) l₂
⊢ False
[PROOFSTEP]
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
[GOAL]
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
mb₂ : b₁ ∈ l₂
⊢ False
[PROOFSTEP]
exact n rfl
[GOAL]
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a✝ b✝ : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a : α
x✝ : a ∈ l₁
b b' : (fun a => σ a) a
h : { fst := a, snd := b } = { fst := a, snd := b' }
⊢ b = b'
[PROOFSTEP]
injection h with _ h
[GOAL]
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ map (Sigma.mk a₁) (l₂ a₁)
h₂ : x ∈ map (Sigma.mk a₂) (l₂ a₂)
⊢ False
[PROOFSTEP]
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₂) (l₂ a₂)
⊢ False
[PROOFSTEP]
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
[GOAL]
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
n : a₁ ≠ a₁
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
mb₂ : b₁ ∈ l₂ a₁
⊢ False
[PROOFSTEP]
exact n rfl
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : b ∈ f a
b' : β
bm' : b' ∈ f a'
e : b = b'
⊢ b' ∈ f a
[PROOFSTEP]
rw [← e]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : b ∈ f a
b' : β
bm' : b' ∈ f a'
e : b = b'
⊢ b ∈ f a
[PROOFSTEP]
exact bm
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
h : ¬a ∈ l
h' : Nodup l
⊢ Nodup (concat l a)
[PROOFSTEP]
rw [concat_eq_append]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
h : ¬a ∈ l
h' : Nodup l
⊢ Nodup (l ++ [a])
[PROOFSTEP]
exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : a ∈ l
⊢ Nodup (List.insert a l)
[PROOFSTEP]
rw [insert_of_mem h']
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : a ∈ l
⊢ Nodup l
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ Nodup (List.insert a l)
[PROOFSTEP]
rw [insert_of_not_mem h', nodup_cons]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ Nodup l
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ ¬a ∈ l
[PROOFSTEP]
assumption
[GOAL]
case right
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ Nodup l
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l₁ : List α
h : Nodup l₂
⊢ Nodup (l₁ ∪ l₂)
[PROOFSTEP]
induction' l₁ with a l₁ ih generalizing l₂
[GOAL]
case nil
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
l₂ : List α
h : Nodup l₂
⊢ Nodup ([] ∪ l₂)
[PROOFSTEP]
exact h
[GOAL]
case cons
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, Nodup l₂ → Nodup (l₁ ∪ l₂)
l₂ : List α
h : Nodup l₂
⊢ Nodup (a :: l₁ ∪ l₂)
[PROOFSTEP]
exact (ih h).insert
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l₁ : List α
x✝ : Nodup l₁
⊢ List.diff l₁ [] = List.filter (fun x => decide ¬x ∈ []) l₁
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : Nodup l₁
⊢ List.diff l₁ (a :: l₂) = List.filter (fun x => decide ¬x ∈ a :: l₂) l₁
[PROOFSTEP]
rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
[GOAL]
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : Nodup l₁
⊢ List.filter (fun a_1 => decide ((decide ¬a_1 ∈ l₂) = true ∧ decide (a_1 ≠ a) = true)) l₁ =
    List.filter (fun x => decide ¬x ∈ a :: l₂) l₁
[PROOFSTEP]
simp only [decide_not, Bool.not_eq_true', decide_eq_false_iff_not, ne_eq, and_comm, Bool.decide_and, find?, mem_cons,
  not_or]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
hl₁ : Nodup l₁
⊢ a ∈ List.diff l₁ l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
[PROOFSTEP]
rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl : Nodup l
f : α → β
x : α
y : β
⊢ map (update f x y) l = if x ∈ l then set (map f l) (indexOf x l) y else map f l
[PROOFSTEP]
induction' l with hd tl ihl
[GOAL]
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hl : Nodup []
⊢ map (update f x y) [] = if x ∈ [] then set (map f []) (indexOf x []) y else map f []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : Nodup (hd :: tl)
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
[PROOFSTEP]
rw [nodup_cons] at hl
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
[PROOFSTEP]
simp only [mem_cons, map, ihl hl.2]
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
[PROOFSTEP]
by_cases H : hd = x
[GOAL]
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
[PROOFSTEP]
subst hd
[GOAL]
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ Nodup tl
⊢ (update f x y x :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then set (f x :: map f tl) (indexOf x (x :: tl)) y else f x :: map f tl
[PROOFSTEP]
simp [set, hl.1]
[GOAL]
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
[PROOFSTEP]
simp [Ne.symm H, H, set, ← apply_ite (cons (f hd))]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
[PROOFSTEP]
classical
refine' pairwise_of_reflexive_on_dupl_of_forall_ne _ h
intro x hx
rw [nodup_iff_count_le_one] at hl
exact absurd (hl x) hx.not_le
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
[PROOFSTEP]
refine' pairwise_of_reflexive_on_dupl_of_forall_ne _ h
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ ∀ (a : α), 1 < count a l → r a a
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
[PROOFSTEP]
rw [nodup_iff_count_le_one] at hl
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl✝ : Nodup l
hl : ∀ (a : α), count a l ≤ 1
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
[PROOFSTEP]
exact absurd (hl x) hx.not_le
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : IsSymm α r
hl : Nodup l
⊢ Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : IsSymm α r
hl✝ : Nodup l
hl : Nodup []
⊢ Set.Pairwise {a | a ∈ []} r ↔ Pairwise r []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : Nodup (a :: l)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
[PROOFSTEP]
rw [List.nodup_cons] at hl
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
[PROOFSTEP]
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb => imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
[GOAL]
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
[PROOFSTEP]
simp [Set.setOf_or, Set.pairwise_insert_of_symmetric (@symm_of _ r _), ih hl.2, and_comm, forall₂_congr this]
[GOAL]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
n : ℕ
x✝ : Nodup []
⊢ take n [] = List.filter (fun x => decide (x ∈ take n [])) []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
x✝ : Nodup (b :: l)
⊢ take 0 (b :: l) = List.filter (fun x => decide (x ∈ take 0 (b :: l))) (b :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ take (n + 1) (b :: l) = List.filter (fun x => decide (x ∈ take (n + 1) (b :: l))) (b :: l)
[PROOFSTEP]
rw [take_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), List.filter_cons_of_pos _ (by simp)]
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ decide (b ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ b :: List.filter (fun x => decide (x ∈ take n l)) l =
    b :: List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
[PROOFSTEP]
congr 1
[GOAL]
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ List.filter (fun x => decide (x ∈ take n l)) l =
    List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
[PROOFSTEP]
refine' List.filter_congr' _
[GOAL]
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ ∀ (x : α),
    x ∈ l → (decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true)
[PROOFSTEP]
intro x hx
[GOAL]
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
[PROOFSTEP]
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
[GOAL]
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
this : x ≠ b
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
[PROOFSTEP]
simp (config := { contextual := true }) [List.mem_filter, this, hx]


[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b a : α
l : List α
p : Chain R a l
⊢ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
[PROOFSTEP]
induction' p with _ a b l r _ IH <;> constructor <;> [exact ⟨mem_cons_self _ _, mem_cons_self _ _, r⟩;
  exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b a : α
l : List α
p : Chain R a l
⊢ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
[PROOFSTEP]
induction' p with _ a b l r _ IH
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b a : α
l : List α
a✝ : α
⊢ Chain (fun x y => x ∈ [a✝] ∧ y ∈ [] ∧ R x y) a✝ []
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u
β : Type v
R r✝ : α → α → Prop
l✝¹ l₁ l₂ : List α
a✝² b✝ a✝¹ : α
l✝ : List α
a b : α
l : List α
r : R a b
a✝ : Chain R b l
IH : Chain (fun x y => x ∈ b :: l ∧ y ∈ l ∧ R x y) b l
⊢ Chain (fun x y => x ∈ a :: b :: l ∧ y ∈ b :: l ∧ R x y) a (b :: l)
[PROOFSTEP]
constructor
[GOAL]
case cons.a
α : Type u
β : Type v
R r✝ : α → α → Prop
l✝¹ l₁ l₂ : List α
a✝² b✝ a✝¹ : α
l✝ : List α
a b : α
l : List α
r : R a b
a✝ : Chain R b l
IH : Chain (fun x y => x ∈ b :: l ∧ y ∈ l ∧ R x y) b l
⊢ a ∈ a :: b :: l ∧ b ∈ b :: l ∧ R a b
[PROOFSTEP]
exact ⟨mem_cons_self _ _, mem_cons_self _ _, r⟩
[GOAL]
case cons.a
α : Type u
β : Type v
R r✝ : α → α → Prop
l✝¹ l₁ l₂ : List α
a✝² b✝ a✝¹ : α
l✝ : List α
a b : α
l : List α
r : R a b
a✝ : Chain R b l
IH : Chain (fun x y => x ∈ b :: l ∧ y ∈ l ∧ R x y) b l
⊢ Chain (fun x y => x ∈ a :: b :: l ∧ y ∈ b :: l ∧ R x y) b l
[PROOFSTEP]
exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ a b : α
⊢ Chain R a [b] ↔ R a b
[PROOFSTEP]
simp only [chain_cons, Chain.nil, and_true_iff]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂
[PROOFSTEP]
induction' l₁ with x l₁ IH generalizing a
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂✝ : List α
a✝¹ b✝ a✝ b : α
l₂ : List α
a : α
⊢ Chain R a ([] ++ b :: l₂) ↔ Chain R a ([] ++ [b]) ∧ Chain R b l₂
[PROOFSTEP]
simp only [*, nil_append, cons_append, Chain.nil, chain_cons, and_true_iff, and_assoc]
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝¹ b✝ a✝ b : α
l₂ : List α
x : α
l₁ : List α
IH : ∀ {a : α}, Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂
a : α
⊢ Chain R a (x :: l₁ ++ b :: l₂) ↔ Chain R a (x :: l₁ ++ [b]) ∧ Chain R b l₂
[PROOFSTEP]
simp only [*, nil_append, cons_append, Chain.nil, chain_cons, and_true_iff, and_assoc]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b c : α
l₁ l₂ : List α
⊢ Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂
[PROOFSTEP]
rw [chain_split, chain_cons]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a✝ b a : α
⊢ Chain R a [] ↔ [] = [] ∨ Forall₂ R (a :: dropLast []) []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
⊢ Chain R a (b :: l) ↔ b :: l = [] ∨ Forall₂ R (a :: dropLast (b :: l)) (b :: l)
[PROOFSTEP]
by_cases h : l = []
[GOAL]
case pos
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
h : l = []
⊢ Chain R a (b :: l) ↔ b :: l = [] ∨ Forall₂ R (a :: dropLast (b :: l)) (b :: l)
[PROOFSTEP]
simp [@chain_iff_forall₂ b l, *]
[GOAL]
case neg
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
h : ¬l = []
⊢ Chain R a (b :: l) ↔ b :: l = [] ∨ Forall₂ R (a :: dropLast (b :: l)) (b :: l)
[PROOFSTEP]
simp [@chain_iff_forall₂ b l, *]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
⊢ Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])
[PROOFSTEP]
simp [chain_iff_forall₂]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b✝ : α
f : β → α
b : β
l : List β
⊢ Chain R (f b) (map f l) ↔ Chain (fun a b => R (f a) (f b)) b l
[PROOFSTEP]
induction l generalizing b
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b✝ : α
f : β → α
b : β
⊢ Chain R (f b) (map f []) ↔ Chain (fun a b => R (f a) (f b)) b []
[PROOFSTEP]
simp only [map, Chain.nil, chain_cons, *]
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b✝ : α
f : β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ {b : β}, Chain R (f b) (map f tail✝) ↔ Chain (fun a b => R (f a) (f b)) b tail✝
b : β
⊢ Chain R (f b) (map f (head✝ :: tail✝)) ↔ Chain (fun a b => R (f a) (f b)) b (head✝ :: tail✝)
[PROOFSTEP]
simp only [map, Chain.nil, chain_cons, *]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a : α
l : List α
hl₁ : Chain R a l
ha : p a
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ Chain S (f a ha) (pmap f l hl₂)
[PROOFSTEP]
induction' l with lh lt l_ih generalizing a
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a✝ : α
l : List α
hl₁✝ : Chain R a✝ l
ha✝ : p a✝
hl₂✝ : ∀ (a : α), a ∈ l → p a
a : α
hl₁ : Chain R a []
ha : p a
hl₂ : ∀ (a : α), a ∈ [] → p a
⊢ Chain S (f a ha) (pmap f [] hl₂)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a✝ : α
l : List α
hl₁✝ : Chain R a✝ l
ha✝ : p a✝
hl₂✝ : ∀ (a : α), a ∈ l → p a
lh : α
lt : List α
l_ih : ∀ {a : α}, Chain R a lt → ∀ (ha : p a) (hl₂ : ∀ (a : α), a ∈ lt → p a), Chain S (f a ha) (pmap f lt hl₂)
a : α
hl₁ : Chain R a (lh :: lt)
ha : p a
hl₂ : ∀ (a : α), a ∈ lh :: lt → p a
⊢ Chain S (f a ha) (pmap f (lh :: lt) hl₂)
[PROOFSTEP]
simp [H _ _ _ _ (rel_of_chain_cons hl₁), l_ih (chain_of_chain_cons hl₁)]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ Chain R a l
[PROOFSTEP]
induction' l with lh lt l_ih generalizing a
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
hl₁ : ∀ (a : α), a ∈ [] → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f [] hl₁)
⊢ Chain R a []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝¹ b : α
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁✝ : ∀ (a : α), a ∈ l → p a
a✝ : α
ha✝ : p a✝
hl₂✝ : Chain S (f a✝ ha✝) (pmap f l hl₁✝)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
lh : α
lt : List α
l_ih : ∀ (hl₁ : ∀ (a : α), a ∈ lt → p a) {a : α} (ha : p a), Chain S (f a ha) (pmap f lt hl₁) → Chain R a lt
hl₁ : ∀ (a : α), a ∈ lh :: lt → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f (lh :: lt) hl₁)
⊢ Chain R a (lh :: lt)
[PROOFSTEP]
simp [H _ _ _ _ (rel_of_chain_cons hl₂), l_ih _ _ (chain_of_chain_cons hl₂)]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ : α
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a' : α), a' ∈ b :: l → R a a'
[PROOFSTEP]
simp only [mem_cons, forall_eq_or_imp, h, true_and_iff]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ : α
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a_1 : α), a_1 ∈ l → R a a_1
[PROOFSTEP]
exact fun c hc => _root_.trans h (rel_of_pairwise_cons hb.pairwise hc)
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Chain R a l₂
h : l₁ <+ l₂
⊢ Chain R a l₁
[PROOFSTEP]
rw [chain_iff_pairwise] at hl ⊢
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l₂)
h : l₁ <+ l₂
⊢ Pairwise R (a :: l₁)
[PROOFSTEP]
exact hl.sublist (h.cons_cons a)
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Chain R a l
hb : b ∈ l
⊢ R a b
[PROOFSTEP]
rw [chain_iff_pairwise] at hl
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b
[PROOFSTEP]
exact rel_of_pairwise_cons hl hb
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
⊢ Chain R a []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
h : 0 < length []
⊢ R a (get [] { val := 0, isLt := h })
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
x✝ : ℕ
h : x✝ < length [] - 1
⊢ R (get [] { val := x✝, isLt := (_ : x✝ < length []) }) (get [] { val := x✝ + 1, isLt := (_ : succ x✝ < length []) })
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ Chain R a (b :: t) ↔
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
rw [chain_cons, @chain_iff_get _ _ t]
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) ↔
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) →
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
rintro ⟨R, ⟨h0, h⟩⟩
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ (∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length (b :: t) - 1),
      R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
        (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })
[PROOFSTEP]
intro _
[GOAL]
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
h✝ : 0 < length (b :: t)
⊢ R✝ a (get (b :: t) { val := 0, isLt := h✝ })
[PROOFSTEP]
exact R
[GOAL]
case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
intro i w
[GOAL]
case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
    (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
[PROOFSTEP]
cases' i with i
[GOAL]
case mp.intro.intro.right.zero
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
w : zero < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := zero, isLt := (_ : zero < length (b :: t)) })
    (get (b :: t) { val := zero + 1, isLt := (_ : succ zero < length (b :: t)) })
[PROOFSTEP]
apply h0
[GOAL]
case mp.intro.intro.right.succ
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := succ i, isLt := (_ : succ i < length (b :: t)) })
    (get (b :: t) { val := succ i + 1, isLt := (_ : succ (succ i) < length (b :: t)) })
[PROOFSTEP]
exact h i (lt_pred_iff.2 <| by simpa using w)
[GOAL]
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ succ i < Nat.sub (length t) 0
[PROOFSTEP]
simpa using w
[GOAL]
case mpr
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ ((∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })) →
    R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
[PROOFSTEP]
rintro ⟨h0, h⟩
[GOAL]
case mpr.intro
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b ∧
    (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length t - 1),
        R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b
[PROOFSTEP]
apply h0
[GOAL]
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ 0 < length (b :: t)
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length t - 1),
      R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.right.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })
[PROOFSTEP]
apply h 0
[GOAL]
case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (i : ℕ) (h : i < length t - 1),
    R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
[PROOFSTEP]
intro i w
[GOAL]
case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
i : ℕ
w : i < length t - 1
⊢ R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
[PROOFSTEP]
exact h (i + 1) (lt_pred_iff.mp w)
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
l : List α
⊢ Chain R a l ↔
    (∀ (h : 0 < length l), R a (nthLe l 0 h)) ∧
      ∀ (i : ℕ) (h : i < length l - 1), R (nthLe l i (_ : i < length l)) (nthLe l (i + 1) (_ : succ i < length l))
[PROOFSTEP]
rw [chain_iff_get]
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
l : List α
⊢ ((∀ (h : 0 < length l), R a (get l { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length l - 1),
        R (get l { val := i, isLt := (_ : i < length l) }) (get l { val := i + 1, isLt := (_ : succ i < length l) })) ↔
    (∀ (h : 0 < length l), R a (nthLe l 0 h)) ∧
      ∀ (i : ℕ) (h : i < length l - 1), R (nthLe l i (_ : i < length l)) (nthLe l (i + 1) (_ : succ i < length l))
[PROOFSTEP]
simp [nthLe]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
l : List α
p : Chain' R l
⊢ Chain' S l
[PROOFSTEP]
cases l <;> [trivial; exact Chain.imp H p]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
l : List α
p : Chain' R l
⊢ Chain' S l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
p : Chain' R []
⊢ Chain' S []
[PROOFSTEP]
trivial
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
head✝ : α
tail✝ : List α
p : Chain' R (head✝ :: tail✝)
⊢ Chain' S (head✝ :: tail✝)
[PROOFSTEP]
exact Chain.imp H p
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
⊢ [] ++ [a, b] ++ l = a :: b :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
x y : α
h : [x, y] <:+: b :: l
⊢ [a] ++ b :: l ++ [] = a :: b :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b✝ b c : α
l₁ l₂ : List α
⊢ Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)
[PROOFSTEP]
rw [chain'_split, chain'_cons]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
f : β → α
l : List β
⊢ Chain' R (map f l) ↔ Chain' (fun a b => R (f a) (f b)) l
[PROOFSTEP]
cases l <;> [rfl; exact chain_map _]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
f : β → α
l : List β
⊢ Chain' R (map f l) ↔ Chain' (fun a b => R (f a) (f b)) l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
f : β → α
⊢ Chain' R (map f []) ↔ Chain' (fun a b => R (f a) (f b)) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
f : β → α
head✝ : β
tail✝ : List β
⊢ Chain' R (map f (head✝ :: tail✝)) ↔ Chain' (fun a b => R (f a) (f b)) (head✝ :: tail✝)
[PROOFSTEP]
exact chain_map _
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Chain' R l₂
h : l₁ <+ l₂
⊢ Chain' R l₁
[PROOFSTEP]
rw [chain'_iff_pairwise] at hl ⊢
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
inst✝ : IsTrans α R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁
[PROOFSTEP]
exact hl.sublist h
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b x : α
l : List α
h : Chain' R (x :: l)
y : α
hy : y ∈ head? l
⊢ R x y
[PROOFSTEP]
rw [← cons_head?_tail hy] at h
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b x : α
l : List α
y : α
h : Chain' R (x :: y :: List.tail l)
hy : y ∈ head? l
⊢ R x y
[PROOFSTEP]
exact h.rel_head
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
⊢ Chain' R ([] ++ l) ↔ Chain' R [] ∧ Chain' R l ∧ ∀ (x : α), x ∈ getLast? [] → ∀ (y : α), y ∈ head? l → R x y
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b a : α
l : List α
⊢ Chain' R ([a] ++ l) ↔ Chain' R [a] ∧ Chain' R l ∧ ∀ (x : α), x ∈ getLast? [a] → ∀ (y : α), y ∈ head? l → R x y
[PROOFSTEP]
simp [chain'_cons', and_comm]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ Chain' R (a :: b :: l₁ ++ l₂) ↔
    Chain' R (a :: b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (a :: b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y
[PROOFSTEP]
rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, and_assoc]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ (R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y) ↔
    R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ getLast? (a :: b :: l₁) → ∀ (y : α), y ∈ head? l₂ → R x y
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Chain' R l
h' : l₁ <:+: l
⊢ Chain' R l₁
[PROOFSTEP]
rcases h' with ⟨l₂, l₃, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l₁ l₂✝ : List α
a b : α
l₂ l₃ : List α
h : Chain' R (l₂ ++ l₁ ++ l₃)
⊢ Chain' R l₁
[PROOFSTEP]
exact h.left_of_append.right_of_append
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b x y : α
⊢ Chain' R [x, y] ↔ R x y
[PROOFSTEP]
simp only [chain'_singleton, chain'_cons, and_true_iff]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a✝ b a : α
⊢ Chain' R (reverse [a]) ↔ Chain' (flip R) [a]
[PROOFSTEP]
simp only [chain'_singleton, reverse_singleton]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
⊢ Chain' R (reverse (a :: b :: l)) ↔ Chain' (flip R) (a :: b :: l)
[PROOFSTEP]
rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append, chain'_split, ← reverse_cons,
  @chain'_reverse (b :: l), and_comm, chain'_pair, flip]
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a b : α
R : α → α → Prop
⊢ Chain' R []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a b : α
R : α → α → Prop
x✝ : ℕ
h : x✝ < length [] - 1
⊢ R (get [] { val := x✝, isLt := (_ : x✝ < length []) }) (get [] { val := x✝ + 1, isLt := (_ : succ x✝ < length []) })
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
⊢ Chain' R [a]
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
x✝ : ℕ
h : x✝ < length [a] - 1
⊢ R (get [a] { val := x✝, isLt := (_ : x✝ < length [a]) })
    (get [a] { val := x✝ + 1, isLt := (_ : succ x✝ < length [a]) })
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ Chain' R (a :: b :: t) ↔
    ∀ (i : ℕ) (h : i < length (a :: b :: t) - 1),
      R (get (a :: b :: t) { val := i, isLt := (_ : i < length (a :: b :: t)) })
        (get (a :: b :: t) { val := i + 1, isLt := (_ : succ i < length (a :: b :: t)) })
[PROOFSTEP]
rw [← and_forall_succ, chain'_cons, chain'_iff_get]
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })) ↔
    (∀ (h : 0 < length (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := 0, isLt := (_ : 0 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := 0 + 1, isLt := (_ : succ 0 < length (a :: b :: t)) })) ∧
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := n + 1, isLt := (_ : n + 1 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := n + 1 + 1, isLt := (_ : succ (n + 1) < length (a :: b :: t)) })
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get t { val := i, isLt := (_ : i < length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (b :: t) { val := n, isLt := (_ : n < length (b :: t)) })
          (get t { val := n, isLt := (_ : n < length t) }))
[PROOFSTEP]
dsimp [succ_sub_one]
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length t),
        R (get (b :: t) { val := i, isLt := (_ : i < succ (length t)) })
          (get t { val := i, isLt := (_ : succ i ≤ length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length t + 1),
        R (get (b :: t) { val := n, isLt := (_ : succ n ≤ length (b :: t)) })
          (get t { val := n, isLt := (_ : succ n ≤ length t) }))
[PROOFSTEP]
exact fun _ => ⟨fun h i hi => h i (Nat.lt_of_succ_lt_succ hi), fun h i hi => h i (Nat.succ_lt_succ hi)⟩
[GOAL]
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
R : α → α → Prop
l : List α
⊢ (∀ (i : ℕ) (h : i < length l - 1),
      R (get l { val := i, isLt := (_ : i < length l) }) (get l { val := i + 1, isLt := (_ : succ i < length l) })) ↔
    ∀ (i : ℕ) (h : i < length l - 1), R (nthLe l i (_ : i < length l)) (nthLe l (i + 1) (_ : succ i < length l))
[PROOFSTEP]
simp [nthLe]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ l₃ : List α
h₁ : Chain' R (l₁ ++ l₂)
h₂ : Chain' R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ getLast? (l₁ ++ l₂) → ∀ (y : α), y ∈ head? l₃ → R x y
[PROOFSTEP]
simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
x✝ : ¬[] ∈ []
⊢ Chain' R (join []) ↔
    (∀ (l : List α), l ∈ [] → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
x✝ : ¬[] ∈ [l]
⊢ Chain' R (join [l]) ↔
    (∀ (l_1 : List α), l_1 ∈ [l] → Chain' R l_1) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) [l]
[PROOFSTEP]
simp [join]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ Chain' R (join (l₁ :: l₂ :: L)) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₁ :: l₂ :: L)
[PROOFSTEP]
rw [mem_cons, not_or, ← Ne.def] at hL
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ Chain' R (join (l₁ :: l₂ :: L)) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₁ :: l₂ :: L)
[PROOFSTEP]
rw [join, chain'_append, chain'_join hL.2, forall_mem_cons, chain'_cons]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? (join (l₂ :: L)) → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L)
[PROOFSTEP]
rw [mem_cons, not_or, ← Ne.def] at hL
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? (join (l₂ :: L)) → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧
      (∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) ∧
        Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L)
[PROOFSTEP]
simp only [forall_mem_cons, and_assoc, join, head?_append_of_ne_nil _ hL.2.1.symm]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) ↔
    Chain' R l₁ ∧
      Chain' R l₂ ∧
        (∀ (x : List α), x ∈ L → Chain' R x) ∧
          (∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) ∧
            Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ getLast? l₁ → ∀ (y : α), y ∈ head? l₂ → R x y) (l₂ :: L)
[PROOFSTEP]
exact Iff.rfl.and (Iff.rfl.and $ Iff.rfl.and and_comm)
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r a l ∧ getLast (a :: l) (_ : a :: l ≠ []) = b
[PROOFSTEP]
refine' Relation.ReflTransGen.head_induction_on h _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r b l ∧ getLast (b :: l) (_ : b :: l ≠ []) = b
[PROOFSTEP]
exact ⟨[], Chain.nil, rfl⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b) →
          ∃ l, Chain r a l ∧ getLast (a :: l) (_ : a :: l ≠ []) = b
[PROOFSTEP]
intro c d e _ ih
[GOAL]
case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, Chain r d l ∧ getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
[PROOFSTEP]
obtain ⟨l, hl₁, hl₂⟩ := ih
[GOAL]
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
[PROOFSTEP]
refine' ⟨d :: l, Chain.cons e hl₁, _⟩
[GOAL]
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ getLast (c :: d :: l) (_ : c :: d :: l ≠ []) = b
[PROOFSTEP]
rwa [getLast_cons_cons]
[GOAL]
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : getLast (a :: l) (_ : a :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ ∀ (i : α), i ∈ a :: l → p i
[PROOFSTEP]
induction' l with _ _ l_ih generalizing a
[GOAL]
case nil
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
a : α
h : Chain r a []
hb : getLast [a] (_ : [a] ≠ []) = b
⊢ ∀ (i : α), i ∈ [a] → p i
[PROOFSTEP]
cases hb
[GOAL]
case nil.refl
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
a : α
h : Chain r a []
hb : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = getLast [a] (_ : [a] ≠ [])
final : p (getLast [a] (_ : [a] ≠ []))
⊢ ∀ (i : α), i ∈ [a] → p i
[PROOFSTEP]
simpa using final
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
a : α
h : Chain r a (head✝ :: tail✝)
hb : getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = b
⊢ ∀ (i : α), i ∈ a :: head✝ :: tail✝ → p i
[PROOFSTEP]
rw [chain_cons] at h
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
a : α
h : r a head✝ ∧ Chain r head✝ tail✝
hb : getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = b
⊢ ∀ (i : α), i ∈ a :: head✝ :: tail✝ → p i
[PROOFSTEP]
simp only [mem_cons]
[GOAL]
case cons
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
a : α
h : r a head✝ ∧ Chain r head✝ tail✝
hb : getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = b
⊢ ∀ (i : α), i = a ∨ i = head✝ ∨ i ∈ tail✝ → p i
[PROOFSTEP]
rintro _ (rfl | H)
[GOAL]
case cons.inl
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
p : α → Prop
l : List α
h✝ : Chain r a l
hb✝ : getLast (a :: l) (_ : a :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
i✝ : α
h : r i✝ head✝ ∧ Chain r head✝ tail✝
hb : getLast (i✝ :: head✝ :: tail✝) (_ : i✝ :: head✝ :: tail✝ ≠ []) = b
⊢ p i✝
case cons.inr
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
a : α
h : r a head✝ ∧ Chain r head✝ tail✝
hb : getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = b
i✝ : α
H : i✝ = head✝ ∨ i✝ ∈ tail✝
⊢ p i✝
[PROOFSTEP]
apply carries h.1 (l_ih h.2 hb _ (mem_cons.2 (Or.inl rfl)))
[GOAL]
case cons.inr
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
p : α → Prop
l : List α
h✝ : Chain r a✝ l
hb✝ : getLast (a✝ :: l) (_ : a✝ :: l ≠ []) = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
head✝ : α
tail✝ : List α
l_ih : ∀ {a : α}, Chain r a tail✝ → getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = b → ∀ (i : α), i ∈ a :: tail✝ → p i
a : α
h : r a head✝ ∧ Chain r head✝ tail✝
hb : getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = b
i✝ : α
H : i✝ = head✝ ∨ i✝ ∈ tail✝
⊢ p i✝
[PROOFSTEP]
apply l_ih h.2 hb _ (mem_cons.2 H)
[GOAL]
α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ List.head? ↑l → Acc r a
⊢ Acc (List.lex_chains r) l
[PROOFSTEP]
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
[GOAL]
case mk.nil
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ List.head? ↑{ val := [], property := hl } → Acc r a
⊢ Acc (List.lex_chains r) { val := [], property := hl }
[PROOFSTEP]
apply Acc.intro
[GOAL]
case mk.nil.h
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ List.head? ↑{ val := [], property := hl } → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y { val := [], property := hl } → Acc (List.lex_chains r) y
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ List.head? ↑{ val := a :: l, property := hl } → Acc r a_1
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
specialize acc a _
[GOAL]
case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ List.head? ↑{ val := a :: l, property := hl } → Acc r a_1
⊢ a ∈ List.head? ↑{ val := a :: l, property := hl }
[PROOFSTEP]
rw [List.head?_cons, Option.mem_some_iff]
  /- For an r-decreasing chain of the form a :: l, apply induction on a -/
[GOAL]
case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : Acc r a
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
induction acc generalizing l with
| intro a _ ih =>
  /- Bundle l with a proof that it is r-decreasing to form l' -/
  have hl' := (List.chain'_cons'.1 hl).2
  let l' : List.chains r := ⟨l, hl'⟩
  have : Acc (List.lex_chains r) l'
  · cases' l with b l
    · apply Acc.intro;
      rintro ⟨_⟩
        ⟨_⟩
            /- l' is accessible by induction hypothesis -/
    ·
      apply
        ih b
          (List.chain'_cons.1 hl).1
            /- make l' a free variable and induct on l' -/
  revert hl
  rw [(by rfl : l = l'.1)]
  clear_value l'
  induction this with
  | intro l _ ihl =>
    intro hl
    apply Acc.intro
    rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
    · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
    · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
    · apply ih b hr
[GOAL]
case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : Acc r a
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
induction acc generalizing l with
| intro a _ ih =>
  /- Bundle l with a proof that it is r-decreasing to form l' -/
  have hl' := (List.chain'_cons'.1 hl).2
  let l' : List.chains r := ⟨l, hl'⟩
  have : Acc (List.lex_chains r) l'
  · cases' l with b l
    · apply Acc.intro;
      rintro ⟨_⟩
        ⟨_⟩
            /- l' is accessible by induction hypothesis -/
    ·
      apply
        ih b
          (List.chain'_cons.1 hl).1
            /- make l' a free variable and induct on l' -/
  revert hl
  rw [(by rfl : l = l'.1)]
  clear_value l'
  induction this with
  | intro l _ ihl =>
    intro hl
    apply Acc.intro
    rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
    · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
    · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
    · apply ih b hr
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]

| intro a _ ih =>
  /- Bundle l with a proof that it is r-decreasing to form l' -/
  have hl' := (List.chain'_cons'.1 hl).2
  let l' : List.chains r := ⟨l, hl'⟩
  have : Acc (List.lex_chains r) l'
  · cases' l with b l
    · apply Acc.intro;
      rintro ⟨_⟩
        ⟨_⟩
            /- l' is accessible by induction hypothesis -/
    ·
      apply
        ih b
          (List.chain'_cons.1 hl).1
            /- make l' a free variable and induct on l' -/
  revert hl
  rw [(by rfl : l = l'.1)]
  clear_value l'
  induction this with
  | intro l _ ihl =>
    intro hl
    apply Acc.intro
    rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
    · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
    · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
    · apply ih b hr
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
have hl' := (List.chain'_cons'.1 hl).2
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
let l' : List.chains r := ⟨l, hl'⟩
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
have : Acc (List.lex_chains r) l'
[GOAL]
case this
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
⊢ Acc (List.lex_chains r) l'
[PROOFSTEP]
cases' l with b l
[GOAL]
case this.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := { val := [], property := hl' }
⊢ Acc (List.lex_chains r) l'
[PROOFSTEP]
apply Acc.intro
[GOAL]
case this.nil.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := { val := [], property := hl' }
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y
[PROOFSTEP]
rintro ⟨_⟩
  ⟨_⟩
      /- l' is accessible by induction hypothesis -/
[GOAL]
case this.cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
b : α
l : List α
hl : List.Chain' (flip r) (a :: b :: l)
hl' : List.Chain' (flip r) (b :: l)
l' : List.chains r := { val := b :: l, property := hl' }
⊢ Acc (List.lex_chains r) l'
[PROOFSTEP]
apply
  ih b
    (List.chain'_cons.1 hl).1
      /- make l' a free variable and induct on l' -/
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
this : Acc (List.lex_chains r) l'
⊢ Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
revert hl
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: l)), Acc (List.lex_chains r) { val := a :: l, property := hl }
[PROOFSTEP]
rw [(by rfl : l = l'.1)]
[GOAL]
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
this : Acc (List.lex_chains r) l'
⊢ l = ↑l'
[PROOFSTEP]
rfl
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := { val := l, property := hl' }
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l')), Acc (List.lex_chains r) { val := a :: ↑l', property := hl }
[PROOFSTEP]
clear_value l'
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l')), Acc (List.lex_chains r) { val := a :: ↑l', property := hl }
[PROOFSTEP]
induction this with
| intro l _ ihl =>
  intro hl
  apply Acc.intro
  rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
  · apply ih b hr
[GOAL]
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l')), Acc (List.lex_chains r) { val := a :: ↑l', property := hl }
[PROOFSTEP]
induction this with
| intro l _ ihl =>
  intro hl
  apply Acc.intro
  rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
  · apply ih b hr
[GOAL]
case mk.cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l)), Acc (List.lex_chains r) { val := a :: ↑l, property := hl }
[PROOFSTEP]

| intro l _ ihl =>
  intro hl
  apply Acc.intro
  rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
  · apply ih b hr
[GOAL]
case mk.cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l)), Acc (List.lex_chains r) { val := a :: ↑l, property := hl }
[PROOFSTEP]
intro hl
[GOAL]
case mk.cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
⊢ Acc (List.lex_chains r) { val := a :: ↑l, property := hl }
[PROOFSTEP]
apply Acc.intro
[GOAL]
case mk.cons.intro.intro.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
⊢ ∀ (y : List.chains r), List.lex_chains r y { val := a :: ↑l, property := hl } → Acc (List.lex_chains r) y
[PROOFSTEP]
rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
[GOAL]
case mk.cons.intro.intro.h.mk.nil.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
hm : List.Chain' (flip r) []
⊢ Acc (List.lex_chains r) { val := [], property := hm }
[PROOFSTEP]
apply Acc.intro
[GOAL]
case mk.cons.intro.intro.h.mk.nil.nil.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
hm : List.Chain' (flip r) []
⊢ ∀ (y : List.chains r), List.lex_chains r y { val := [], property := hm } → Acc (List.lex_chains r) y
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.cons.intro.intro.h.mk.cons.cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
m : List α
hm : List.Chain' (flip r) (a :: m)
hr : List.Lex r m ↑l
⊢ Acc (List.lex_chains r) { val := a :: m, property := hm }
[PROOFSTEP]
apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
[GOAL]
case mk.cons.intro.intro.h.mk.cons.rel
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) { val := y :: l, property := hl }
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l →
      ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) { val := a :: ↑y, property := hl }
hl : List.Chain' (flip r) (a :: ↑l)
b : α
m : List α
hm : List.Chain' (flip r) (b :: m)
hr : r b a
⊢ Acc (List.lex_chains r) { val := b :: m, property := hm }
[PROOFSTEP]
apply ih b hr