[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).fst = y :: ys ++ ts
[PROOFSTEP]
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).snd =
    f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x => f (y :: x)).snd
[PROOFSTEP]
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd
[PROOFSTEP]
induction ys generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd ++ r = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd ++ r = (permutationsAux2 t ts r (head✝ :: tail✝) f).snd
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd
[PROOFSTEP]
induction' ys with ys_hd _ ys_ih generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ : List α → β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd
[PROOFSTEP]
simp [ys_ih fun xs => f (ys_hd :: xs)]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd
[PROOFSTEP]
induction' ys with ys_hd _ ys_ih generalizing f f'
[GOAL]
case nil
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd
[PROOFSTEP]
simp
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail✝)) f').snd
[PROOFSTEP]
simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (permutationsAux2 t ts r tail✝ fun x => f (ys_hd :: x)).fst)) =
      f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail✝ fun x => f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x => f' (g ys_hd :: x)).snd
[PROOFSTEP]
rw [ys_ih, permutationsAux2_fst]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) ?cons.f').snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x => f' (g ys_hd :: x)).snd
case cons.f'
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ List α' → β'
case cons.f'
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ List α' → β'
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = ?cons.f' (map g a)
[PROOFSTEP]
refine' ⟨_, rfl⟩
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts))
[PROOFSTEP]
simp only [← map_cons, ← map_append]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (map g (t :: ys_hd :: (tail✝ ++ ts)))
[PROOFSTEP]
apply H
[GOAL]
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
[PROOFSTEP]
intro a
[GOAL]
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd
[PROOFSTEP]
rw [map_permutationsAux2' id, map_id, map_id]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys ?f').snd = (permutationsAux2 t ts [] ys f).snd
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case H α : Type u_1 β : Type u_2 t : α ts ys : List α f : List α → β ⊢ ∀ (a : List α), f (id a) = ?f' (map id a)
[PROOFSTEP]
rfl
[GOAL]
case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun x => f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
[PROOFSTEP]
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
[PROOFSTEP]
induction' ts with a ts ih <;> [rfl; (simp [← ih]; rfl)]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
[PROOFSTEP]
induction' ts with a ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
f : α → β
t : α
⊢ map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f) (permutations'Aux t (a :: ts)) = permutations'Aux (f t) (map f (a :: ts))
[PROOFSTEP]
simp [← ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f ∘ cons a) (permutations'Aux t ts) = map (cons (f a) ∘ map f) (permutations'Aux t ts)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
[PROOFSTEP]
induction' ts with a ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
[PROOFSTEP]
simp [permutations'Aux, permutationsAux2_snd_cons, ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).snd
[PROOFSTEP]
simp (config := { singlePass := true }) only [← permutationsAux2_append]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).snd ++ [a :: (ts ++ [t])]
[PROOFSTEP]
simp [map_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l l' : List α
⊢ l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
induction' ys with y ys ih generalizing l
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts l✝ l' l : List α
⊢ l' ∈ (permutationsAux2 t ts [] [] fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ [] = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (permutationsAux2 t ts [] (y :: ys) fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [permutationsAux2_snd_cons, show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by funext _; simp, mem_cons, ih]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (fun x => l ++ y :: x) = fun x => l ++ [y] ++ x
[PROOFSTEP]
funext _
[GOAL]
case h
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l x✝ : List α
⊢ l ++ y :: x✝ = l ++ [y] ++ x✝
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
[GOAL]
case cons.mp.inl
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
exact ⟨[], y :: ys, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ y :: ys ≠ [] ∧ y :: ys = [] ++ y :: ys ∧ l ++ (t :: y :: ys ++ ts) = l ++ [] ++ t :: y :: ys ++ ts
[PROOFSTEP]
simp
[GOAL]
case cons.mp.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ ∃ l₁_1 l₂_1,
    l₂_1 ≠ [] ∧ y :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
exact ⟨y :: l₁, l₂, l0, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ y :: (l₁ ++ l₂) = y :: l₁ ++ l₂ ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ y :: l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp
[GOAL]
case cons.mpr
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
[GOAL]
case cons.mpr.intro.nil.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = [] ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ [] ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l_1 ++ l₁ ++ t :: l₂_1 ++ ts
⊢ l ++ [] ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂_1 ++ ts
[PROOFSTEP]
simp [ye]
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: l₁ ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
simp only [cons_append] at ye
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: (l₁ ++ l₂)
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
rcases ye with ⟨rfl, rfl⟩
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro.refl
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ y :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: (l₁ ++ l₂) ++ ts) ∨
    ∃ l₁_1 l₂_1,
      l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
exact Or.inr ⟨l₁, l₂, l0, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ y :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys id).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [show @id (List α) = ([] ++ ·) by funext _; rfl]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ id = fun x => [] ++ x
[PROOFSTEP]
funext _
[GOAL]
case h
α : Type u_1
β : Type u_2
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
apply mem_permutationsAux2
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ length (permutationsAux2 t ts [] ys f).snd = length ys
[PROOFSTEP]
induction ys generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
f : List α → β
⊢ length (permutationsAux2 t ts [] [] f).snd = length []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), length (permutationsAux2 t ts [] tail✝ f).snd = length tail✝
f : List α → β
⊢ length (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd = length (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
induction' L with l L ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r [] =
    (List.bind [] fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r (l :: L) =
    (List.bind (l :: L) fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
simp [ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ (permutationsAux2 t ts ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r)
[PROOFSTEP]
rw [← permutationsAux2_append]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
have :
  (∃ a : List α, a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
  ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ => ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [foldr_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_bind, append_assoc, cons_append,
  exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
⊢ length (foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L) = sum (map length L) + length r
[PROOFSTEP]
simp [foldr_permutationsAux2, (· ∘ ·), length_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ length (foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L) = n * length L + length r
[PROOFSTEP]
rw [length_foldr_permutationsAux2, (_ : List.sum (map length L) = n * length L)]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ sum (map length L) = n * length L
[PROOFSTEP]
induction' L with l L ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L → length l = n
H : ∀ (l : List α), l ∈ [] → length l = n
⊢ sum (map length []) = n * length []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
have sum_map : sum (map length L) = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
have length_l : length l = n := H _ (mem_cons_self _ _)
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
length_l : length l = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
simp [sum_map, length_l, mul_add, add_comm, mul_succ]
[GOAL]
α : Type u_1
β : Type u_2
is : List α
⊢ permutationsAux [] is = []
[PROOFSTEP]
rw [permutationsAux, permutationsAux.rec]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts is : List α
⊢ permutationsAux (t :: ts) is =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd) (permutationsAux ts (t :: is)) (permutations is)
[PROOFSTEP]
rw [permutationsAux, permutationsAux.rec]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (permutations is)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
⊢ permutations [] = [[]]
[PROOFSTEP]
rw [permutations, permutationsAux_nil]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is)
[PROOFSTEP]
refine' permutationsAux.rec (by simp) _
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (is : List α), map (map f) (permutationsAux [] is) = permutationsAux (map f []) (map f is)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is)) →
      map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f []) →
        map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
introv IH1 IH2
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f [])
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
rw [map] at IH2
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) []
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations, bind_map, IH1, append_assoc,
  permutationsAux_cons, cons_bind, ← IH2, map_bind]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations ts) = permutations (map f ts)
