mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
⊢ ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l).length ≤ l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p l[0] = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
⊢ foldl (flip cons) [] l = l.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v b (a :: l) = v (foldl v b l) a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ r ≤ r + v % r

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ foldr f b (a :: l) = foldr f (f a b) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
a b : α
⊢ f (foldl f a l) b = f a (foldr f b l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a l = foldr f a l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
inst✝ : LeftCommutative f
⊢ foldl (flip f) b l = foldr f b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst✝ : RightCommutative v
⊢ foldr (flip v) b l = foldl v b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Indexes

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i ↦ f (↑i) (l.get i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Indexes

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l
⊢ p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ r ≤ r + b % r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
⊢ count (fun x ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p q : α → Bool
l : List α
⊢ takeWhile p (takeWhile q l) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
⊢ ¬p head = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ [].rdrop n = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.rdrop 0 = l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rdrop n = (drop n l.reverse).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rdrop (n + 1) = l.rdrop n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ [].rtake n = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.rtake 0 = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

Tactic:
exact drop_length

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rdropWhile p [] = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((rdropWhile p l).getLast hl) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? p l = (dropWhile (fun x ↦ !p x) l).head?

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? (fun x ↦ !p x) l = (dropWhile p l).head?

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p (dropWhile p l) = dropWhile p l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ dropWhile (fun x ↦ !p x) l ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l.reverse = (dropWhile p l).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rtakeWhile p [] = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ find? p l = some ((dropWhile (fun x ↦ !p x) l).head ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ dropWhile p l ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l <:+ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l.reverse = (takeWhile p l).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l ++ rtakeWhile p l = l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ find? (fun x ↦ !p x) l = some ((dropWhile p l).head ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n : ℕ
⊢ Ico 0 n = range n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).length = m - n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ Pairwise (fun x1 x2 ↦ x1 < x2) (Ico n m)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ Ico n m = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m k : ℕ
⊢ map (fun x ↦ k + x) (Ico n m) = Ico (n + k) (m + k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x ↦ x - k) (Ico n m) = Ico (n - k) (m - k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : Ico n m = []
⊢ m - n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left' f as [] = (map (fun a ↦ f a none) as, [])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft' [] = (map (fun a ↦ (a, none)) as, [])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n : ℕ
⊢ Ico n (n + 1) = [n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight' bs = (map (fun b ↦ (none, b)) bs, [])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left f as [] = map (fun a ↦ f a none) as

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : List β
⊢ map₂Left f [] x✝ = (map₂Left' f [] x✝).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
⊢ map₂Left f (a :: as) (b :: bs) = (map₂Left' f (a :: as) (b :: bs)).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : [].length ≤ [].length
⊢ map₂Left f [] [] = zipWith (fun a b ↦ f a (some b)) [] []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : β
tail✝ : List β
x✝ : [].length ≤ (head✝ :: tail✝).length
⊢ map₂Left f [] (head✝ :: tail✝) = zipWith (fun a b ↦ f a (some b)) [] (head✝ :: tail✝)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
h : (a :: as).length ≤ [].length
⊢ map₂Left f (a :: as) [] = zipWith (fun a b ↦ f a (some b)) (a :: as) []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : (a :: as).length ≤ (b :: bs).length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b ↦ f a (some b)) (a :: as) (b :: bs)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ ¬m ∈ Ico n m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: α : Type u_1
f : α → α
a : α
l : List α
⊢ modifyLast f (l ++ [a]) = l ++ [f a]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
⊢ map₂Right f as bs = (map₂Right' f as bs).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
⊢ map₂Right f as bs = zipWith (fun a b ↦ f (some a) b) as bs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n l) ++ filter (fun x ↦ decide (x < l)) (Ico l m) = Ico n l

Tactic:
filter_lt_of_top_le (le_refl l),

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l ++ filter (fun x ↦ decide (x < l)) (Ico l m) = Ico n l
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft [] = map (fun a ↦ (a, none)) as

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: α : Type u_1
f : α → α
l₁ l₂ : List α
x✝ : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipLeft bs = (as.zipLeft' bs).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse = l → l.Palindrome

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
⊢ (l ++ l.reverse).Palindrome

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = map (fun b ↦ (none, b)) bs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ (map f l).reverse = map f l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipRight bs = (as.zipRight' bs).fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x < n + 1)) (Ico n m) = [n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = decide (x✝¹ < n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = [n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k ↦ l.insertIdx k x) {n | n ≤ l.length}

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : 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)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : 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)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun a s ↦
        let r := f a s.1;
        (r.1, r.2 :: s.2))
      (s, []) (a :: as)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun ab s ↦
        let r := f ab.1 ab.2 s.1;
        (r.1, r.2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sections

Goal state before:
pp: α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Shortlex r s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
h : s.length = t.length
⊢ Shortlex r s t ↔ Lex r s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s t : List α
⊢ Shortlex r (a :: s) (a :: t) ↔ Shortlex r s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : List α
⊢ ¬Shortlex r s []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ Shortlex r [a] [b] ↔ r a b

Tactic:
by

Goal state after: