/-
Copyright (c) 2021 Yakov Pechersky. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yakov Pechersky, Yury Kudryashov

! This file was ported from Lean 3 source module data.list.lemmas
! leanprover-community/mathlib commit 2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Function
import Mathlib.Data.List.Basic

/-! # Some lemmas about lists involving sets

Split out from `Data.List.Basic` to reduce its dependencies.
-/


open List

variable {
α: Type ?u.2
α 
β: Type ?u.3433
β 
γ: Type ?u.8
γ : 
Type _: Type (?u.4846+1)
Type _}

namespace List

theorem 
injOn_insertNth_index_of_not_mem: ∀ {α : Type u_1} (l : List α) (x : α), ¬x ∈ l → Set.InjOn (fun k => insertNth k x l) { n | n ≤ length l }
injOn_insertNth_index_of_not_mem (
l: List α
l : 
List: Type ?u.20 → Type ?u.20
List 
α: Type ?u.11
α) (
x: α
x : 
α: Type ?u.11
α) (
hx: ¬x ∈ l
hx : 
x: α
x ∉ 
l: List α
l) :
    
Set.InjOn: {α : Type ?u.43} → {β : Type ?u.42} → (α → β) → Set α → Prop
Set.InjOn (fun 
k: ?m.47
k => 
insertNth: {α : Type ?u.49} → ℕ → α → List α → List α
insertNth 
k: ?m.47
k 
x: α
x 
l: List α
l) { 
n: ?m.59
n | 
n: ?m.59
n ≤ 
l: List α
l.
length: {α : Type ?u.62} → List α → ℕ
length } := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx: ¬x ∈ l

Set.InjOn (fun k => insertNth k x l) { n | n ≤ length l }induction' 
l: List α
l with 
hd: ?m.102
hd 
tl: List ?m.102
tl 
IH: ?m.103 tl
IH
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx✝: ¬x ∈ l

hx: ¬x ∈ []

nil
Set.InjOn (fun k => insertNth k x []) { n | n ≤ length [] }
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }
  
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx: ¬x ∈ l

Set.InjOn (fun k => insertNth k x l) { n | n ≤ length l }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx✝: ¬x ∈ l

hx: ¬x ∈ []

nil
Set.InjOn (fun k => insertNth k x []) { n | n ≤ length [] } 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx✝: ¬x ∈ l

hx: ¬x ∈ []

nil
Set.InjOn (fun k => insertNth k x []) { n | n ≤ length [] }
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }intro 
n: ℕ
n 
hn: n ∈ { n | n ≤ length [] }
hn 
m: ℕ
m 
hm: m ∈ { n | n ≤ length [] }
hm 
_: (fun k => insertNth k x []) n = (fun k => insertNth k x []) m
_
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

nil
n = m
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx✝: ¬x ∈ l

hx: ¬x ∈ []

nil
Set.InjOn (fun k => insertNth k x []) { n | n ≤ length [] }simp only [
Set.mem_singleton_iff: ∀ {α : Type ?u.147} {a b : α}, a ∈ {b} ↔ a = b
Set.mem_singleton_iff, 
Set.setOf_eq_eq_singleton: ∀ {α : Type ?u.170} {a : α}, { n | n = a } = {a}
Set.setOf_eq_eq_singleton,
      
length: {α : Type ?u.179} → List α → ℕ
length, 
nonpos_iff_eq_zero: ∀ {α : Type ?u.444} [inst : CanonicallyOrderedAddMonoid α] {a : α}, a ≤ 0 ↔ a = 0
nonpos_iff_eq_zero] at 
hn: n ∈ { n | n ≤ length [] }
hn 
hm: m ∈ { n | n ≤ length [] }
hm
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

nil
n = m
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx✝: ¬x ∈ l

hx: ¬x ∈ []

nil
Set.InjOn (fun k => insertNth k x []) { n | n ≤ length [] }simp [
hn: n = 0
hn, 
hm: m = 0
hm]
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

l: List α

x: α

hx: ¬x ∈ l

Set.InjOn (fun k => insertNth k x l) { n | n ≤ length l }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) } 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }intro 
n: ℕ
n 
hn: n ∈ { n | n ≤ length (hd :: tl) }
hn 
m: ℕ
m 
hm: m ∈ { n | n ≤ length (hd :: tl) }
hm 
h: (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
h
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
n = m
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }simp only [
length: {α : Type ?u.765} → List α → ℕ
length, 
Set.mem_setOf_eq: ∀ {α : Type ?u.781} {x : α} {p : α → Prop}, (x ∈ { y | p y }) = p x
Set.mem_setOf_eq] at 
hn: n ∈ { n | n ≤ length (hd :: tl) }
hn 
hm: m ∈ { n | n ≤ length (hd :: tl) }
hm
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
n = m
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }simp only [
mem_cons: ∀ {α : Type ?u.871} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
mem_cons, 
not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬q
not_or] at 
hx: ¬x ∈ hd :: tl
hx
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
n = m
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }cases 
n: ℕ
n
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero
Nat.zero = m
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ
Nat.succ n✝ = m 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
n = m<;>
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero
Nat.zero = m
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ
Nat.succ n✝ = m 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
n = mcases 
m: ℕ
m
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.zero
Nat.zero = Nat.zero
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.succ
Nat.zero = Nat.succ n✝
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.zero
Nat.zero = Nat.zero 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.zero
Nat.zero = Nat.zero
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.succ
Nat.zero = Nat.succ n✝
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.zero
Nat.succ n✝ = Nat.zero
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝rfl
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.succ
Nat.zero = Nat.succ n✝ 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.zero.succ
Nat.zero = Nat.succ n✝
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.zero
Nat.succ n✝ = Nat.zero
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝simp [
hx: ¬x = hd ∧ ¬x ∈ tl
hx.
left: ∀ {a b : Prop}, a ∧ b → a
left] at 
h: (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
h
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.zero
Nat.succ n✝ = Nat.zero 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.zero
Nat.succ n✝ = Nat.zero
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝simp [
Ne.symm: ∀ {α : Sort ?u.1328} {a b : α}, a ≠ b → b ≠ a
Ne.symm 
hx: ¬x = hd ∧ ¬x ∈ tl
hx.
left: ∀ {a b : Prop}, a ∧ b → a
left] at 
h: (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝) = (fun k => insertNth k x (hd :: tl)) Nat.zero
h
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons
Set.InjOn (fun k => insertNth k x (hd :: tl)) { n | n ≤ length (hd :: tl) }·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝ 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝simp only [
true_and_iff: ∀ (p : Prop), True ∧ p ↔ p
true_and_iff, 
eq_self_iff_true: ∀ {α : Sort ?u.1461} (a : α), a = a ↔ True
eq_self_iff_true, 
insertNth_succ_cons: ∀ {α : Type ?u.1476} (s : List α) (hd x : α) (n : ℕ), insertNth (n + 1) x (hd :: s) = hd :: insertNth n x s
insertNth_succ_cons] at 
h: (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝¹) = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
h
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝
      
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝rw [
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝
Nat.succ_inj': ∀ {n m : ℕ}, Nat.succ n = Nat.succ m ↔ n = m
Nat.succ_inj'
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
n✝¹ = n✝]
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
n✝¹ = n✝
      
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝refine' 
IH: ?m.103 tl
IH 
hx: ¬x = hd ∧ ¬x ∈ tl
hx.
right: ∀ {a b : Prop}, a ∧ b → b
right 
_: ?m.1601 ∈ { n | n ≤ length tl }
_ 
_: ?m.1603 ∈ { n | n ≤ length tl }
_ (
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
n✝¹ = n✝by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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✝injection 
h: hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
h
Goals accomplished! 🐙)
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_1
n✝¹ ∈ { n | n ≤ length tl }
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_2
n✝ ∈ { n | n ≤ length tl }
      
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_1
n✝¹ ∈ { n | n ≤ length tl } 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_1
n✝¹ ∈ { n | n ≤ length tl }
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_2
n✝ ∈ { n | n ≤ length tl }simpa [
Nat.succ_le_succ_iff: ∀ {a b : ℕ}, Nat.succ a ≤ Nat.succ b ↔ a ≤ b
Nat.succ_le_succ_iff] using 
hn: Nat.succ n✝¹ ≤ length tl + 1
hn
Goals accomplished! 🐙
      
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ
Nat.succ n✝¹ = Nat.succ n✝·
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_2
n✝ ∈ { n | n ≤ length tl } 
α: Type u_1

β: Type ?u.14

γ: Type ?u.17

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

cons.succ.succ.refine'_2
n✝ ∈ { n | n ≤ length tl }simpa [
Nat.succ_le_succ_iff: ∀ {a b : ℕ}, Nat.succ a ≤ Nat.succ b ↔ a ≤ b
Nat.succ_le_succ_iff] using 
hm: Nat.succ n✝ ≤ length tl + 1
hm
Goals accomplished! 🐙
#align list.inj_on_insert_nth_index_of_not_mem 
List.injOn_insertNth_index_of_not_mem: ∀ {α : Type u_1} (l : List α) (x : α), ¬x ∈ l → Set.InjOn (fun k => insertNth k x l) { n | n ≤ length l }
List.injOn_insertNth_index_of_not_mem

theorem 
foldr_range_subset_of_range_subset: ∀ {f : β → α → α} {g : γ → α → α}, Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (foldr f a) ⊆ Set.range (foldr g a)
foldr_range_subset_of_range_subset {
f: β → α → α
f : 
β: Type ?u.2956
β → 
α: Type ?u.2953
α → 
α: Type ?u.2953
α} {
g: γ → α → α
g : 
γ: Type ?u.2959
γ → 
α: Type ?u.2953
α → 
α: Type ?u.2953
α}
    (
hfg: Set.range f ⊆ Set.range g
hfg : 
Set.range: {α : Type ?u.2983} → {ι : Sort ?u.2982} → (ι → α) → Set α
Set.range 
f: β → α → α
f ⊆ 
Set.range: {α : Type ?u.2995} → {ι : Sort ?u.2994} → (ι → α) → Set α
Set.range 
g: γ → α → α
g) (
a: α
a : 
α: Type ?u.2953
α) : 
Set.range: {α : Type ?u.3027} → {ι : Sort ?u.3026} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.3032} → {β : Type ?u.3031} → (α → β → β) → β → List α → β
foldr 
f: β → α → α
f 
a: α
a) ⊆ 
Set.range: {α : Type ?u.3049} → {ι : Sort ?u.3048} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.3054} → {β : Type ?u.3053} → (α → β → β) → β → List α → β
foldr 
g: γ → α → α
g 
a: α
a) := by
Goals accomplished! 🐙
  