[PROOFSTEP]
rw [permutations, permutations, map, map_permutationsAux, map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations' ts) = permutations' (map f ts)
[PROOFSTEP]
induction' ts with t ts ih <;> [rfl; simp [← ih, map_bind, ← map_map_permutations'Aux, bind_map]]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations' ts) = permutations' (map f ts)
[PROOFSTEP]
induction' ts with t ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ map (map f) (permutations' []) = permutations' (map f [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
ih : map (map f) (permutations' ts) = permutations' (map f ts)
⊢ map (map f) (permutations' (t :: ts)) = permutations' (map f (t :: ts))
[PROOFSTEP]
simp [← ih, map_bind, ← map_map_permutations'Aux, bind_map]
[GOAL]
α : Type u_1
β : Type u_2
is is' ts : List α
⊢ permutationsAux (is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
[PROOFSTEP]
induction' is with t is ih generalizing is'
[GOAL]
case nil
α : Type u_1
β : Type u_2
is'✝ ts is' : List α
⊢ permutationsAux ([] ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux [] is') ++ permutationsAux ts (reverse [] ++ is')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ permutationsAux (t :: is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux (t :: is) is') ++ permutationsAux ts (reverse (t :: is) ++ is')
[PROOFSTEP]
simp only [foldr_permutationsAux2, ih, bind_map, cons_append, permutationsAux_cons, map_append, reverse_cons,
  append_assoc, singleton_append]
[GOAL]
case cons
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (List.bind (permutations is') fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: is')) =
    (List.bind (permutations is') fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: ([] ++ is')))
[PROOFSTEP]
congr 2
[GOAL]
case cons.e_a.e_b
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) = fun a =>
    map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd
[PROOFSTEP]
funext _
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).snd
[PROOFSTEP]
rw [map_permutationsAux2]
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = (permutationsAux2 t is [] x✝ fun x => x ++ ts).snd
[PROOFSTEP]
simp (config := { singlePass := true }) only [← permutationsAux2_comp_append]
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).snd =
    (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).snd
[PROOFSTEP]
simp only [id, append_assoc]
[GOAL]
α : Type u_1
β : Type u_2
is ts : List α
⊢ permutations (is ++ ts) = map (fun x => x ++ ts) (permutations is) ++ permutationsAux ts (reverse is)
[PROOFSTEP]
simp [permutations, permutationsAux_append]


[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n l = List.oldMapIdx (fun i a => f (i + n) a) l
[PROOFSTEP]
induction' l with hd tl hl generalizing f n
[GOAL]
case nil
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)
[PROOFSTEP]
rw [List.oldMapIdx]
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)
[PROOFSTEP]
simp only [List.oldMapIdxCore, hl, add_left_comm, add_comm, add_zero, zero_add]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
⊢ ∀ (l : List α), p l
[PROOFSTEP]
let q := fun l ↦ p (reverse l)
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p l
[PROOFSTEP]
have pq : ∀ l, p (reverse l) → q l := by simp only [reverse_reverse]; intro; exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → q l
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → p (reverse l)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
l✝ : List α
⊢ p (reverse l✝) → p (reverse l✝)
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l
[PROOFSTEP]
have qp : ∀ l, q (reverse l) → p l := by simp only [reverse_reverse]; intro; exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), q (reverse l) → p l
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l → p l
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
l✝ : List α
⊢ p l✝ → p l✝
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
⊢ ∀ (l : List α), p l
[PROOFSTEP]
intro l
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p l
[PROOFSTEP]
apply qp
[GOAL]
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q (reverse l)
[PROOFSTEP]
generalize (reverse l) = l
[GOAL]
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l✝ l : List α
⊢ q l
[PROOFSTEP]
induction' l with head tail ih
[GOAL]
case a.nil
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q []
[PROOFSTEP]
apply pq
[GOAL]
case a.nil.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p (reverse [])
[PROOFSTEP]
simp only [reverse_nil, base]
[GOAL]
case a.cons
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (head :: tail)
[PROOFSTEP]
apply pq
[GOAL]
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse (head :: tail))
[PROOFSTEP]
simp only [reverse_cons]
[GOAL]
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail ++ [head])
[PROOFSTEP]
apply ind
[GOAL]
case a.cons.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail)
[PROOFSTEP]
apply qp
[GOAL]
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (reverse (reverse tail))
[PROOFSTEP]
rw [reverse_reverse]
[GOAL]
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q tail
[PROOFSTEP]
exact ih
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
    List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros f n l₁ l₂
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
generalize e : (l₁ ++ l₂).length = len
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
revert n l₁ l₂
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = Nat.zero →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros n l₁ l₂ h
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = Nat.succ len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros n l₁ l₂ h
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
[PROOFSTEP]
cases l₁
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h ; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
[PROOFSTEP]
cases l₂
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rw [List.length_append] at h
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
simp only [l₁_nil, l₂_nil]
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
cases' l₁ with head tail
[GOAL]
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n ([] ++ l₂) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) l₂
[PROOFSTEP]
rfl
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (head :: tail ++ l₂) =
    List.oldMapIdxCore f n (head :: tail) ++ List.oldMapIdxCore f (n + length (head :: tail)) l₂
[PROOFSTEP]
simp only [List.oldMapIdxCore, List.append_eq, length_cons, cons_append, cons.injEq, true_and]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
[PROOFSTEP]
suffices : n + Nat.succ (length tail) = n + 1 + tail.length
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
{ rw [this]
  apply ih (n + 1) _ _ _
  simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
  simp only [length_append, h]
}
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
[PROOFSTEP]
rw [this]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + 1 + length tail) l₂
[PROOFSTEP]
apply ih (n + 1) _ _ _
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
this : n + Nat.succ (length tail) = n + 1 + length tail
h : length tail + length l₂ = len
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [length_append, h]
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
{rw [Nat.add_assoc]; simp only [Nat.add_comm]
}
-- Porting note: new theorem.
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
rw [Nat.add_assoc]
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + (1 + length tail)
[PROOFSTEP]
simp only [Nat.add_comm]
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
[PROOFSTEP]
intros f l e
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
[PROOFSTEP]
unfold List.oldMapIdx
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f (length l) e]
[PROOFSTEP]
rw [List.oldMapIdxCore_append f 0 l [e]]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + length l) [e] = List.oldMapIdxCore f 0 l ++ [f (length l) e]
[PROOFSTEP]
simp only [zero_add, append_cancel_left_eq]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f (length l) [e] = [f (length l) e]
[PROOFSTEP]
rfl
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l₁ l₂ : List α) (arr : Array β),
    mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
intros f l₁ l₂ arr
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
generalize e : (l₁ ++ l₂).length = len
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
revert l₁ l₂ arr
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = Nat.zero → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
intros l₁ l₂ arr h
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = Nat.succ len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
intros l₁ l₂ arr h
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
[PROOFSTEP]
cases l₁
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h ; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
[PROOFSTEP]
cases l₂
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rw [List.length_append] at h
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
rw [l₁_nil, l₂_nil]
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f ([] ++ []) arr = mapIdx.go f [] (toArray (mapIdx.go f [] arr))
[PROOFSTEP]
simp only [mapIdx.go, Array.toList_eq, Array.toArray_data]
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.succ len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
cases' l₁ with head tail
[GOAL]
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.succ len
⊢ mapIdx.go f ([] ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f [] arr))
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (head :: tail ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f (head :: tail) arr))
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.succ len
⊢ mapIdx.go f ([] ++ l₂) arr = mapIdx.go f l₂ (toArray (Array.toList arr))
[PROOFSTEP]
simp only [nil_append, Array.toList_eq, Array.toArray_data]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (List.append tail l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
[PROOFSTEP]
simp only [List.append_eq]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (tail ++ l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
[PROOFSTEP]
rw [ih]
[GOAL]
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
[GOAL]
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length tail + length l₂ = len
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [length_append, h]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
[PROOFSTEP]
intro f l
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
⊢ ∀ (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
[PROOFSTEP]
induction' l with head tail ih
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (arr : Array β), length (mapIdx.go f [] arr) = length [] + Array.size arr
[PROOFSTEP]
intro
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
arr✝ : Array β
⊢ length (mapIdx.go f [] arr✝) = length [] + Array.size arr✝
[PROOFSTEP]
simp only [mapIdx.go, Array.toList_eq, length_nil, zero_add]
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
⊢ ∀ (arr : Array β), length (mapIdx.go f (head :: tail) arr) = length (head :: tail) + Array.size arr
[PROOFSTEP]
intro
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f (head :: tail) arr✝) = length (head :: tail) + Array.size arr✝
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f tail (Array.push arr✝ (f (Array.size arr✝) head))) = length (head :: tail) + Array.size arr✝
[PROOFSTEP]
rw [ih]
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + Array.size (Array.push arr✝ (f (Array.size arr✝) head)) = length (head :: tail) + Array.size arr✝
[PROOFSTEP]
simp only [Array.size_push, length_cons]
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + (Array.size arr✝ + 1) = Nat.succ (length tail) + Array.size arr✝
[PROOFSTEP]
simp only [Nat.add_succ, add_zero, Nat.add_comm]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), mapIdx f (l ++ [e]) = mapIdx f l ++ [f (length l) e]
[PROOFSTEP]
intros f l e
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx f (l ++ [e]) = mapIdx f l ++ [f (length l) e]
[PROOFSTEP]
unfold mapIdx
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx.go f (l ++ [e]) #[] = mapIdx.go f l #[] ++ [f (length l) e]
[PROOFSTEP]
rw [mapIdxGo_append f l [e]]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx.go f [e] (toArray (mapIdx.go f l #[])) = mapIdx.go f l #[] ++ [f (length l) e]
[PROOFSTEP]
simp only [mapIdx.go, Array.size_toArray, mapIdxGo_length, length_nil, add_zero, Array.toList_eq, Array.push_data,
  Array.data_toArray]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α), mapIdx f l = List.oldMapIdx f l
[PROOFSTEP]
intro f
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l
[PROOFSTEP]
apply list_reverse_induction
[GOAL]
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []
[PROOFSTEP]
rfl
[GOAL]
case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
[PROOFSTEP]
intro l e h
[GOAL]
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
[PROOFSTEP]
rw [List.oldMapIdx_append, mapIdx_append_one, h]
[GOAL]
α : Type u
β : Type v
⊢ ∀ (l : List α) (n : ℕ) (f : ℕ → α → β),
    map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
[PROOFSTEP]
intro l
[GOAL]
α : Type u
β : Type v
l : List α
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
[PROOFSTEP]
generalize e : l.length = len
[GOAL]
α : Type u
β : Type v
l : List α
len : ℕ
e : length l = len
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
[PROOFSTEP]
revert l
[GOAL]
α : Type u
β : Type v
len : ℕ
⊢ ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
⊢ ∀ (l : List α),
    length l = Nat.zero →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
intros l e n f
[GOAL]
case succ
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
⊢ ∀ (l : List α),
    length l = Nat.succ len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) l
