[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k => insertNth k x l) {n | n ≤ length l}
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
⊢ Set.InjOn (fun k => insertNth k x []) {n | n ≤ length []}
[PROOFSTEP]
intro n hn m hm _
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
n : ℕ
hn : n ∈ {n | n ≤ length []}
m : ℕ
hm : m ∈ {n | n ≤ length []}
a✝ : (fun k => insertNth k x []) n = (fun k => insertNth k x []) m
⊢ n = m
[PROOFSTEP]
simp only [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length, nonpos_iff_eq_zero] at hn hm 
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
n m : ℕ
a✝ : (fun k => insertNth k x []) n = (fun k => insertNth k x []) m
hn : n = 0
hm : m = 0
⊢ n = m
[PROOFSTEP]
simp [hn, hm]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
⊢ Set.InjOn (fun k => insertNth k x (hd :: tl)) {n | n ≤ length (hd :: tl)}
[PROOFSTEP]
intro n hn m hm h
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ length (hd :: tl)}
m : ℕ
hm : m ∈ {n | n ≤ length (hd :: tl)}
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
⊢ n = m
[PROOFSTEP]
simp only [length, Set.mem_setOf_eq] at hn hm 
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ≤ length tl + 1
m : ℕ
hm : m ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
⊢ n = m
[PROOFSTEP]
simp only [mem_cons, not_or] at hx 
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
n : ℕ
hn : n ≤ length tl + 1
m : ℕ
hm : m ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
hx : ¬x = hd ∧ ¬x ∈ tl
⊢ n = m
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
m : ℕ
hm : m ≤ length tl + 1
hx : ¬x = hd ∧ ¬x ∈ tl
hn : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) m
⊢ Nat.zero = m
[PROOFSTEP]
cases m
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
m : ℕ
hm : m ≤ length tl + 1
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝) = (fun k => insertNth k x (hd :: tl)) m
⊢ Nat.succ n✝ = m
[PROOFSTEP]
cases m
[GOAL]
case cons.zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
hn hm : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) Nat.zero
⊢ Nat.zero = Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case cons.zero.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
hn : Nat.zero ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
⊢ Nat.zero = Nat.succ n✝
[PROOFSTEP]
simp [hx.left] at h 
[GOAL]
case cons.succ.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : Nat.succ n✝ ≤ length tl + 1
hm : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝) = (fun k => insertNth k x (hd :: tl)) Nat.zero
⊢ Nat.succ n✝ = Nat.zero
[PROOFSTEP]
simp [Ne.symm hx.left] at h 
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝¹) = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
⊢ Nat.succ n✝¹ = Nat.succ n✝
[PROOFSTEP]
simp only [true_and_iff, eq_self_iff_true, insertNth_succ_cons] at h 
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ Nat.succ n✝¹ = Nat.succ n✝
[PROOFSTEP]
rw [Nat.succ_inj']
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝¹ = n✝
[PROOFSTEP]
refine' IH hx.right _ _ (by injection h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ (fun k => insertNth k x tl) n✝¹ = (fun k => insertNth k x tl) n✝
[PROOFSTEP]
injection h
[GOAL]
case cons.succ.succ.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝¹ ∈ {n | n ≤ length tl}
[PROOFSTEP]
simpa [Nat.succ_le_succ_iff] using hn
[GOAL]
case cons.succ.succ.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝ ∈ {n | n ≤ length tl}
[PROOFSTEP]
simpa [Nat.succ_le_succ_iff] using hm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ Set.range (foldr f a) ⊆ Set.range (foldr g a)
[PROOFSTEP]
rintro _ ⟨l, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
[PROOFSTEP]
induction' l with b l H
[GOAL]
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)
[PROOFSTEP]
exact ⟨[], rfl⟩
[GOAL]
case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
cases' hfg (Set.mem_range_self b) with c hgf
[GOAL]
case intro.cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
cases' H with m hgf'
[GOAL]
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
rw [foldr_cons, ← hgf, ← hgf']
[GOAL]
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
[PROOFSTEP]
exact ⟨c :: m, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)
[PROOFSTEP]
change
  (Set.range fun l => _) ⊆
    Set.range fun l =>
      _
        -- Porting note: This was simply `simp_rw [← foldr_reverse]`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l
[PROOFSTEP]
simp_rw [← foldr_reverse _ (fun z w => g w z), ← foldr_reverse _ (fun z w => f w z)]
  -- Porting note: This `change` was not necessary in mathlib3
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a (reverse l)) ⊆
    Set.range fun l => foldr (fun z w => g w z) a (reverse l)
[PROOFSTEP]
change (Set.range (foldr (fun z w => f w z) a ∘ reverse)) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
[PROOFSTEP]
simp_rw [Set.range_comp _ reverse, reverse_involutive.bijective.surjective.range_eq, Set.image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)
[PROOFSTEP]
exact foldr_range_subset_of_range_subset hfg a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun a s =>
        let r := f a s.fst;
        (r.fst, r.snd :: s.snd))
      (s, []) (a :: as)
[PROOFSTEP]
simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun ab s =>
        let r := f ab.fst ab.snd s.fst;
        (r.fst, r.snd :: s.snd))
      (s, []) (zip (a :: as) (b :: bs))
[PROOFSTEP]
simp only [mapAccumr₂, foldr, mapAccumr₂_eq_foldr f as]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b
          (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
              (zip as bs)).fst).fst,
      (f a b
            (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
                (zip as bs)).fst).snd ::
        (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
            (zip as bs)).snd) =
    ((f a b
          (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
              (zipWith Prod.mk as bs)).fst).fst,
      (f a b
            (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
                (zipWith Prod.mk as bs)).fst).snd ::
        (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
            (zipWith Prod.mk as bs)).snd)
[PROOFSTEP]
rfl
