Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Seul Baek

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

/-!
# Lists as Functions

Definitions for using lists as finite representations of finitely-supported functions with domain
ℕ.

These include pointwise operations on lists, as well as get and set operations.

## Notations

An index notation is introduced in this file for setting a particular element of a list. With `as`
as a list `m` as an index, and `a` as a new element, the notation is `as {m ↦ a}`.

So, for example
`[1, 3, 5] {1 ↦ 9}` would result in `[1, 9, 5]`

This notation is in the locale `list.func`.
-/

open List

universe u v w

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w}

namespace List

namespace Func

variable {a: αa : α: Type uα}

variable {as: List αas as1: List αas1 as2: List αas2 as3: List αas3 : List: Type ?u.36927 → Type ?u.36927List α: Type uα}

/-- Elementwise negation of a list -/
def neg: [inst : Neg α] → (as : List α) → ?m.63 asneg [Neg: Type ?u.56 → Type ?u.56Neg α: Type uα] (as: List αas : List: Type ?u.59 → Type ?u.59List α: Type uα) :=
as: List αas.map: {α : Type ?u.68} → {β : Type ?u.67} → (α → β) → List α → List βmap fun a: ?m.84a ↦ -a: ?m.84a
#align list.func.neg List.Func.neg: {α : Type u} → [inst : Neg α] → List α → List αList.Func.neg

variable [Inhabited: Sort ?u.18210 → Sort (max1?u.18210)Inhabited α: Type uα] [Inhabited: Sort ?u.15708 → Sort (max1?u.15708)Inhabited β: Type vβ]

/-- Update element of a list by index. If the index is out of range, extend the list with default
elements
-/
@[simp]
def set: {α : Type u} → [inst : Inhabited α] → α → List α → ℕ → List αset (a: αa : α: Type uα) : List: Type ?u.225 → Type ?u.225List α: Type uα → ℕ: Typeℕ → List: Type ?u.229 → Type ?u.229List α: Type uα
| _ :: as: List αas, 0: ℕ0 => a: αa :: as: List αas
| [], 0: ℕ0 => [a: αa]
| h: αh :: as: List αas, k: ℕk + 1 => h: αh :: set: α → List α → ℕ → List αset a: αa as: List αas k: ℕk
| [], k: ℕk + 1 => default: {α : Sort ?u.460} → [self : Inhabited α] → αdefault :: set: α → List α → ℕ → List αset a: αa ([]: List ?m.608[] : List: Type ?u.606 → Type ?u.606List α: Type uα) k: ℕk
#align list.func.set List.Func.set: {α : Type u} → [inst : Inhabited α] → α → List α → ℕ → List αList.Func.set

-- mathport name: list.func.set
@[inherit_doc]
scoped notation as: ?m.4355 aas " {" m: ?m.2161m " ↦ " a: ?m.2152a "}" => List.Func.set: {α : Type u} → [inst : Inhabited α] → α → List α → ℕ → List αList.Func.set a: ?m.4342a as: ?m.4345as m: ?m.4348m

/-- Get element of a list by index. If the index is out of range, return the default element -/
@[simp]
def get: {α : Type u} → [inst : Inhabited α] → ℕ → List α → αget : ℕ: Typeℕ → List: Type ?u.10879 → Type ?u.10879List α: Type uα → α: Type uα
| _, [] => default: {α : Sort ?u.10905} → [self : Inhabited α] → αdefault
| 0: ℕ0, a: αa :: _ => a: αa
| n: ℕn + 1, _ :: as: List αas => get: ℕ → List α → αget n: ℕn as: List αas
#align list.func.get List.Func.get: {α : Type u} → [inst : Inhabited α] → ℕ → List α → αList.Func.get

/-- Pointwise equality of lists. If lists are different lengths, compare with the default
element.
-/
def Equiv: List α → List α → PropEquiv (as1: List αas1 as2: List αas2 : List: Type ?u.15714 → Type ?u.15714List α: Type uα) : Prop: TypeProp :=
∀ m: ℕm : Nat: TypeNat, get: {α : Type ?u.15724} → [inst : Inhabited α] → ℕ → List α → αget m: ℕm as1: List αas1 = get: {α : Type ?u.15735} → [inst : Inhabited α] → ℕ → List α → αget m: ℕm as2: List αas2
#align list.func.equiv List.Func.Equiv: {α : Type u} → [inst : Inhabited α] → List α → List α → PropList.Func.Equiv

