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
Cmd instead of
Ctrl .
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
! This file was ported from Lean 3 source module data.list.basic
! leanprover-community/mathlib commit 9da1b3534b65d9661eb8f42443598a92bbb49211
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Init.Data.List.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.List.Defs
import Mathlib.Init.Core
import Std.Data.List.Lemmas
/-!
# Basic properties of lists
-/
open Function
open Nat hiding one_pos
assert_not_exists Set.range
namespace List
universe u v w x
variable { ι : Type _ : Type (?u.72291+1)} { α : Type u } { β : Type v } { γ : Type w } { δ : Type x } { l₁ l₂ : List α }
-- Porting note: Delete this attribute
-- attribute [inline] List.head!
/-- There is only one list of an empty type -/
instance uniqueOfIsEmpty [ IsEmpty α ] : Unique ( List α ) :=
{ instInhabitedList with
uniq := fun l =>
match l with
| [] => rfl : ∀ {α : Sort ?u.71} {a : α }, a = a
| a :: _ => isEmptyElim : ∀ {α : Sort ?u.100} [inst : IsEmpty α p : α → Sort ?u.99a : α ), p a a }
#align list.unique_of_is_empty List.uniqueOfIsEmpty
instance : IsLeftId ( List α ) Append.append : {α : Type ?u.269} → [self : Append α α → α → α [] :=
⟨ nil_append : ∀ {α : Type ?u.313} (as : List α [] ++ as = as ⟩
instance : IsRightId ( List α ) Append.append : {α : Type ?u.358} → [self : Append α α → α → α [] :=
⟨ append_nil : ∀ {α : Type ?u.402} (as : List α as ++ [] = as ⟩
instance : IsAssociative : (α : Type ?u.445) → (α → α → α Prop ( List α ) Append.append : {α : Type ?u.447} → [self : Append α α → α → α :=
⟨ append_assoc : ∀ {α : Type ?u.486} (as bs cs : List α as ++ bs ++ cs = as ++ (bs ++ cs ⟩
#align list.cons_ne_nil List.cons_ne_nil : ∀ {α : Type u_1} (a : α ) (l : List α a :: l ≠ []
#align list.cons_ne_self List.cons_ne_self : ∀ {α : Type u_1} (a : α ) (l : List α a :: l ≠ l
#align list.head_eq_of_cons_eq List.head_eq_of_cons_eqₓ : ∀ {α : Type u_1} {h₁ : α } {t₁ : List α h₂ : α } {t₂ : List α h₁ :: t₁ = h₂ :: t₂ h₁ = h₂ -- implicits order
#align list.tail_eq_of_cons_eq List.tail_eq_of_cons_eqₓ : ∀ {α : Type u_1} {h₁ : α } {t₁ : List α h₂ : α } {t₂ : List α h₁ :: t₁ = h₂ :: t₂ t₁ = t₂ -- implicits order
@[ simp ] theorem cons_injective { a : α } : Injective : {α : Sort ?u.538} → {β : Sort ?u.537} → (α → β Prop ( cons a ) := fun _ _ => tail_eq_of_cons_eq : ∀ {α : Type ?u.558} {h₁ : α } {t₁ : List α h₂ : α } {t₂ : List α h₁ :: t₁ = h₂ :: t₂ t₁ = t₂
#align list.cons_injective List.cons_injective
#align list.cons_inj List.cons_inj : ∀ {α : Type u_1} (a : α ) {l l' : List α a :: l = a :: l' ↔ l = l'
theorem cons_eq_cons : ∀ {α : Type u} {a b : α } {l l' : List α a :: l = b :: l' ↔ a = b ∧ l = l' cons_eq_cons { a b : α } { l l' : List α } : a :: l = b :: l' ↔ a = b ∧ l = l' :=
⟨ List.cons.inj : ∀ {α : Type ?u.645} {head : α } {tail : List α head_1 : α } {tail_1 : List α head :: tail = head_1 :: tail_1 head = head_1 ∧ tail = tail_1 , fun h => h . 1 : ∀ {a b : Prop }, a ∧ b a ▸ h . 2 : ∀ {a b : Prop }, a ∧ b b ▸ rfl : ∀ {α : Sort ?u.669} {a : α }, a = a ⟩
#align list.cons_eq_cons List.cons_eq_cons : ∀ {α : Type u} {a b : α } {l l' : List α a :: l = b :: l' ↔ a = b ∧ l = l'
theorem singleton_injective : Injective : {α : Sort ?u.715} → {β : Sort ?u.714} → (α → β Prop fun a : α => [ a ] := fun _ _ h => ( cons_eq_cons : ∀ {α : Type ?u.738} {a b : α } {l l' : List α a :: l = b :: l' ↔ a = b ∧ l = l' . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 1 : ∀ {a b : Prop }, a ∧ b a
#align list.singleton_injective List.singleton_injective
theorem singleton_inj : ∀ {α : Type u} {a b : α }, [a ] = [b ] ↔ a = b singleton_inj { a b : α } : [ a ] = [ b ] ↔ a = b :=
singleton_injective . eq_iff : ∀ {α : Sort ?u.812} {β : Sort ?u.813} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b
#align list.singleton_inj List.singleton_inj : ∀ {α : Type u} {a b : α }, [a ] = [b ] ↔ a = b
#align list.exists_cons_of_ne_nil List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α l ≠ [] ∃ b L , l = b :: L
theorem set_of_mem_cons : ∀ {α : Type u} (l : List α a : α ), { x | x ∈ a :: l = insert a { x | x ∈ l set_of_mem_cons ( l : List α ) ( a : α ) : { x | x ∈ a :: l } = insert a { x | x ∈ l } :=
Set.ext : ∀ {α : Type ?u.938} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ => mem_cons : ∀ {α : Type ?u.949} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l
#align list.set_of_mem_cons List.set_of_mem_cons : ∀ {α : Type u} (l : List α a : α ), { x | x ∈ a :: l = insert a { x | x ∈ l
/-! ### mem -/
#align list.mem_singleton_self List.mem_singleton_self : ∀ {α : Type u_1} (a : α ), a ∈ [a ]
#align list.eq_of_mem_singleton List.eq_of_mem_singleton : ∀ {α : Type u_1} {a b : α }, a ∈ [b ] a = b
#align list.mem_singleton List.mem_singleton : ∀ {α : Type u_1} {a b : α }, a ∈ [b ] ↔ a = b
#align list.mem_of_mem_cons_of_mem List.mem_of_mem_cons_of_mem : ∀ {α : Type u_1} {a b : α } {l : List α a ∈ b :: l b ∈ l a ∈ l
theorem _root_.Decidable.List.eq_or_ne_mem_of_mem : ∀ [inst : DecidableEq α a b : α } {l : List α a ∈ b :: l a = b ∨ a ≠ b ∧ a ∈ l _root_.Decidable.List.eq_or_ne_mem_of_mem [ DecidableEq : Sort ?u.996 → Sort (max1?u.996) α ]
{ a b : α } { l : List α } ( h : a ∈ b :: l ) : a = b ∨ a ≠ b ∧ a ∈ l := by
by_cases hab : a = b
· exact Or.inl : ∀ {a b : Prop }, a → a ∨ b hab
· exact (( List.mem_cons : ∀ {α : Type ?u.1097} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c elim Or.inl : ∀ {a b : Prop }, a → a ∨ b ( fun h => Or.inr : ∀ {a b : Prop }, b → a ∨ b ⟨ hab , h ⟩))
#align decidable.list.eq_or_ne_mem_of_mem Decidable.List.eq_or_ne_mem_of_mem
#align list.eq_or_ne_mem_of_mem List.eq_or_ne_mem_of_mem : ∀ {α : Type u_1} {a b : α } {l : List α a ∈ b :: l a = b ∨ a ≠ b ∧ a ∈ l
-- porting note: from init.data.list.lemmas
alias mem_cons : ∀ {α : Type u_1} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ↔ eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {a b : α } {l : List α a ∈ b :: l a = b ∨ a ∈ l _
#align list.eq_or_mem_of_mem_cons List.eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {a b : α } {l : List α a ∈ b :: l a = b ∨ a ∈ l
#align list.not_mem_append List.not_mem_append : ∀ {α : Type u_1} {a : α } {s t : List α ¬ a ∈ s ¬ a ∈ t ¬ a ∈ s ++ t
#align list.ne_nil_of_mem List.ne_nil_of_mem : ∀ {α : Type u_1} {a : α } {l : List α a ∈ l l ≠ []
theorem mem_split : ∀ {a : α } {l : List α a ∈ l ∃ s t , l = s ++ a :: t mem_split { a : α } { l : List α } ( h : a ∈ l ) : ∃ s t : List α , l = s ++ a :: t := by
induction' l with b l ih ; { cases h } ; rcases h with ( _ | ⟨ _ , h ⟩ )
· exact ⟨ [] , l , rfl : ∀ {α : Sort ?u.1578} {a : α }, a = a ⟩
· rcases ih h with ⟨s, t, rfl⟩ : ∃ s t , l = s ++ a :: t s ⟨s, t, rfl⟩ : ∃ s t , l = s ++ a :: t t ⟨s, t, rfl⟩ : ∃ s t , l = s ++ a :: t rfl ⟨s, t, rfl⟩ : ∃ s t , l = s ++ a :: t
exact ⟨ b :: s , t , rfl : ∀ {α : Sort ?u.1685} {a : α }, a = a ⟩
#align list.mem_split List.mem_split : ∀ {α : Type u} {a : α } {l : List α a ∈ l ∃ s t , l = s ++ a :: t
#align list.mem_of_ne_of_mem List.mem_of_ne_of_mem : ∀ {α : Type u_1} {a y : α } {l : List α a ≠ y a ∈ y :: l a ∈ l
#align list.ne_of_not_mem_cons List.ne_of_not_mem_cons : ∀ {α : Type u_1} {a b : α } {l : List α ¬ a ∈ b :: l a ≠ b
#align list.not_mem_of_not_mem_cons List.not_mem_of_not_mem_cons : ∀ {α : Type u_1} {a b : α } {l : List α ¬ a ∈ b :: l ¬ a ∈ l
#align list.not_mem_cons_of_ne_of_not_mem List.not_mem_cons_of_ne_of_not_mem : ∀ {α : Type u_1} {a y : α } {l : List α a ≠ y ¬ a ∈ l ¬ a ∈ y :: l
#align list.ne_and_not_mem_of_not_mem_cons List.ne_and_not_mem_of_not_mem_cons : ∀ {α : Type u_1} {a y : α } {l : List α ¬ a ∈ y :: l a ≠ y ∧ ¬ a ∈ l
#align list.mem_map List.mem_map : ∀ {α : Type u_1} {β : Type u_2} {b : β } {f : α → β l : List α b ∈ map f l ↔ ∃ a , a ∈ l ∧ f a = b
#align list.exists_of_mem_map List.exists_of_mem_map : ∀ {α : Type u_1} {b : α } {α_1 : Type u_2} {f : α_1 → α l : List α_1 b ∈ map f l ∃ a , a ∈ l ∧ f a = b
#align list.mem_map_of_mem List.mem_map_of_memₓ : ∀ {α : Type u_1} {β : Type u_2} {a : α } {l : List α f : α → β a ∈ l f a ∈ map f l -- implicits order
theorem mem_map_of_injective { f : α → β } ( H : Injective : {α : Sort ?u.1809} → {β : Sort ?u.1808} → (α → β Prop f ) { a : α } { l : List α } :
f a ∈ map f l ↔ a ∈ l :=
⟨ fun m => let ⟨ _ , m' , e ⟩ := exists_of_mem_map : ∀ {α : Type ?u.1875} {b : α } {α_1 : Type ?u.1876} {f : α_1 → α l : List α_1 b ∈ map f l ∃ a , a ∈ l ∧ f a = b m ; H e ▸ m' , mem_map_of_mem : ∀ {α : Type ?u.2063} {β : Type ?u.2064} {a : α } {l : List α f : α → β a ∈ l f a ∈ map f l _ ⟩
#align list.mem_map_of_injective List.mem_map_of_injective
@[ simp ]
theorem _root_.Function.Involutive.exists_mem_and_apply_eq_iff : ∀ {α : Type u} {f : α → α Involutive f ∀ (x : α ) (l : List α (∃ y , y ∈ l ∧ f y = x ) ↔ f x ∈ l _root_.Function.Involutive.exists_mem_and_apply_eq_iff { f : α → α }
( hf : Function.Involutive : {α : Sort ?u.2132} → (α → α Prop f ) ( x : α ) ( l : List α ) : (∃ y : α , y ∈ l ∧ f y = x ) ↔ f x ∈ l :=
⟨ by (∃ y , y ∈ l ∧ f y = x ) → f x ∈ l rintro ⟨y, h, rfl⟩ : ∃ y , y ∈ l ∧ f y = x y ⟨y, h, rfl⟩ : ∃ y , y ∈ l ∧ f y = x h ⟨y, h, rfl⟩ : ∃ y , y ∈ l ∧ f y = x rfl ⟨y, h, rfl⟩ : ∃ y , y ∈ l ∧ f y = x ; (∃ y , y ∈ l ∧ f y = x ) → f x ∈ l rwa [ hf y ] , fun h => ⟨ f x , h , hf _ ⟩⟩
#align function.involutive.exists_mem_and_apply_eq_iff Function.Involutive.exists_mem_and_apply_eq_iff : ∀ {α : Type u} {f : α → α Involutive f ∀ (x : α ) (l : List α (∃ y , y ∈ l ∧ f y = x ) ↔ f x ∈ l
theorem mem_map_of_involutive { f : α → α } ( hf : Involutive : {α : Sort ?u.2342} → (α → α Prop f ) { a : α } { l : List α } :
a ∈ map f l ↔ f a ∈ l := by rw [ mem_map : ∀ {α : Type ?u.2388} {β : Type ?u.2389} {b : β } {f : α → β l : List α b ∈ map f l ↔ ∃ a , a ∈ l ∧ f a = b , (∃ a_1 , a_1 ∈ l ∧ f a_1 = a ) ↔ f a ∈ l hf . exists_mem_and_apply_eq_iff : ∀ {α : Type ?u.2410} {f : α → α Involutive f ∀ (x : α ) (l : List α (∃ y , y ∈ l ∧ f y = x ) ↔ f x ∈ l ]
#align list.mem_map_of_involutive List.mem_map_of_involutive
#align list.forall_mem_map_iff List.forall_mem_map_iffₓ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β l : List α P : β → Prop (∀ (i : β ), i ∈ map f l P i ) ↔ ∀ (j : α ), j ∈ l P (f j -- universe order
#align list.map_eq_nil List.map_eq_nilₓ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β l : List α map f l = [] ↔ l = [] -- universe order
attribute [ simp ] List.mem_join
#align list.mem_join List.mem_join
#align list.exists_of_mem_join List.exists_of_mem_join : ∀ {α : Type u_1} {a : α } {L : List (List α a ∈ join L ∃ l , l ∈ L ∧ a ∈ l
#align list.mem_join_of_mem List.mem_join_of_memₓ -- implicits order
attribute [ simp ] List.mem_bind
#align list.mem_bind List.mem_bindₓ -- implicits order
-- Porting note: bExists in Lean3, And in Lean4
#align list.exists_of_mem_bind List.exists_of_mem_bindₓ -- implicits order
#align list.mem_bind_of_mem List.mem_bind_of_memₓ -- implicits order
#align list.bind_map List.bind_mapₓ -- implicits order
theorem map_bind ( g : β → List γ ) ( f : α → β ) :
∀ l : List α , ( List.map f l ). bind g = l . bind fun a => g ( f a )
| [] => rfl : ∀ {α : Sort ?u.2594} {a : α }, a = a
| a :: l => by simp only [ cons_bind , map_cons : ∀ {α : Type ?u.2775} {β : Type ?u.2776} (f : α → β a : α ) (l : List α map f (a :: l = f a :: map f l , map_bind _ _ l ]
#align list.map_bind List.map_bind
/-! ### length -/
#align list.length_eq_zero List.length_eq_zero
#align list.length_singleton List.length_singleton : ∀ {α : Type u_1} (a : α ), length [a ] = 1
#align list.length_pos_of_mem List.length_pos_of_mem : ∀ {α : Type u_1} {a : α } {l : List α a ∈ l 0 < length l
#align list.exists_mem_of_length_pos List.exists_mem_of_length_pos : ∀ {α : Type u_1} {l : List α 0 < length l ∃ a , a ∈ l
#align list.length_pos_iff_exists_mem List.length_pos_iff_exists_mem : ∀ {α : Type u_1} {l : List α 0 < length l ↔ ∃ a , a ∈ l
alias length_pos ↔ ne_nil_of_length_pos length_pos_of_ne_nil
#align list.ne_nil_of_length_pos List.ne_nil_of_length_pos
#align list.length_pos_of_ne_nil List.length_pos_of_ne_nil
theorem length_pos_iff_ne_nil { l : List α } : 0 < length l ↔ l ≠ [] :=
⟨ ne_nil_of_length_pos , length_pos_of_ne_nil ⟩
#align list.length_pos_iff_ne_nil List.length_pos_iff_ne_nil
#align list.exists_mem_of_ne_nil List.exists_mem_of_ne_nil : ∀ {α : Type u_1} (l : List α l ≠ [] ∃ x , x ∈ l
#align list.length_eq_one List.length_eq_one
theorem exists_of_length_succ : ∀ {n : ℕ } (l : List α length l = n + 1 ∃ h t , l = h :: t exists_of_length_succ { n } : ∀ l : List α , l . length = n + 1 → ∃ h t , l = h :: t
| [], H => absurd : ∀ {a : Prop } {b : Sort ?u.3320}, a → ¬ a b H . symm : ∀ {α : Sort ?u.3323} {a b : α }, a = b b = a <| succ_ne_zero : ∀ (n : ℕ ), succ n ≠ 0 n
| h :: t , _ => ⟨ h , t , rfl : ∀ {α : Sort ?u.3397} {a : α }, a = a ⟩
#align list.exists_of_length_succ List.exists_of_length_succ : ∀ {α : Type u} {n : ℕ } (l : List α length l = n + 1 ∃ h t , l = h :: t
@[ simp ] lemma length_injective_iff : Injective : {α : Sort ?u.3537} → {β : Sort ?u.3536} → (α → β Prop ( List.length : List α → ℕ ) ↔ Subsingleton α := by
constructor
· intro h ; refine ⟨ fun x y => ?_ ⟩ ; ( suffices [ x ] = [ y ] by simpa using this ) ; apply h ; rfl
· intros hα l1 l2 hl
induction l1 generalizing l2 <;> cases l2
· mpr.nil.nil mpr.nil.cons mpr.cons.nil mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ rfl
· mpr.nil.cons mpr.cons.nil mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ cases hl
· mpr.cons.nil mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ cases hl
· mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ next ih _ _ =>
mpr.cons.cons head✝¹ :: tail✝¹ = head✝ :: tail✝ congr
head✝¹ :: tail✝¹ = head✝ :: tail✝ · exact Subsingleton.elim _ _
head✝¹ :: tail✝¹ = head✝ :: tail✝ · apply ih ; simpa using hl
#align list.length_injective_iff List.length_injective_iff
@[ simp default +1] -- Porting note: this used to be just @[simp]
lemma length_injective [ Subsingleton α ] : Injective : {α : Sort ?u.4557} → {β : Sort ?u.4556} → (α → β Prop ( length : List α → ℕ ) :=
length_injective_iff . mpr : ∀ {a b : Prop }, (a ↔ b b → a inferInstance : ∀ {α : Sort ?u.4588} [i : α ], α
#align list.length_injective List.length_injective
theorem length_eq_two { l : List α } : l . length = 2 ↔ ∃ a b , l = [ a , b ] :=
⟨ fun _ => let [ a , b ] := l ; ⟨ a , b , rfl : ∀ {α : Sort ?u.4812} {a : α }, a = a ⟩, fun ⟨ _ , _, e ⟩ => e ▸ rfl : ∀ {α : Sort ?u.5372} {a : α }, a = a ⟩
#align list.length_eq_two List.length_eq_two
theorem length_eq_three : ∀ {l : List α length l = 3 ↔ ∃ a b c , l = [a , b , c ] length_eq_three { l : List α } : l . length = 3 ↔ ∃ a b c , l = [ a , b , c ] :=
⟨ fun _ => let [ a , b , c ] := l ; ⟨ a , b , c , rfl : ∀ {α : Sort ?u.5774} {a : α }, a = a ⟩, fun ⟨ _ , _ , _, e ⟩ => e ▸ rfl : ∀ {α : Sort ?u.6561} {a : α }, a = a ⟩
#align list.length_eq_three List.length_eq_three : ∀ {α : Type u} {l : List α length l = 3 ↔ ∃ a b c , l = [a , b , c ]
-- Porting note: Lean 3 core library had the name length_le_of_sublist
-- and data.list.basic the command `alias length_le_of_sublist ← sublist.length_le`,
-- but Std has the name Sublist.length_le instead.
alias Sublist.length_le ← length_le_of_sublist
#align list.length_le_of_sublist List.length_le_of_sublist
#align list.sublist.length_le List.Sublist.length_le
/-! ### set-theoretic notation of lists -/
-- ADHOC Porting note: instance from Lean3 core
instance : Singleton α ( List α ) := ⟨ fun x => [ x ]⟩
#align list.has_singleton List.instSingletonList
-- ADHOC Porting note: instance from Lean3 core
instance [ DecidableEq : Sort ?u.6890 → Sort (max1?u.6890) α ] : Insert α ( List α ) := ⟨ List.insert ⟩
-- ADHOC Porting note: instance from Lean3 core
instance [ DecidableEq : Sort ?u.7087 → Sort (max1?u.7087) α ]: IsLawfulSingleton α ( List α ) :=
{ insert_emptyc_eq := fun x =>
show ( if x ∈ ( [] : List α ) then [] else [ x ]) = [ x ] from if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.7295} {t e : α }, (if c then t else e ) = e ( not_mem_nil : ∀ {α : Type ?u.7298} (a : α ), ¬ a ∈ [] _ ) }
#align list.empty_eq List.empty_eq : ∀ {α : Type u_1}, ∅ = []
theorem singleton_eq : ∀ (x : α ), {x } = [x ] singleton_eq ( x : α ) : ({ x } : List α ) = [ x ] :=
rfl : ∀ {α : Sort ?u.7457} {a : α }, a = a
#align list.singleton_eq List.singleton_eq : ∀ {α : Type u} (x : α ), {x } = [x ]
theorem insert_neg [ DecidableEq : Sort ?u.7483 → Sort (max1?u.7483) α ] { x : α } { l : List α } ( h : x ∉ l ) : Insert.insert x l = x :: l :=
if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.7568} {t e : α }, (if c then t else e ) = e h
#align list.insert_neg List.insert_neg
theorem insert_pos [ DecidableEq : Sort ?u.7687 → Sort (max1?u.7687) α ] { x : α } { l : List α } ( h : x ∈ l ) : Insert.insert x l = l :=
if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.7780} {t e : α }, (if c then t else e ) = t h
#align list.insert_pos List.insert_pos
theorem doubleton_eq : ∀ [inst : DecidableEq α x y : α }, x ≠ y {x , y } = [x , y ] doubleton_eq [ DecidableEq : Sort ?u.7897 → Sort (max1?u.7897) α ] { x y : α } ( h : x ≠ y ) : ({ x , y } : List α ) = [ x , y ] := by
rw [ insert_neg , singleton_eq : ∀ {α : Type ?u.8140} (x : α ), {x } = [x ] ]
rwa [ singleton_eq : ∀ {α : Type ?u.8156} (x : α ), {x } = [x ] , mem_singleton : ∀ {α : Type ?u.8163} {a b : α }, a ∈ [b ] ↔ a = b ]
#align list.doubleton_eq List.doubleton_eq : ∀ {α : Type u} [inst : DecidableEq α x y : α }, x ≠ y {x , y } = [x , y ]
/-! ### bounded quantifiers over lists -/
#align list.forall_mem_nil List.forall_mem_nil : ∀ {α : Type u_1} (p : α → Prop x : α ), x ∈ [] p x
#align list.forall_mem_cons List.forall_mem_cons : ∀ {α : Type u_1} {p : α → Prop a : α } {l : List α (∀ (x : α ), x ∈ a :: l p x ) ↔ p a ∧ ∀ (x : α ), x ∈ l p x
theorem forall_mem_of_forall_mem_cons : ∀ {p : α → Prop a : α } {l : List α (∀ (x : α ), x ∈ a :: l p x ) → ∀ (x : α ), x ∈ l p x forall_mem_of_forall_mem_cons { p : α → Prop } { a : α } { l : List α } ( h : ∀ (x : α ), x ∈ a :: l p x h : ∀ x ∈ a :: l , p x ) :
∀ x ∈ l , p x := ( forall_mem_cons : ∀ {α : Type ?u.8304} {p : α → Prop a : α } {l : List α (∀ (x : α ), x ∈ a :: l p x ) ↔ p a ∧ ∀ (x : α ), x ∈ l p x . 1 : ∀ {a b : Prop }, (a ↔ b a → b h : ∀ (x : α ), x ∈ a :: l p x h ). 2 : ∀ {a b : Prop }, a ∧ b b
#align list.forall_mem_of_forall_mem_cons List.forall_mem_of_forall_mem_cons : ∀ {α : Type u} {p : α → Prop a : α } {l : List α (∀ (x : α ), x ∈ a :: l p x ) → ∀ (x : α ), x ∈ l p x
#align list.forall_mem_singleton List.forall_mem_singleton : ∀ {α : Type u_1} {p : α → Prop a : α }, (∀ (x : α ), x ∈ [a ] p x ) ↔ p a
#align list.forall_mem_append List.forall_mem_append : ∀ {α : Type u_1} {p : α → Prop l₁ l₂ : List α (∀ (x : α ), x ∈ l₁ ++ l₂ p x ) ↔ (∀ (x : α ), x ∈ l₁ p x ) ∧ ∀ (x : α ), x ∈ l₂ p x
theorem not_exists_mem_nil : ∀ (p : α → Prop ¬ ∃ x , x ∈ [] ∧ p x not_exists_mem_nil ( p : α → Prop ) : ¬∃ x ∈ @ nil α , p x :=
fun .
#align list.not_exists_mem_nil List.not_exists_mem_nilₓ : ∀ {α : Type u} (p : α → Prop ¬ ∃ x , x ∈ [] ∧ p x -- bExists change
-- Porting note: bExists in Lean3 and And in Lean4
theorem exists_mem_cons_of : ∀ {α : Type u} {p : α → Prop a : α } (l : List α p a ∃ x , x ∈ a :: l ∧ p x exists_mem_cons_of { p : α → Prop } { a : α } ( l : List α ) ( h : p a ) : ∃ x ∈ a :: l , p x :=
⟨ a , mem_cons_self : ∀ {α : Type ?u.8656} (a : α ) (l : List α a ∈ a :: l _ _ , h ⟩
#align list.exists_mem_cons_of List.exists_mem_cons_ofₓ : ∀ {α : Type u} {p : α → Prop a : α } (l : List α p a ∃ x , x ∈ a :: l ∧ p x -- bExists change
-- Porting note: bExists in Lean3 and And in Lean4
theorem exists_mem_cons_of_exists : ∀ {p : α → Prop a : α } {l : List α (∃ x , x ∈ l ∧ p x ) → ∃ x , x ∈ a :: l ∧ p x exists_mem_cons_of_exists { p : α → Prop } { a : α } { l : List α } : (∃ x ∈ l , p x ) →
∃ x ∈ a :: l , p x :=
fun ⟨ x , xl , px ⟩ => ⟨ x , mem_cons_of_mem : ∀ {α : Type ?u.8817} (y : α ) {a : α } {l : List α a ∈ l a ∈ y :: l _ xl , px ⟩
#align list.exists_mem_cons_of_exists List.exists_mem_cons_of_existsₓ : ∀ {α : Type u} {p : α → Prop a : α } {l : List α (∃ x , x ∈ l ∧ p x ) → ∃ x , x ∈ a :: l ∧ p x -- bExists change
-- Porting note: bExists in Lean3 and And in Lean4
theorem or_exists_of_exists_mem_cons : ∀ {p : α → Prop a : α } {l : List α (∃ x , x ∈ a :: l ∧ p x ) → p a ∨ ∃ x , x ∈ l ∧ p x or_exists_of_exists_mem_cons { p : α → Prop } { a : α } { l : List α } : (∃ x ∈ a :: l , p x ) →
p a ∨ ∃ x ∈ l , p x :=
fun ⟨ x , xal , px ⟩ =>
Or.elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c ( eq_or_mem_of_mem_cons : ∀ {α : Type ?u.9066} {a b : α } {l : List α a ∈ b :: l a = b ∨ a ∈ l xal ) ( fun h : x = a => by rw [ ← h ] ; left ; exact px )
fun h : x ∈ l => Or.inr : ∀ {a b : Prop }, b → a ∨ b ⟨ x , h , px ⟩
#align list.or_exists_of_exists_mem_cons List.or_exists_of_exists_mem_consₓ : ∀ {α : Type u} {p : α → Prop a : α } {l : List α (∃ x , x ∈ a :: l ∧ p x ) → p a ∨ ∃ x , x ∈ l ∧ p x -- bExists change
theorem exists_mem_cons_iff : ∀ {α : Type u} (p : α → Prop a : α ) (l : List α (∃ x , x ∈ a :: l ∧ p x ) ↔ p a ∨ ∃ x , x ∈ l ∧ p x exists_mem_cons_iff ( p : α → Prop ) ( a : α ) ( l : List α ) :
(∃ x ∈ a :: l , p x ) ↔ p a ∨ ∃ x ∈ l , p x :=
Iff.intro : ∀ {a b : Prop }, (a → b (b → a a ↔ b or_exists_of_exists_mem_cons : ∀ {α : Type ?u.9345} {p : α → Prop a : α } {l : List α (∃ x , x ∈ a :: l ∧ p x ) → p a ∨ ∃ x , x ∈ l ∧ p x fun h =>
Or.elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c h ( exists_mem_cons_of : ∀ {α : Type ?u.9377} {p : α → Prop a : α } (l : List α p a ∃ x , x ∈ a :: l ∧ p x l ) exists_mem_cons_of_exists : ∀ {α : Type ?u.9386} {p : α → Prop a : α } {l : List α (∃ x , x ∈ l ∧ p x ) → ∃ x , x ∈ a :: l ∧ p x
#align list.exists_mem_cons_iff List.exists_mem_cons_iff : ∀ {α : Type u} (p : α → Prop a : α ) (l : List α (∃ x , x ∈ a :: l ∧ p x ) ↔ p a ∨ ∃ x , x ∈ l ∧ p x
/-! ### list subset -/
instance : IsTrans ( List α ) Subset where
trans := fun _ _ _ => List.Subset.trans : ∀ {α : Type ?u.9468} {l₁ l₂ l₃ : List α l₁ ⊆ l₂ l₂ ⊆ l₃ l₁ ⊆ l₃
#align list.subset_def List.subset_def : ∀ {α : Type u_1} {l₁ l₂ : List α l₁ ⊆ l₂ ↔ ∀ {a : α }, a ∈ l₁ a ∈ l₂
#align list.subset_append_of_subset_left List.subset_append_of_subset_left : ∀ {α : Type u_1} {l l₁ : List α l₂ : List α l ⊆ l₁ l ⊆ l₁ ++ l₂
@[ deprecated subset_append_of_subset_right : ∀ {α : Type u_1} {l l₂ : List α l₁ : List α l ⊆ l₂ l ⊆ l₁ ++ l₂ ]
theorem subset_append_of_subset_right' : ∀ {α : Type u} (l l₁ l₂ : List α l ⊆ l₂ l ⊆ l₁ ++ l₂ subset_append_of_subset_right' ( l l₁ l₂ : List α ) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
subset_append_of_subset_right : ∀ {α : Type ?u.9610} {l l₂ : List α l₁ : List α l ⊆ l₂ l ⊆ l₁ ++ l₂ _
#align list.subset_append_of_subset_right List.subset_append_of_subset_right' : ∀ {α : Type u} (l l₁ l₂ : List α l ⊆ l₂ l ⊆ l₁ ++ l₂
#align list.cons_subset List.cons_subset : ∀ {α : Type u_1} {a : α } {l m : List α a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m
theorem cons_subset_of_subset_of_mem : ∀ {a : α } {l m : List α a ∈ m l ⊆ m a :: l ⊆ m cons_subset_of_subset_of_mem { a : α } { l m : List α }
( ainm : a ∈ m ) ( lsubm : l ⊆ m ) : a :: l ⊆ m :=
cons_subset : ∀ {α : Type ?u.9725} {a : α } {l m : List α a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ ainm , lsubm ⟩
#align list.cons_subset_of_subset_of_mem List.cons_subset_of_subset_of_mem : ∀ {α : Type u} {a : α } {l m : List α a ∈ m l ⊆ m a :: l ⊆ m
theorem append_subset_of_subset_of_subset : ∀ {l₁ l₂ l : List α l₁ ⊆ l l₂ ⊆ l l₁ ++ l₂ ⊆ l append_subset_of_subset_of_subset { l₁ l₂ l : List α } ( l₁subl : l₁ ⊆ l ) ( l₂subl : l₂ ⊆ l ) :
l₁ ++ l₂ ⊆ l :=
fun _ h ↦ ( mem_append : ∀ {α : Type ?u.9875} {a : α } {s t : List α a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c elim (@ l₁subl _ ) (@ l₂subl _ )
#align list.append_subset_of_subset_of_subset List.append_subset_of_subset_of_subset : ∀ {α : Type u} {l₁ l₂ l : List α l₁ ⊆ l l₂ ⊆ l l₁ ++ l₂ ⊆ l
-- Porting note: in Std
#align list.append_subset_iff List.append_subset : ∀ {α : Type u_1} {l₁ l₂ l : List α l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l
alias subset_nil : ∀ {α : Type u_1} {l : List α l ⊆ [] ↔ l = [] ↔ eq_nil_of_subset_nil : ∀ {α : Type u_1} {l : List α l ⊆ [] l = [] _
#align list.eq_nil_of_subset_nil List.eq_nil_of_subset_nil : ∀ {α : Type u_1} {l : List α l ⊆ [] l = []
#align list.eq_nil_iff_forall_not_mem List.eq_nil_iff_forall_not_mem : ∀ {α : Type u_1} {l : List α l = [] ↔ ∀ (a : α ), ¬ a ∈ l
#align list.map_subset List.map_subset : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α f : α → β l₁ ⊆ l₂ map f l₁ ⊆ map f l₂
theorem map_subset_iff { l₁ l₂ : List α } ( f : α → β ) ( h : Injective : {α : Sort ?u.9961} → {β : Sort ?u.9960} → (α → β Prop f ) :
map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂ := by
refine' ⟨ _ , map_subset : ∀ {α : Type ?u.10019} {β : Type ?u.10020} {l₁ l₂ : List α f : α → β l₁ ⊆ l₂ map f l₁ ⊆ map f l₂ f ⟩ ; intro h2 x hx
rcases mem_map : ∀ {α : Type ?u.10046} {β : Type ?u.10047} {b : β } {f : α → β l : List α b ∈ map f l ↔ ∃ a , a ∈ l ∧ f a = b . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( h2 ( mem_map_of_mem : ∀ {α : Type ?u.10068} {β : Type ?u.10069} {a : α } {l : List α f : α → β a ∈ l f a ∈ map f l f hx )) with ⟨x', hx', hxx'⟩ : x' ∈ l₂ ∧ f x' = f x x' ⟨x', hx', hxx'⟩ : x' ∈ l₂ ∧ f x' = f x hx' ⟨x', hx', hxx'⟩ : x' ∈ l₂ ∧ f x' = f x hxx' ⟨x', hx', hxx'⟩ : x' ∈ l₂ ∧ f x' = f x
cases h hxx' ; exact hx'
#align list.map_subset_iff List.map_subset_iff
/-! ### append -/
theorem append_eq_has_append { L₁ L₂ : List α } : List.append L₁ L₂ = L₁ ++ L₂ :=
rfl : ∀ {α : Sort ?u.10339} {a : α }, a = a
#align list.append_eq_has_append List.append_eq_has_append
#align list.singleton_append List.singleton_append : ∀ {α : Type u_1} {x : α } {l : List α [x ] ++ l = x :: l
#align list.append_ne_nil_of_ne_nil_left List.append_ne_nil_of_ne_nil_left : ∀ {α : Type u_1} (s t : List α s ≠ [] s ++ t ≠ []
#align list.append_ne_nil_of_ne_nil_right List.append_ne_nil_of_ne_nil_right : ∀ {α : Type u_1} (s t : List α t ≠ [] s ++ t ≠ []
#align list.append_eq_nil List.append_eq_nil : ∀ {α : Type u_1} {p q : List α p ++ q = [] ↔ p = [] ∧ q = []
-- Porting note: in Std
#align list.nil_eq_append_iff List.nil_eq_append : ∀ {α : Type u_1} {a b : List α [] = a ++ b ↔ a = [] ∧ b = []
theorem append_eq_cons_iff : ∀ {a b c : List α x : α }, a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ a' , a = x :: a' ∧ c = a' ++ b append_eq_cons_iff { a b c : List α } { x : α } :
a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ a' , a = x :: a' ∧ c = a' ++ b := by