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

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
]

Goal state after:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true

Tactic:
]

Goal state after:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true
Module: Mathlib.Data.Int.CardIntervalMod

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

Tactic:
]

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ v % r < r + b % r ∧ b % r ≤ v % r
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case false
α : 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
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun x ↦ !p x) tail).head?

pp: case false
α : 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
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
]

Goal state after:
case false
α : 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
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun x ↦ !p x) tail).head?

case false
α : 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
phh' : ¬p head = true
⊢ (!p head) = true
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse
Module: Mathlib.Data.List.TakeWhile

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

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

Tactic:
]

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

case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p l = rdropWhile p l

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse
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).head ?m.26 = (dropWhile (fun x ↦ !p x) l).head ⋯

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

Tactic:
]

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:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

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:
convert! l.find?_eq_head_dropWhile_not ?_
  · simp
  · simpa using h

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ l₁ = l₁

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.DropRight

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n m k : ℕ
⊢ range' (k + n) (m - n) = range' (k + n) (m - n)

Tactic:
]

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
  rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]

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

Goal state before:
pp: n m k : ℕ
h₁ : k ≤ n
⊢ range' (n - k) (m - n) = range' (n - k) (m - n)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case e'_2.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' m ?convert_3

Tactic:
]

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

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

pp: case hnm
n m : ℕ
h : n ≤ m
⊢ n ≤ m

pp: case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1

Tactic:
]

Goal state after:
case hnm
n m : ℕ
h : n ≤ m
⊢ n ≤ m

case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
Module: Mathlib.Data.List.ModifyLast

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

pp: case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

pp: case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
]

Goal state after:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.Intervals

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

Tactic:
]

Goal state after:
n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m
Module: Mathlib.Data.List.ModifyLast

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

Tactic:
]

Goal state after:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ (r.push hd).toListAppend (go f (tl ++ [a]) #[]) = r.toListAppend ((#[].push hd).toListAppend (go f (tl ++ [a]) #[]))
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case pos
n m : ℕ
h : n < m
⊢ IsChain (fun a b ↦ b = a.succ) (n :: Ico (n + 1) m)

Tactic:
]

Goal state after:
case pos
n m : ℕ
h : n < m
⊢ IsChain (fun a b ↦ b = a.succ) (n :: Ico (n + 1) m)
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

pp: case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
]

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) []

Tactic:
]

Goal state after:
case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) []
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]

Tactic:
]

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ l₁ ++ ([hd] ++ modifyLast f (hd' :: tl')) = l₁ ++ ([hd] ++ modifyLast f (hd' :: tl'))

pp: α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

pp: α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
]

Goal state after:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l = Ico n l

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ [] = []

Tactic:
]

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

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
reverse_cons,

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (l ++ [y]).reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst

Tactic:
]

Goal state after:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
]

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
]

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [x])).Palindrome
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hml : m ≤ l
⊢ Ico n m = Ico n m

Tactic:
]

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

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

Tactic:
]

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 = map f l

Tactic:
]

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

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
⊢ Ico n l = Ico n l

Tactic:
]

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

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
]

Goal state after:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k

Tactic:
]

Goal state after:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ Ico l m = Ico l m

Tactic:
]

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

Goal state before:
pp: case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ [] = []

Tactic:
]

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

Goal state before:
pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ = n✝

Tactic:
]

Goal state after:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ = n✝
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hnl : n ≤ l
⊢ Ico l m = Ico l m

Tactic:
]

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

Goal state before:
pp: case inr
n m l : ℕ
hln : l ≤ n
⊢ Ico n m = Ico n m

Tactic:
]

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) = filter (fun x ↦ decide (x < n + 1)) (Ico n m)

Tactic:
]

Goal state after:
n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = filter (fun x ↦ decide (x < n + 1)) (Ico n m)
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < s₂.length + t.length

Tactic:
]

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < s₂.length + t.length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ s₂

Tactic:
]

Goal state after:
case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ s₂
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (tail.length + 1)

Tactic:
]

Goal state after:
case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (tail.length + 1)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < s.length + t₂.length

Tactic:
]

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < s.length + t₂.length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ t₂

Tactic:
]

Goal state after:
case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ t₂
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ l = l

pp: case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum

Tactic:
]

Goal state after:
case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

pp: case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length

Tactic:
]

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.cons
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1

Tactic:
]

Goal state after:
case intro.intro.inr.cons
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (take (i + 1) (sz.splitLengths l))[i].length = sz[i]

Tactic:
]

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (take (i + 1) (sz.splitLengths l))[i].length = sz[i]