/-- Pointwise operations on lists. If lists are different lengths, use the default element. -/
@[simp]
def pointwise: {α : Type u} →
{β : Type v} → {γ : Type w} → [inst : Inhabited α] → [inst : Inhabited β] → (α → β → γ) → List α → List β → List γpointwise (f: α → β → γf : α: Type uα → β: Type vβ → γ: Type wγ) : List: Type ?u.15785 → Type ?u.15785List α: Type uα → List: Type ?u.15788 → Type ?u.15788List β: Type vβ → List: Type ?u.15790 → Type ?u.15790List γ: Type wγ
| [], [] => []: List ?m.15820[]
| [], b: βb :: bs: List βbs => map: {α : Type ?u.15852} → {β : Type ?u.15851} → (α → β) → List α → List βmap (f: α → β → γf default: {α : Sort ?u.15857} → [self : Inhabited α] → αdefault) (b: βb :: bs: List βbs)
| a: αa :: as: List αas, [] => map: {α : Type ?u.16037} → {β : Type ?u.16036} → (α → β) → List α → List βmap (fun x: ?m.16041x ↦ f: α → β → γf x: ?m.16041x default: {α : Sort ?u.16043} → [self : Inhabited α] → αdefault) (a: αa :: as: List αas)
| a: αa :: as: List αas, b: βb :: bs: List βbs => f: α → β → γf a: αa b: βb :: pointwise: (α → β → γ) → List α → List β → List γpointwise f: α → β → γf as: List αas bs: List βbs
#align list.func.pointwise List.Func.pointwise: {α : Type u} →
{β : Type v} → {γ : Type w} → [inst : Inhabited α] → [inst : Inhabited β] → (α → β → γ) → List α → List β → List γList.Func.pointwise

/-- Pointwise addition on lists. If lists are different lengths, use zero. -/
def add: {α : Type u} → [inst : Zero α] → [inst : Add α] → List α → List α → List αadd {α: Type uα : Type u: Type (u+1)Type u} [Zero: Type ?u.17835 → Type ?u.17835Zero α: Type uα] [Add: Type ?u.17838 → Type ?u.17838Add α: Type uα] : List: Type ?u.17842 → Type ?u.17842List α: Type uα → List: Type ?u.17845 → Type ?u.17845List α: Type uα → List: Type ?u.17847 → Type ?u.17847List α: Type uα :=
@pointwise: {α : Type ?u.17854} →
{β : Type ?u.17853} →
{γ : Type ?u.17852} → [inst : Inhabited α] → [inst : Inhabited β] → (α → β → γ) → List α → List β → List γpointwise α: Type uα α: Type uα α: Type uα ⟨0: ?m.178660⟩ ⟨0: ?m.178960⟩ (· + ·): α → α → α(· + ·)
#align list.func.add List.Func.add: {α : Type u} → [inst : Zero α] → [inst : Add α] → List α → List α → List αList.Func.add

/-- Pointwise subtraction on lists. If lists are different lengths, use zero. -/
def sub: {α : Type u} → [inst : Zero α] → [inst : Sub α] → List α → List α → List αsub {α: Type uα : Type u: Type (u+1)Type u} [Zero: Type ?u.18063 → Type ?u.18063Zero α: Type uα] [Sub: Type ?u.18066 → Type ?u.18066Sub α: Type uα] : List: Type ?u.18070 → Type ?u.18070List α: Type uα → List: Type ?u.18073 → Type ?u.18073List α: Type uα → List: Type ?u.18075 → Type ?u.18075List α: Type uα :=
@pointwise: {α : Type ?u.18082} →
{β : Type ?u.18081} →
{γ : Type ?u.18080} → [inst : Inhabited α] → [inst : Inhabited β] → (α → β → γ) → List α → List β → List γpointwise α: Type uα α: Type uα α: Type uα ⟨0: ?m.180940⟩ ⟨0: ?m.181240⟩ (@Sub.sub: {α : Type ?u.18126} → [self : Sub α] → α → α → αSub.sub α: Type uα _)
#align list.func.sub List.Func.sub: {α : Type u} → [inst : Zero α] → [inst : Sub α] → List α → List α → List αList.Func.sub