α: 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)rintro 
_: α
_ 
⟨l, rfl⟩: a✝¹ ∈ Set.range (foldr f a)
⟨
l: List β
l
⟨l, rfl⟩: a✝¹ ∈ Set.range (foldr f a)
, 
rfl: foldr f a l = a✝
rfl
⟨l, rfl⟩: a✝¹ ∈ Set.range (foldr f a)
⟩
α: Type u_1

β: Type u_2

γ: Type u_3

f: β → α → α

g: γ → α → α

hfg: Set.range f ⊆ Set.range g

a: α

l: List β

intro
foldr f a l ∈ Set.range (foldr g a)
  
α: 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)induction' 
l: List β
l with 
b: ?m.3140
b 
l: List ?m.3140
l 
H: ?m.3141 l
H
α: Type u_1

β: Type u_2

γ: Type u_3

f: β → α → α

g: γ → α → α

hfg: Set.range f ⊆ Set.range g

a: α

intro.nil
foldr f a [] ∈ Set.range (foldr g a)
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)
  
α: 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)·
α: Type u_1

β: Type u_2

γ: Type u_3

f: β → α → α

g: γ → α → α

hfg: Set.range f ⊆ Set.range g

a: α

intro.nil
foldr f a [] ∈ Set.range (foldr g a) 
α: Type u_1

β: Type u_2

γ: Type u_3

f: β → α → α

g: γ → α → α

hfg: Set.range f ⊆ Set.range g

a: α

intro.nil
foldr f a [] ∈ Set.range (foldr g a)
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)exact ⟨
[]: List ?m.3167
[], 
rfl: ∀ {α : Sort ?u.3169} {a : α}, a = a
rfl⟩
Goals accomplished! 🐙
  
α: 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)·
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a) 
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)cases' 
hfg: Set.range f ⊆ Set.range g
hfg (
Set.mem_range_self: ∀ {α : Type ?u.3208} {ι : Sort ?u.3209} {f : ι → α} (i : ι), f i ∈ Set.range f
Set.mem_range_self 
b: ?m.3140
b) with 
c: ?m.3252
c 
hgf: ?m.3253 c
hgf
α: 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

intro.cons.intro
foldr f a (b :: l) ∈ Set.range (foldr g a)
    
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)cases' 
H: ?m.3141 l
H with 
m: ?m.3301
m 
hgf': ?m.3302 m
hgf'
α: 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

intro.cons.intro.intro
foldr f a (b :: l) ∈ Set.range (foldr g a)
    
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)rw [
α: 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

intro.cons.intro.intro
foldr f a (b :: l) ∈ Set.range (foldr g a)
foldr_cons: ∀ {α : Type ?u.3332} {β : Type ?u.3331} (f : α → β → β) (b : β) (a : α) (l : List α),
  foldr f b (a :: l) = f a (foldr f b l)
foldr_cons,
α: 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

intro.cons.intro.intro
f b (foldr f a l) ∈ Set.range (foldr g a) 
α: 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

intro.cons.intro.intro
foldr f a (b :: l) ∈ Set.range (foldr g a)← 
hgf: ?m.3253 c
hgf,
α: 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

intro.cons.intro.intro
g c (foldr f a l) ∈ Set.range (foldr g a) 
α: 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

intro.cons.intro.intro
foldr f a (b :: l) ∈ Set.range (foldr g a)← 
hgf': ?m.3302 m
hgf'
α: 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

intro.cons.intro.intro
g c (foldr g a m) ∈ Set.range (foldr g a)]
α: 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

intro.cons.intro.intro
g c (foldr g a m) ∈ Set.range (foldr g a)
    
α: 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)

intro.cons
foldr f a (b :: l) ∈ Set.range (foldr g a)exact ⟨
c: ?m.3252
c :: 
m: ?m.3301
m, 
rfl: ∀ {α : Sort ?u.3380} {a : α}, a = a
rfl⟩
Goals accomplished! 🐙
#align list.foldr_range_subset_of_range_subset 
List.foldr_range_subset_of_range_subset: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α → α} {g : γ → α → α},
  Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (foldr f a) ⊆ Set.range (foldr g a)
List.foldr_range_subset_of_range_subset

theorem 
foldl_range_subset_of_range_subset: ∀ {f : α → β → α} {g : α → γ → α},
  ((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)
foldl_range_subset_of_range_subset {
f: α → β → α
f : 
α: Type ?u.3430
α → 
β: Type ?u.3433
β → 
α: Type ?u.3430
α} {
g: α → γ → α
g : 
α: Type ?u.3430
α → 
γ: Type ?u.3436
γ → 
α: Type ?u.3430
α}
    (
hfg: (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
hfg : (
Set.range: {α : Type ?u.3460} → {ι : Sort ?u.3459} → (ι → α) → Set α
Set.range fun 
a: ?m.3465
a 
c: ?m.3468
c => 
f: α → β → α
f 
c: ?m.3468
c 
a: ?m.3465
a) ⊆ 
Set.range: {α : Type ?u.3477} → {ι : Sort ?u.3476} → (ι → α) → Set α
Set.range fun 
b: ?m.3483
b 
c: ?m.3486
c => 
g: α → γ → α
g 
c: ?m.3486
c 
b: ?m.3483
b) (
a: α
a : 
α: Type ?u.3430
α) :
    
Set.range: {α : Type ?u.3514} → {ι : Sort ?u.3513} → (ι → α) → Set α
Set.range (
foldl: {α : Type ?u.3519} → {β : Type ?u.3518} → (α → β → α) → α → List β → α
foldl 
f: α → β → α
f 
a: α
a) ⊆ 
Set.range: {α : Type ?u.3536} → {ι : Sort ?u.3535} → (ι → α) → Set α
Set.range (
foldl: {α : Type ?u.3541} → {β : Type ?u.3540} → (α → β → α) → α → List β → α
foldl 
g: α → γ → α
g 
a: α
a) := by
Goals accomplished! 🐙
  
α: 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)change (
Set.range: {α : Type ?u.3581} → {ι : Sort ?u.3580} → (ι → α) → Set α
Set.range fun 
l: ?m.3586
l => 
_: ?m.3582
_) ⊆ 
Set.range: {α : Type ?u.3593} → {ι : Sort ?u.3592} → (ι → α) → Set α
Set.range fun 
l: ?m.3599
l => 
_: ?m.3594
_
α: 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
  -- Porting note: This was simply `simp_rw [← foldr_reverse]`
  
α: 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)simp_rw [
α: 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← 
foldr_reverse: ∀ {α : Type ?u.3744} {β : Type ?u.3745} (l : List α) (f : α → β → β) (b : β),
  foldr f b (reverse l) = foldl (fun x y => f y x) b l
foldr_reverse 
_: List ?m.3746
_ (fun 
z: ?m.3750
z 
w: ?m.3753
w => 
g: α → γ → α
g 
w: ?m.3753
w 
z: ?m.3750
z),
α: 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 => foldr (fun z w => g w z) a (reverse l) 
α: 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← 
foldr_reverse: ∀ {α : Type ?u.3840} {β : Type ?u.3841} (l : List α) (f : α → β → β) (b : β),
  foldr f b (reverse l) = foldl (fun x y => f y x) b l
foldr_reverse 
_: List ?m.3842
_ (fun 
z: ?m.3846
z 
w: ?m.3849
w => 
f: α → β → α
f 
w: ?m.3849
w 
z: ?m.3846
z)
α: 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)]
α: 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)
  -- Porting note: This `change` was not necessary in mathlib3
  
α: 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)change (
Set.range: {α : Type ?u.3943} → {ι : Sort ?u.3942} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.3956} → {β : Type ?u.3955} → (α → β → β) → β → List α → β
foldr (fun 
z: ?m.3962
z 
w: ?m.3965
w => 
f: α → β → α
f 
w: ?m.3965
w 
z: ?m.3962
z) 
a: α
a ∘ 
reverse: {α : Type ?u.3975} → List α → List α
reverse)) ⊆
    
Set.range: {α : Type ?u.3985} → {ι : Sort ?u.3984} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.3998} → {β : Type ?u.3997} → (α → β → β) → β → List α → β
foldr (fun 
z: ?m.4004
z 
w: ?m.4007
w => 
g: α → γ → α
g 
w: ?m.4007
w 
z: ?m.4004
z) 
a: α
a ∘ 
reverse: {α : Type ?u.4017} → List α → List α
reverse)
α: 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)
  
α: 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)simp_rw [
α: 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)
Set.range_comp: ∀ {α : Type ?u.4194} {β : Type ?u.4192} {ι : Sort ?u.4193} (g : α → β) (f : ι → α), Set.range (g ∘ f) = g '' Set.range f
Set.range_comp 
_: ?m.4195 → ?m.4196
_ 
reverse: {α : Type ?u.4199} → List α → List α
reverse,
α: 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: α