[PROOFSTEP]
intros l e n f
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
have : l = [] := by cases l; rfl; contradiction
[GOAL]
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
⊢ l = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
e : length [] = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
this : l = []
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
rw [this]
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
this : l = []
⊢ map (uncurry f) (enumFrom n []) = zipWith (fun i => f (i + n)) (range Nat.zero) []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
l : List α
e : length l = Nat.succ len
n : ℕ
f : ℕ → α → β
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) l
[PROOFSTEP]
cases' l with head tail
[GOAL]
case succ.nil
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
e : length [] = Nat.succ len
⊢ map (uncurry f) (enumFrom n []) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) []
[PROOFSTEP]
contradiction
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ map (uncurry f) (enumFrom n (head :: tail)) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) (head :: tail)
[PROOFSTEP]
simp only [map, uncurry_apply_pair, range_succ_eq_map, zipWith, zero_add, zipWith_map_left]
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ f n head :: map (uncurry f) (enumFrom (n + 1) tail) =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
[PROOFSTEP]
rw [ih]
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ f n head :: zipWith (fun i => f (i + (n + 1))) (range len) tail =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
suffices : (fun i ↦ f (i + (n + 1))) = ((fun i ↦ f (i + n)) ∘ Nat.succ)
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
this : (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
⊢ f n head :: zipWith (fun i => f (i + (n + 1))) (range len) tail =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
case this
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
rw [this]
[GOAL]
case this
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
funext n' a
[GOAL]
case this.h.h
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
n' : ℕ
a : α
⊢ f (n' + (n + 1)) a = ((fun i => f (i + n)) ∘ Nat.succ) n' a
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
simp only [comp, Nat.add_assoc, Nat.add_comm, Nat.add_succ]
[GOAL]
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
simp only [length_cons, Nat.succ.injEq] at e
[GOAL]
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length tail = len
⊢ length tail = len
[PROOFSTEP]
exact e
[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = map (uncurry f) (enum l)
[PROOFSTEP]
rw [List.new_def_eq_old_def]
[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ List.oldMapIdx f l = map (uncurry f) (enum l)
[PROOFSTEP]
induction' l with hd tl hl generalizing f
[GOAL]
case nil
α : Type u
β : Type v
f✝ f : ℕ → α → β
⊢ List.oldMapIdx f [] = map (uncurry f) (enum [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β), List.oldMapIdx f tl = map (uncurry f) (enum tl)
f : ℕ → α → β
⊢ List.oldMapIdx f (hd :: tl) = map (uncurry f) (enum (hd :: tl))
[PROOFSTEP]
rw [List.oldMapIdx, List.oldMapIdxCore, List.oldMapIdxCore_eq, hl]
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β), List.oldMapIdx f tl = map (uncurry f) (enum tl)
f : ℕ → α → β
⊢ f 0 hd :: map (uncurry fun i a => f (i + (0 + 1)) a) (enum tl) = map (uncurry f) (enum (hd :: tl))
[PROOFSTEP]
simp [enum_eq_zip_range, map_uncurry_zip_eq_zipWith]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
a : α
⊢ mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l
[PROOFSTEP]
simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith, range_succ_eq_map, zipWith_map_left]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
K L : List α
f : ℕ → α → β
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i a => f (i + length K) a) L
[PROOFSTEP]
induction' K with a J IH generalizing f
[GOAL]
case nil
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ f : ℕ → α → β
⊢ mapIdx f ([] ++ L) = mapIdx f [] ++ mapIdx (fun i a => f (i + length []) a) L
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ : ℕ → α → β
a : α
J : List α
IH : ∀ (f : ℕ → α → β), mapIdx f (J ++ L) = mapIdx f J ++ mapIdx (fun i a => f (i + length J) a) L
f : ℕ → α → β
⊢ mapIdx f (a :: J ++ L) = mapIdx f (a :: J) ++ mapIdx (fun i a_1 => f (i + length (a :: J)) a_1) L
[PROOFSTEP]
simp [IH fun i ↦ f (i + 1), add_assoc]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ length (mapIdx f l) = length l
[PROOFSTEP]
induction' l with hd tl IH generalizing f
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ length (mapIdx f []) = length []
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), length (mapIdx f tl) = length tl
f : ℕ → α → β
⊢ length (mapIdx f (hd :: tl)) = length (hd :: tl)
[PROOFSTEP]
simp [IH]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
i : ℕ
h : i < length l
h' : optParam (i < length (mapIdx f l)) (_ : i < length (mapIdx f l))
⊢ nthLe (mapIdx f l) i h' = f i (nthLe l i h)
[PROOFSTEP]
simp [mapIdx_eq_enum_map, enum_eq_zip_range]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i => f (↑i) (get l i)
[PROOFSTEP]
induction' l with hd tl IH generalizing f
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i => f (↑i) (get [] i)
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tl = ofFn fun i => f (↑i) (get tl i)
f : ℕ → α → β
⊢ mapIdx f (hd :: tl) = ofFn fun i => f (↑i) (get (hd :: tl) i)
[PROOFSTEP]
simp [IH]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
start : ℕ
⊢ foldrIdx f b as start = foldrIdxSpec f b as start
[PROOFSTEP]
induction as generalizing start
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start
[PROOFSTEP]
simp only [foldrIdx, foldrIdxSpec_cons, *]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
⊢ foldrIdx f b as = foldr (uncurry f) b (enum as)
[PROOFSTEP]
simp only [foldrIdx, foldrIdxSpec, foldrIdx_eq_foldrIdxSpec, enum]
[GOAL]
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ indexesValues (fun b => decide (p b)) as = filter ((fun b => decide (p b)) ∘ Prod.snd) (enum as)
[PROOFSTEP]
simp [indexesValues, foldrIdx_eq_foldr_enum, uncurry, filter_eq_foldr]
[GOAL]
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ findIdxs (fun b => decide (p b)) as = map Prod.fst (indexesValues (fun b => decide (p b)) as)
[PROOFSTEP]
simp only [indexesValues_eq_filter_enum, map_filter_eq_foldr, findIdxs, uncurry, foldrIdx_eq_foldr_enum,
  decide_eq_true_eq, comp_apply, Bool.cond_decide]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
start : ℕ
⊢ foldlIdx f a bs start = foldlIdxSpec f a bs start
[PROOFSTEP]
induction bs generalizing start a
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start
[PROOFSTEP]
simp [foldlIdxSpec, *]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
⊢ foldlIdx f a bs = foldl (fun a p => f p.fst a p.snd) a (enum bs)
[PROOFSTEP]
simp only [foldlIdx, foldlIdxSpec, foldlIdx_eq_foldlIdxSpec, enum]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type u
f : ℕ → α → β → m β
b : β
as : List α
inst✝ : LawfulMonad m
⊢ foldrIdxM f b as = foldrM (uncurry f) b (enum as)
[PROOFSTEP]
simp only [foldrIdxM, foldrM_eq_foldr, foldrIdx_eq_foldr_enum, uncurry]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → β → α → m β
b : β
as : List α
⊢ foldlIdxM f b as = List.foldlM (fun b p => f p.fst b p.snd) b (enum as)
[PROOFSTEP]
rw [foldlIdxM, foldlM_eq_foldl, foldlIdx_eq_foldl_enum]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
generalize e : as.length = len
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : length as = len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
revert as arr
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
⊢ ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
⊢ ∀ (arr : Array β) (as : List α),
    length as = Nat.zero →
      mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
intro arr as h
[GOAL]
case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
⊢ ∀ (arr : Array β) (as : List α),
    length as = Nat.succ len →
      mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
intro arr as h
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
have : as = [] := by cases as; rfl; contradiction
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ as = []
[PROOFSTEP]
cases as
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
h : length [] = Nat.zero
⊢ [] = []
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
this : as = []
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
simp only [this, mapIdxM.go, mapIdxMAuxSpec, List.traverse, map_pure, append_nil]
[GOAL]
case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length as = Nat.succ len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
match as with
| nil => contradiction
| cons head tail =>
  simp only [length_cons, Nat.succ.injEq] at h
  simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map, LawfulMonad.bind_assoc, pure_bind]
  congr
  conv => {lhs; intro x; rw [ih _ _ h]; }
  funext x
  simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push, map_eq_pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length [] = Nat.succ len