-- set
theorem length_set: ∀ {m : ℕ} {as : List α}, length (as {m ↦ a}) = max (length as) (m + 1)length_set : ∀ {m: ℕm : ℕ: Typeℕ} {as: List αas : List: Type ?u.18219 → Type ?u.18219List α: Type uα}, as: List αas {m: ℕm ↦ a: αa}.length: {α : Type ?u.18233} → List α → ℕlength = max: {α : Type ?u.18237} → [self : Max α] → α → α → αmax as: List αas.length: {α : Type ?u.18240} → List α → ℕlength (m: ℕm + 1: ?m.182481)
| 0: ℕ0, [] => rfl: ∀ {α : Sort ?u.18350} {a : α}, a = arfl
| 0: ℕ0, a: αa :: as: List αas => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)rw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)max_eq_left: ∀ {α : Type ?u.18763} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = amax_eq_leftα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = length (a :: as)α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as)]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = length (a :: as)α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as)
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)·α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = length (a :: as) α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = length (a :: as)α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as)rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αlength ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)·α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as) α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as)simp [Nat.le_add_right: ∀ (n k : ℕ), n ≤ n + kNat.le_add_right]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α1 ≤ Nat.succ (length as)
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List α0 + 1 ≤ length (a :: as)exact Nat.succ_le_succ: ∀ {n m : ℕ}, n ≤ m → Nat.succ n ≤ Nat.succ mNat.succ_le_succ (Nat.zero_le: ∀ (n : ℕ), 0 ≤ nNat.zero_le _: ℕ_)Goals accomplished! 🐙
| m: ℕm + 1, [] => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βm: ℕlength ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)have := @length_set: ∀ {m : ℕ} {as : List α}, length (as {m ↦ a}) = max (length as) (m + 1)length_set m: ℕm []: List ?m.19144[]α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βm: ℕthis: length ([] {m ↦ a}) = max (length []) (m + 1)length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βm: ℕlength ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)simp [set: {α : Type ?u.19152} → [inst : Inhabited α] → α → List α → ℕ → List αset, length: {α : Type ?u.19196} → List α → ℕlength, @length_set: ∀ {m : ℕ} {as : List α}, length (as {m ↦ a}) = max (length as) (m + 1)length_set m: ℕm, Nat.zero_max: ∀ {n : ℕ}, max 0 n = nNat.zero_max]Goals accomplished! 🐙
| m: ℕm + 1, _ :: as: List αas => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βm: ℕhead✝: αas: List αlength ((head✝ :: as) {m + 1 ↦ a}) = max (length (head✝ :: as)) (m + 1 + 1)simp [set: {α : Type ?u.20985} → [inst : Inhabited α] → α → List α → ℕ → List αset, length: {α : Type ?u.21026} → List α → ℕlength, @length_set: ∀ {m : ℕ} {as : List α}, length (as {m ↦ a}) = max (length as) (m + 1)length_set m: ℕm, Nat.max_succ_succ: ∀ {m n : ℕ}, max (Nat.succ m) (Nat.succ n) = Nat.succ (max m n)Nat.max_succ_succ]Goals accomplished! 🐙
#align list.func.length_set List.Func.length_set: ∀ {α : Type u} {a : α} [inst : Inhabited α] {m : ℕ} {as : List α}, length (as {m ↦ a}) = max (length as) (m + 1)List.Func.length_set

-- porting note : @[simp] has been removed since `#lint` says this is
theorem get_nil: ∀ {k : ℕ}, get k [] = defaultget_nil {k: ℕk : ℕ: Typeℕ} : (get: {α : Type ?u.23738} → [inst : Inhabited α] → ℕ → List α → αget k: ℕk []: List ?m.23878[] : α: Type uα) = default: {α : Sort ?u.23886} → [self : Inhabited α] → αdefault := byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βk: ℕget k [] = defaultcases k: ℕkα: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βzeroget Nat.zero [] = defaultα: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn✝: ℕsuccget (Nat.succ n✝) [] = default α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βk: ℕget k [] = default<;>α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βzeroget Nat.zero [] = defaultα: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn✝: ℕsuccget (Nat.succ n✝) [] = default α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βk: ℕget k [] = defaultrflGoals accomplished! 🐙
#align list.func.get_nil List.Func.get_nil: ∀ {α : Type u} [inst : Inhabited α] {k : ℕ}, get k [] = defaultList.Func.get_nil

theorem get_eq_default_of_le: ∀ (k : ℕ) {as : List α}, length as ≤ k → get k as = defaultget_eq_default_of_le : ∀ (k: ℕk : ℕ: Typeℕ) {as: List αas : List: Type ?u.24274 → Type ?u.24274List α: Type uα}, as: List αas.length: {α : Type ?u.24279} → List α → ℕlength ≤ k: ℕk → get: {α : Type ?u.24291} → [inst : Inhabited α] → ℕ → List α → αget k: ℕk as: List αas = default: {α : Sort ?u.24301} → [self : Inhabited α] → αdefault
| 0: ℕ0, [], _ => rfl: ∀ {α : Sort ?u.24619} {a : α}, a = arfl
| 0: ℕ0, a: αa :: as: List αas, h1: length (a :: as) ≤ 0h1 => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αh1: length (a :: as) ≤ 0get 0 (a :: as) = defaultcases h1: length (a :: as) ≤ 0h1Goals accomplished! 🐙
| k: ℕk + 1, [], _ => rfl: ∀ {α : Sort ?u.24775} {a : α}, a = arfl
| k: ℕk + 1, _ :: as: List αas, h1: length (head✝ :: as) ≤ k + 1h1 => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βk: ℕhead✝: αas: List αh1: length (head✝ :: as) ≤ k + 1get (k + 1) (head✝ :: as) = defaultapply get_eq_default_of_le: ∀ (k : ℕ) {as : List α}, length as ≤ k → get k as = defaultget_eq_default_of_le k: ℕkα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βk: ℕhead✝: αas: List αh1: length (head✝ :: as) ≤ k + 1length as ≤ k
#align list.func.get_eq_default_of_le List.Func.get_eq_default_of_le: ∀ {α : Type u} [inst : Inhabited α] (k : ℕ) {as : List α}, length as ≤ k → get k as = defaultList.Func.get_eq_default_of_le