foldr (fun z w => f w z) a '' Set.range reverse ⊆ foldr (fun z w => g w z) a '' Set.range reverse 
α: 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)
reverse_involutive: ∀ {α : Type ?u.4458}, Function.Involutive reverse
reverse_involutive.
bijective: ∀ {α : Sort ?u.4460} {f : α → α}, Function.Involutive f → Function.Bijective f
bijective.
surjective: ∀ {α : Sort ?u.4467} {β : Sort ?u.4468} {f : α → β}, Function.Bijective f → Function.Surjective f
surjective.
range_eq: ∀ {α : Type ?u.4478} {ι : Sort ?u.4479} {f : ι → α}, Function.Surjective f → Set.range f = Set.univ
range_eq,
α: 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: α

foldr (fun z w => f w z) a '' Set.univ ⊆ foldr (fun z w => g w z) a '' Set.univ
    
α: 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)
Set.image_univ: ∀ {α : Type ?u.4668} {β : Type ?u.4667} {f : α → β}, f '' Set.univ = Set.range f
Set.image_univ
α: 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)]
α: 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)
  
α: 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)exact 
foldr_range_subset_of_range_subset: ∀ {α : Type ?u.4745} {β : Type ?u.4746} {γ : Type ?u.4747} {f : β → α → α} {g : γ → α → α},
  Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (foldr f a) ⊆ Set.range (foldr g a)
foldr_range_subset_of_range_subset 
hfg: (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
hfg 
a: α
a
Goals accomplished! 🐙
#align list.foldl_range_subset_of_range_subset 
List.foldl_range_subset_of_range_subset: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → α} {g : α → γ → α},
  ((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)
List.foldl_range_subset_of_range_subset

theorem 
foldr_range_eq_of_range_eq: ∀ {f : β → α → α} {g : γ → α → α}, Set.range f = Set.range g → ∀ (a : α), Set.range (foldr f a) = Set.range (foldr g a)
foldr_range_eq_of_range_eq {
f: β → α → α
f : 
β: Type ?u.4846
β → 
α: Type ?u.4843
α → 
α: Type ?u.4843
α} {
g: γ → α → α
g : 
γ: Type ?u.4849
γ → 
α: Type ?u.4843
α → 
α: Type ?u.4843
α} (
hfg: Set.range f = Set.range g
hfg : 
Set.range: {α : Type ?u.4866} → {ι : Sort ?u.4865} → (ι → α) → Set α
Set.range 
f: β → α → α
f = 
Set.range: {α : Type ?u.4876} → {ι : Sort ?u.4875} → (ι → α) → Set α
Set.range 
g: γ → α → α
g)
    (
a: α
a : 
α: Type ?u.4843
α) : 
Set.range: {α : Type ?u.4893} → {ι : Sort ?u.4892} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.4897} → {β : Type ?u.4896} → (α → β → β) → β → List α → β
foldr 
f: β → α → α
f 
a: α
a) = 
Set.range: {α : Type ?u.4914} → {ι : Sort ?u.4913} → (ι → α) → Set α
Set.range (
foldr: {α : Type ?u.4918} → {β : Type ?u.4917} → (α → β → β) → β → List α → β
foldr 
g: γ → α → α
g 
a: α
a) :=
  (
foldr_range_subset_of_range_subset: ∀ {α : Type ?u.4940} {β : Type ?u.4941} {γ : Type ?u.4942} {f : β → α → α} {g : γ → α → α},
  Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (foldr f a) ⊆ Set.range (foldr g a)
foldr_range_subset_of_range_subset 
hfg: Set.range f = Set.range g
hfg.
le: ∀ {α : Type ?u.4948} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le 
a: α
a).
antisymm: ∀ {α : Type ?u.5269} [inst : HasSubset α] {a b : α} [inst_1 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊆ a → a = b
antisymm
    (
foldr_range_subset_of_range_subset: ∀ {α : Type ?u.5309} {β : Type ?u.5310} {γ : Type ?u.5311} {f : β → α → α} {g : γ → α → α},
  Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (foldr f a) ⊆ Set.range (foldr g a)
foldr_range_subset_of_range_subset 
hfg: Set.range f = Set.range g
hfg.
ge: ∀ {α : Type ?u.5317} [inst : Preorder α] {x y : α}, x = y → y ≤ x
ge 
a: α
a)
#align list.foldr_range_eq_of_range_eq 
List.foldr_range_eq_of_range_eq: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α → α} {g : γ → α → α},
  Set.range f = Set.range g → ∀ (a : α), Set.range (foldr f a) = Set.range (foldr g a)
List.foldr_range_eq_of_range_eq

theorem 
foldl_range_eq_of_range_eq: ∀ {f : α → β → α} {g : α → γ → α},
  ((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)
foldl_range_eq_of_range_eq {
f: α → β → α
f : 
α: Type ?u.5360
α → 
β: Type ?u.5363
β → 
α: Type ?u.5360
α} {
g: α → γ → α
g : 
α: Type ?u.5360
α → 
γ: Type ?u.5366
γ → 
α: Type ?u.5360
α}
    (
hfg: (Set.range fun a c => f c a) = Set.range fun b c => g c b
hfg : (
Set.range: {α : Type ?u.5383} → {ι : Sort ?u.5382} → (ι → α) → Set α
Set.range fun 
a: ?m.5387
a 
c: ?m.5390
c => 
f: α → β → α
f 
c: ?m.5390
c 
a: ?m.5387
a) = 
Set.range: {α : Type ?u.5398} → {ι : Sort ?u.5397} → (ι → α) → Set α
Set.range fun 
b: ?m.5402
b 
c: ?m.5405
c => 
g: α → γ → α
g 
c: ?m.5405
c 
b: ?m.5402
b) (
a: α
a : 
α: Type ?u.5360
α) :
    
Set.range: {α : Type ?u.5420} → {ι : Sort ?u.5419} → (ι → α) → Set α
Set.range (
foldl: {α : Type ?u.5424} → {β : Type ?u.5423} → (α → β → α) → α → List β → α
foldl 
f: α → β → α
f 
a: α
a) = 
Set.range: {α : Type ?u.5441} → {ι : Sort ?u.5440} → (ι → α) → Set α
Set.range (
foldl: {α : Type ?u.5445} → {β : Type ?u.5444} → (α → β → α) → α → List β → α
foldl 
g: α → γ → α
g 
a: α
a) :=
  (
foldl_range_subset_of_range_subset: ∀ {α : Type ?u.5467} {β : Type ?u.5468} {γ : Type ?u.5469} {f : α → β → α} {g : α → γ → α},
  ((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)
foldl_range_subset_of_range_subset 
hfg: (Set.range fun a c => f c a) = Set.range fun b c => g c b
hfg.
le: ∀ {α : Type ?u.5475} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le 
a: α
a).
antisymm: ∀ {α : Type ?u.5804} [inst : HasSubset α] {a b : α} [inst_1 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊆ a → a = b
antisymm
    (
foldl_range_subset_of_range_subset: ∀ {α : Type ?u.5864} {β : Type ?u.5865} {γ : Type ?u.5866} {f : α → β → α} {g : α → γ → α},
  ((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)
foldl_range_subset_of_range_subset 
hfg: (Set.range fun a c => f c a) = Set.range fun b c => g c b
hfg.
ge: ∀ {α : Type ?u.5872} [inst : Preorder α] {x y : α}, x = y → y ≤ x
ge 
a: α
a)
#align list.foldl_range_eq_of_range_eq 
List.foldl_range_eq_of_range_eq: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → α} {g : α → γ → α},
  ((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)
List.foldl_range_eq_of_range_eq

end List