⊢ mapIdxM.go f [] arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) []
[PROOFSTEP]
contradiction
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length (head :: tail) = Nat.succ len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
[PROOFSTEP]
simp only [length_cons, Nat.succ.injEq] at h
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
[PROOFSTEP]
simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map, LawfulMonad.bind_assoc, pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (do
      let __do_lift ← f (Array.size arr) head
      mapIdxM.go f tail (Array.push arr __do_lift)) =
    do
    let x ← f (Array.size arr) head
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
congr
[GOAL]
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
conv => {lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
{lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
{lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
lhs
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)
[PROOFSTEP]
intro x
[GOAL]
case h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
| mapIdxM.go f tail (Array.push arr x)
[PROOFSTEP]
rw [ih _ _ h]
[GOAL]
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun x =>
      (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail) =
    fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
funext x
[GOAL]
case e_a.h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
⊢ (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail = do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push, map_eq_pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
as : List α
⊢ mapIdxM as f = List.traverse (uncurry f) (enum as)
[PROOFSTEP]
simp only [mapIdxM, mapIdxMGo_eq_mapIdxMAuxSpec, Array.toList_eq, Array.data_toArray, nil_append, mapIdxMAuxSpec,
  Array.size_toArray, length_nil, id_map', enum]
[GOAL]
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
[PROOFSTEP]
revert arr
[GOAL]
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
[PROOFSTEP]
induction' as with head tail ih
[GOAL]
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit
[PROOFSTEP]
intro arr
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) (head :: tail) =
      SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
[PROOFSTEP]
intro arr
[GOAL]
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit
[PROOFSTEP]
simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) (head :: tail) =
    SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
[PROOFSTEP]
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind, bind_pure_unit, LawfulMonad.bind_assoc, pure_bind,
  mapIdxM.go, seq_pure]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ (do
      f (Array.size arr) head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← f (Array.size arr) head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
generalize (f (Array.size arr) head) = head
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
let arr_1 := arr.push ⟨⟩
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
have : arr_1.size = arr.size + 1 := Array.size_push arr ⟨⟩
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
rw [← this, ih arr_1]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      SeqRight.seqRight (mapIdxM.go f tail arr_1) fun x => pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]