@[simp]
theorem get_set: ∀ {α : Type u} [inst : Inhabited α] {a : α} {k : ℕ} {as : List α}, get k (as {k ↦ a}) = aget_set {a: αa : α: Type uα} : ∀ {k: ℕk : ℕ: Typeℕ} {as: List αas : List: Type ?u.25438 → Type ?u.25438List α: Type uα}, get: {α : Type ?u.25442} → [inst : Inhabited α] → ℕ → List α → αget k: ℕk (as: List αas {k: ℕk ↦ a: αa}) = a: αa
| 0: ℕ0, as: List αas => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αget 0 (as {0 ↦ a}) = acases as: List αasα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αnilget 0 ([] {0 ↦ a}) = aα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, head✝: αtail✝: List αconsget 0 ((head✝ :: tail✝) {0 ↦ a}) = a α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αget 0 (as {0 ↦ a}) = a<;>α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αnilget 0 ([] {0 ↦ a}) = aα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, head✝: αtail✝: List αconsget 0 ((head✝ :: tail✝) {0 ↦ a}) = a α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αget 0 (as {0 ↦ a}) = arflGoals accomplished! 🐙
| k: ℕk + 1, as: List αas => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕas: List αget (k + 1) (as {k + 1 ↦ a}) = acases as: List αasα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕnilget (k + 1) ([] {k + 1 ↦ a}) = aα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αconsget (k + 1) ((head✝ :: tail✝) {k + 1 ↦ a}) = a α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕas: List αget (k + 1) (as {k + 1 ↦ a}) = a<;>α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕnilget (k + 1) ([] {k + 1 ↦ a}) = aα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αconsget (k + 1) ((head✝ :: tail✝) {k + 1 ↦ a}) = a α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕas: List αget (k + 1) (as {k + 1 ↦ a}) = asimp [get_set: ∀ {a : α} {k : ℕ} {as : List α}, get k (as {k ↦ a}) = aget_set]Goals accomplished! 🐙
#align list.func.get_set List.Func.get_set: ∀ {α : Type u} [inst : Inhabited α] {a : α} {k : ℕ} {as : List α}, get k (as {k ↦ a}) = aList.Func.get_set

theorem eq_get_of_mem: ∀ {a : α} {as : List α}, a ∈ as → ∃ n, a = get n aseq_get_of_mem {a: αa : α: Type uα} : ∀ {as: List αas : List: Type ?u.26368 → Type ?u.26368List α: Type uα}, a: αa ∈ as: List αas → ∃ n: ℕn : Nat: TypeNat, a: αa = get: {α : Type ?u.26403} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas
| [], h: a ∈ []h => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αh: a ∈ []∃ n, a = get n []cases h: a ∈ []hGoals accomplished! 🐙
| b: αb :: as: List αas, h: a ∈ b :: ash => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a ∈ b :: as∃ n, a = get n (b :: as)rw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a ∈ b :: as∃ n, a = get n (b :: as)mem_cons: ∀ {α : Type ?u.26645} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_consα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = b ∨ a ∈ as∃ n, a = get n (b :: as)]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = b ∨ a ∈ as∃ n, a = get n (b :: as) at h: a ∈ b :: ashα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = b ∨ a ∈ as∃ n, a = get n (b :: as) -- porting note : `mem_cons_iff` is now named `mem_cons`
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a ∈ b :: as∃ n, a = get n (b :: as)cases h: a = b ∨ a ∈ ash with
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = b ∨ a ∈ as∃ n, a = get n (b :: as)| inl: ∀ {a b : Prop}, a → a ∨ binl h: ?m.26692h => α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = binl∃ n, a = get n (b :: as)exact ⟨0: ?m.267350, h: ?m.26692h⟩Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a = b ∨ a ∈ as∃ n, a = get n (b :: as)| inr: ∀ {a b : Prop}, b → a ∨ binr h: ?m.26693h =>
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a ∈ asinr∃ n, a = get n (b :: as)rcases eq_get_of_mem: ∀ {a : α} {as : List α}, a ∈ as → ∃ n, a = get n aseq_get_of_mem h: ?m.26693h with ⟨n, h⟩: ∃ n, a = get n as⟨n: ℕn⟨n, h⟩: ∃ n, a = get n as, h: a = get n ash⟨n, h⟩: ∃ n, a = get n as⟩α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh✝: a ∈ asn: ℕh: a = get n asinr.intro∃ n, a = get n (b :: as)
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa, b: αas: List αh: a ∈ asinr∃ n, a = get n (b :: as)exact ⟨n: ℕn + 1: ?m.268261, h: a = get n ash⟩Goals accomplished! 🐙
#noalign list.func.eq_get_of_mem
-- porting note : the signature has been changed to correct what was presumably a bug,
-- hence the #noalign

theorem mem_get_of_le: ∀ {α : Type u} [inst : Inhabited α] {n : ℕ} {as : List α}, n < length as → get n as ∈ asmem_get_of_le : ∀ {n: ℕn : ℕ: Typeℕ} {as: List αas : List: Type ?u.27084 → Type ?u.27084List α: Type uα}, n: ℕn < as: List αas.length: {α : Type ?u.27089} → List α → ℕlength → get: {α : Type ?u.27115} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas ∈ as: List αas
| _, [], h1: x✝ < length []h1 => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: x✝ < length []get x✝ [] ∈ []cases h1: x✝ < length []h1Goals accomplished! 🐙
-- porting note : needed to add to `rw [mem_cons] here` in the two cases below
-- and in other lemmas (presumably because previously lean could see through the def of `mem` ?)
| 0: ℕ0, a: αa :: as: List αas, _ => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) ∈ a :: asrw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) ∈ a :: asmem_cons: ∀ {α : Type ?u.27767} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_consα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as;α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: 0 < length (a :: as)get 0 (a :: as) ∈ a :: asexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl rfl: ∀ {α : Sort ?u.27793} {a : α}, a = arflGoals accomplished! 🐙
| n: ℕn + 1, a: αa :: as: List αas, h1: n + 1 < length (a :: as)h1 => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asrw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asmem_cons: ∀ {α : Type ?u.27812} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_consα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as;α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asapply Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inrα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)hget (n + 1) (a :: as) ∈ as;α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)hget (n + 1) (a :: as) ∈ as α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asunfold get: {α : Type u} → [inst : Inhabited α] → ℕ → List α → αgetα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)hget (Nat.add n 0) as ∈ as
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asapply mem_get_of_le: ∀ {n : ℕ} {as : List α}, n < length as → get n as ∈ asmem_get_of_leα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)h.aNat.add n 0 < length as
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: n + 1 < length (a :: as)get (n + 1) (a :: as) ∈ a :: asapply Nat.lt_of_succ_lt_succ: ∀ {n m : ℕ}, Nat.succ n < Nat.succ m → n < mNat.lt_of_succ_lt_succ h1: n + 1 < length (a :: as)h1Goals accomplished! 🐙
#align list.func.mem_get_of_le List.Func.mem_get_of_le: ∀ {α : Type u} [inst : Inhabited α] {n : ℕ} {as : List α}, n < length as → get n as ∈ asList.Func.mem_get_of_le

theorem mem_get_of_ne_zero: ∀ {n : ℕ} {as : List α}, get n as ≠ default → get n as ∈ asmem_get_of_ne_zero : ∀ {n: ℕn : ℕ: Typeℕ} {as: List αas : List: Type ?u.28583 → Type ?u.28583List α: Type uα}, get: {α : Type ?u.28589} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas ≠ default: {α : Sort ?u.28736} → [self : Inhabited α] → αdefault → get: {α : Type ?u.28891} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas ∈ as: List αas
| _, [], h1: get x✝ [] ≠ defaulth1 => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaultget x✝ [] ∈ []exfalsoα: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthFalse;α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthFalse α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaultget x✝ [] ∈ []apply h1: get x✝ [] ≠ defaulth1α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthget x✝ [] = default;α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthget x✝ [] = default α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaultget x✝ [] ∈ []rw [α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthget x✝ [] = defaultget_nil: ∀ {α : Type ?u.29481} [inst : Inhabited α] {k : ℕ}, get k [] = defaultget_nilα: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βx✝: ℕh1: get x✝ [] ≠ defaulthdefault = default]Goals accomplished! 🐙
| 0: ℕ0, a: αa :: as: List αas, _ => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) ∈ a :: asrw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) ∈ a :: asmem_cons: ∀ {α : Type ?u.29774} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_consα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as;α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αx✝: get 0 (a :: as) ≠ defaultget 0 (a :: as) ∈ a :: asexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl rfl: ∀ {α : Sort ?u.29800} {a : α}, a = arflGoals accomplished! 🐙
| n: ℕn + 1, a: αa :: as: List αas, h1: get (n + 1) (a :: as) ≠ defaulth1 => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) ∈ a :: asrw [α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) ∈ a :: asmem_cons: ∀ {α : Type ?u.29819} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_consα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as]α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as;α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) ∈ a :: asunfold get: {α : Type u} → [inst : Inhabited α] → ℕ → List α → αgetα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (Nat.add n 0) as = a ∨ get (Nat.add n 0) as ∈ as
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) ∈ a :: asapply Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (mem_get_of_ne_zero: ∀ {n : ℕ} {as : List α}, get n as ≠ default → get n as ∈ asmem_get_of_ne_zero _: get ?m.29949 ?m.29950 ≠ default_)α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (Nat.add n 0) as ≠ default
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βn: ℕa: αas: List αh1: get (n + 1) (a :: as) ≠ defaultget (n + 1) (a :: as) ∈ a :: asapply h1: get (n + 1) (a :: as) ≠ defaulth1Goals accomplished! 🐙
#align list.func.mem_get_of_ne_zero List.Func.mem_get_of_ne_zero: ∀ {α : Type u} [inst : Inhabited α] {n : ℕ} {as : List α}, get n as ≠ default → get n as ∈ asList.Func.mem_get_of_ne_zero

theorem get_set_eq_of_ne: ∀ {α : Type u} [inst : Inhabited α] {a : α} {as : List α} (k m : ℕ), m ≠ k → get m (as {k ↦ a}) = get m asget_set_eq_of_ne {a: αa : α: Type uα} :
∀ {as: List αas : List: Type ?u.30172 → Type ?u.30172List α: Type uα} (k: ℕk : ℕ: Typeℕ) (m: ℕm : ℕ: Typeℕ), m: ℕm ≠ k: ℕk → get: {α : Type ?u.30184} → [inst : Inhabited α] → ℕ → List α → αget m: ℕm (as: List αas {k: ℕk ↦ a: αa}) = get: {α : Type ?u.30334} → [inst : Inhabited α] → ℕ → List α → αget m: ℕm as: List αas
| as: List αas, 0: ℕ0, m: ℕm, h1: m ≠ 0h1 => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αm: ℕh1: m ≠ 0get m (as {0 ↦ a}) = get m ascases m: ℕmα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αh1: Nat.zero ≠ 0zeroget Nat.zero (as {0 ↦ a}) = get Nat.zero asα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αn✝: ℕh1: Nat.succ n✝ ≠ 0succget (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) as
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αm: ℕh1: m ≠ 0get m (as {0 ↦ a}) = get m ascontradictionα: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αn✝: ℕh1: Nat.succ n✝ ≠ 0succget (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) as
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αm: ℕh1: m ≠ 0get m (as {0 ↦ a}) = get m ascases as: List αasα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αn✝: ℕh1: Nat.succ n✝ ≠ 0succ.nilget (Nat.succ n✝) ([] {0 ↦ a}) = get (Nat.succ n✝) []α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αn✝: ℕh1: Nat.succ n✝ ≠ 0head✝: αtail✝: List αsucc.consget (Nat.succ n✝) ((head✝ :: tail✝) {0 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝) α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αn✝: ℕh1: Nat.succ n✝ ≠ 0succget (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) as<;>α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αn✝: ℕh1: Nat.succ n✝ ≠ 0succ.nilget (Nat.succ n✝) ([] {0 ↦ a}) = get (Nat.succ n✝) []α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αn✝: ℕh1: Nat.succ n✝ ≠ 0head✝: αtail✝: List αsucc.consget (Nat.succ n✝) ((head✝ :: tail✝) {0 ↦ a}) = get (Nat.succ n✝) (head✝ :: tail✝) α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αn✝: ℕh1: Nat.succ n✝ ≠ 0succget (Nat.succ n✝) (as {0 ↦ a}) = get (Nat.succ n✝) assimp only [set: {α : Type ?u.30953} → [inst : Inhabited α] → α → List α → ℕ → List αset, get: {α : Type ?u.30830} → [inst : Inhabited α] → ℕ → List α → αget, get_nil: ∀ {α : Type ?u.30864} [inst : Inhabited α] {k : ℕ}, get k [] = defaultget_nil]Goals accomplished! 🐙
| as: List αas, k: ℕk + 1, m: ℕm, h1: m ≠ k + 1h1 => byGoals accomplished! 🐙
-- porting note : I somewhat rearranged the case split
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αk, m: ℕh1: m ≠ k + 1get m (as {k + 1 ↦ a}) = get m ascase nil =>
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕh1: Nat.zero ≠ k + 1get Nat.zero ([] {k + 1 ↦ a}) = get Nat.zero []simp only [set: {α : Type ?u.31229} → [inst : Inhabited α] → α → List α → ℕ → List αset, get: {α : Type ?u.31267} → [inst : Inhabited α] → ℕ → List α → αget]Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αk, m: ℕh1: m ≠ k + 1get m (as {k + 1 ↦ a}) = get m ascase nil m: ℕm =>
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []have h3: get m ([] {k ↦ a}) = defaulth3 : get: {α : Type ?u.31322} → [inst : Inhabited α] → ℕ → List α → αget m: ℕm (nil: {α : Type ?u.31465} → List αnil {k: ℕk ↦ a: αa}) = default: {α : Sort ?u.31467} → [self : Inhabited α] → αdefault := α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultrw [α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultget_set_eq_of_ne: ∀ {a : α} {as : List α} (k m : ℕ), m ≠ k → get m (as {k ↦ a}) = get m asget_set_eq_of_ne k: ℕk m: ℕm,α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m [] = defaultα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1m ≠ k α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultget_nil: ∀ {α : Type ?u.31753} [inst : Inhabited α] {k : ℕ}, get k [] = defaultget_nilα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1default = defaultα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1m ≠ k]α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1m ≠ k
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultintro hc: m = khcα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1hc: m = kFalse
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultapply h1: Nat.succ m ≠ k + 1h1α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1hc: m = kNat.succ m = k + 1
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get m ([] {k ↦ a}) = defaultsimp [hc: m = khc]Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk, m: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ([] {k + 1 ↦ a}) = get (Nat.succ m) []apply h3: get m ([] {k ↦ a}) = defaulth3Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αk, m: ℕh1: m ≠ k + 1get m (as {k + 1 ↦ a}) = get m ascase zero =>
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αh1: Nat.zero ≠ k + 1get Nat.zero ((head✝ :: tail✝) {k + 1 ↦ a}) = get Nat.zero (head✝ :: tail✝)simp only [set: {α : Type ?u.32124} → [inst : Inhabited α] → α → List α → ℕ → List αset, get: {α : Type ?u.32162} → [inst : Inhabited α] → ℕ → List α → αget]Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa✝: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αas: List αk, m: ℕh1: m ≠ k + 1get m (as {k + 1 ↦ a}) = get m ascase _ _ m: ℕm =>
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)apply get_set_eq_of_ne: ∀ {a : α} {as : List α} (k m : ℕ), m ≠ k → get m (as {k ↦ a}) = get m asget_set_eq_of_ne k: ℕk m: ℕmα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1m ≠ k
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)intro hc: m = khcα: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1hc: m = kFalse
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)apply h1: Nat.succ m ≠ k + 1h1α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1hc: m = kNat.succ m = k + 1
α: Type uβ: Type vγ: Type wa✝: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βa: αk: ℕhead✝: αtail✝: List αm: ℕh1: Nat.succ m ≠ k + 1get (Nat.succ m) ((head✝ :: tail✝) {k + 1 ↦ a}) = get (Nat.succ m) (head✝ :: tail✝)simp [hc: m = khc]Goals accomplished! 🐙
#align list.func.get_set_eq_of_ne List.Func.get_set_eq_of_ne: ∀ {α : Type u} [inst : Inhabited α] {a : α} {as : List α} (k m : ℕ), m ≠ k → get m (as {k ↦ a}) = get m asList.Func.get_set_eq_of_ne

theorem get_map: ∀ {f : α → β} {n : ℕ} {as : List α}, n < length as → get n (map f as) = f (get n as)get_map {f: α → βf : α: Type uα → β: Type vβ} :
∀ {n: ℕn : ℕ: Typeℕ} {as: List αas : List: Type ?u.32615 → Type ?u.32615List α: Type uα}, n: ℕn < as: List αas.length: {α : Type ?u.32620} → List α → ℕlength → get: {α : Type ?u.32632} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn (as: List αas.map: {α : Type ?u.32636} → {β : Type ?u.32635} → (α → β) → List α → List βmap f: α → βf) = f: α → βf (get: {α : Type ?u.32654} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas)
| _, [], h: x✝ < length []h => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αas, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βx✝: ℕh: x✝ < length []get x✝ (map f []) = f (get x✝ [])cases h: x✝ < length []hGoals accomplished! 🐙
| 0: ℕ0, a: αa :: as: List αas, _ => rfl: ∀ {α : Sort ?u.32888} {a : α}, a = arfl
| n: ℕn + 1, _ :: as: List αas, h1: n + 1 < length (head✝ :: as)h1 => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕhead✝: αas: List αh1: n + 1 < length (head✝ :: as)get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))have h2: n < length ash2 : n: ℕn < length: {α : Type ?u.33321} → List α → ℕlength as: List αas := α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕhead✝: αas: List αh1: n + 1 < length (head✝ :: as)get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕhead✝: αas: List αh1: n + 1 < length (head✝ :: as)n < length asapply h1: n + 1 < length (head✝ :: as)h1Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕhead✝: αas: List αh1: n + 1 < length (head✝ :: as)get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))apply get_map: ∀ {f : α → β} {n : ℕ} {as : List α}, n < length as → get n (map f as) = f (get n as)get_map h2: n < length ash2Goals accomplished! 🐙
#align list.func.get_map List.Func.get_map: ∀ {α : Type u} {β : Type v} [inst : Inhabited α] [inst_1 : Inhabited β] {f : α → β} {n : ℕ} {as : List α},
n < length as → get n (map f as) = f (get n as)List.Func.get_map

theorem get_map': ∀ {f : α → β} {n : ℕ} {as : List α}, f default = default → get n (map f as) = f (get n as)get_map' {f: α → βf : α: Type uα → β: Type vβ} {n: ℕn : ℕ: Typeℕ} {as: List αas : List: Type ?u.33575 → Type ?u.33575List α: Type uα} :
f: α → βf default: {α : Sort ?u.33580} → [self : Inhabited α] → αdefault = default: {α : Sort ?u.33725} → [self : Inhabited α] → αdefault → get: {α : Type ?u.34008} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn (as: List αas.map: {α : Type ?u.34012} → {β : Type ?u.34011} → (α → β) → List α → List βmap f: α → βf) = f: α → βf (get: {α : Type ?u.34025} → [inst : Inhabited α] → ℕ → List α → αget n: ℕn as: List αas) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αf default = default → get n (map f as) = f (get n as)intro h1: f default = defaulth1α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaultget n (map f as) = f (get n as);α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaultget n (map f as) = f (get n as) α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αf default = default → get n (map f as) = f (get n as)by_cases h2: ?m.34208h2 : n: ℕn < as: List αas.length: {α : Type ?u.34175} → List α → ℕlengthα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: n < length asposget n (map f as) = f (get n as)α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αf default = default → get n (map f as) = f (get n as)·α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: n < length asposget n (map f as) = f (get n as) α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: n < length asposget n (map f as) = f (get n as)α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)apply get_map: ∀ {α : Type ?u.34216} {β : Type ?u.34215} [inst : Inhabited α] [inst_1 : Inhabited β] {f : α → β} {n : ℕ} {as : List α},
n < length as → get n (map f as) = f (get n as)get_map h2: ?m.34201h2Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αf default = default → get n (map f as) = f (get n as)·α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as) α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)rw [α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)not_lt: ∀ {α : Type ?u.34526} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ anot_ltα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as)]α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as) at h2: ?m.34208h2α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as)
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)rw [α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as)get_eq_default_of_le: ∀ {α : Type ?u.34610} [inst : Inhabited α] (k : ℕ) {as : List α}, length as ≤ k → get k as = defaultget_eq_default_of_le _: ℕ_ h2: length as ≤ nh2,α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f default α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as)get_eq_default_of_le: ∀ {α : Type ?u.34628} [inst : Inhabited α] (k : ℕ) {as : List α}, length as ≤ k → get k as = defaultget_eq_default_of_le,α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegdefault = f defaultα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength (map f as) ≤ n α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegget n (map f as) = f (get n as)h1: f default = defaulth1α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nnegdefault = defaultα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength (map f as) ≤ n]α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength (map f as) ≤ n
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)rw [α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength (map f as) ≤ nlength_map: ∀ {α : Type ?u.34920} {β : Type ?u.34919} (as : List α) (f : α → β), length (map f as) = length aslength_mapα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength as ≤ n]α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: length as ≤ nneg.alength as ≤ n
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βf: α → βn: ℕas: List αh1: f default = defaulth2: ¬n < length asnegget n (map f as) = f (get n as)apply h2: length as ≤ nh2Goals accomplished! 🐙
#align list.func.get_map' List.Func.get_map': ∀ {α : Type u} {β : Type v} [inst : Inhabited α] [inst_1 : Inhabited β] {f : α → β} {n : ℕ} {as : List α},
f default = default → get n (map f as) = f (get n as)List.Func.get_map'

theorem forall_val_of_forall_mem: ∀ {α : Type u} [inst : Inhabited α] {as : List α} {p : α → Prop},
p default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)forall_val_of_forall_mem {as: List αas : List: Type ?u.35030 → Type ?u.35030List α: Type uα} {p: α → Propp : α: Type uα → Prop: TypeProp} :
p: α → Propp default: {α : Sort ?u.35038} → [self : Inhabited α] → αdefault → (∀ x: ?m.35186x ∈ as: List αas, p: α → Propp x: ?m.35186x) → ∀ n: ?m.35220n, p: α → Propp (get: {α : Type ?u.35223} → [inst : Inhabited α] → ℕ → List α → αget n: ?m.35220n as: List αas) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Propp default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)intro h1: p defaulth1 h2: ∀ (x : α), x ∈ as → p xh2 n: ℕnα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕp (get n as)
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Propp default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)by_cases h3: ?m.35403h3 : n: ℕn < as: List αas.length: {α : Type ?u.35377} → List α → ℕlengthα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: n < length asposp (get n as)α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as)
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Propp default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)·α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: n < length asposp (get n as) α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: n < length asposp (get n as)α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as)apply h2: ∀ (x : α), x ∈ as → p xh2 _: α_ (mem_get_of_le: ∀ {α : Type ?u.35418} [inst : Inhabited α] {n : ℕ} {as : List α}, n < length as → get n as ∈ asmem_get_of_le h3: ?m.35403h3)Goals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Propp default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (get n as)·α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as) α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as)rw [α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as)not_lt: ∀ {α : Type ?u.35576} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ anot_ltα: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: length as ≤ nnegp (get n as)]α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: length as ≤ nnegp (get n as) at h3: ?m.35410h3α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: length as ≤ nnegp (get n as)
α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2: ∀ (x : α), x ∈ as → p xn: ℕh3: ¬n < length asnegp (get n as)rw [α: Type uβ: Type vγ: Type wa: αas✝, as1, as2, as3: List αinst✝¹: Inhabited αinst✝: Inhabited βas: List αp: α → Proph1: p defaulth2```