mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

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
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?
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?
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
⊢ ¬(!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
⊢ ¬(!p head) = true
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
  simp [rtakeWhile, reverse_eq_iff]

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

Goal state before:
pp: case e'_3
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝

pp: case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Tactic:
·

Goal state after:
case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true
Module: Mathlib.Data.List.Intervals

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

Tactic:
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
  lia

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' (n + 1 * (m - n)) ?convert_3

pp: case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + ?convert_3

pp: case convert_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ ℕ

Tactic:
·

Goal state after:
case e'_2.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) ?convert_3
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)

Tactic:
·

Goal state after:
case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)
Module: Mathlib.Data.List.Intervals

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

pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
·

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

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

Tactic:
·

Goal state after:
case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)
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 m) = Ico n l

pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l
Module: Mathlib.Data.List.Intervals

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

pp: case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
·

Goal state after:
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
Module: Mathlib.Data.List.Intervals

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

Tactic:
·

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.zero.zero
α : 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
hn hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ 0 = 0

pp: case cons.zero.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
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1

pp: case cons.succ.zero
α : 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
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

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 : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
·

Goal state after:
case cons.zero.zero
α : 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
hn hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ 0 = 0
Module: Mathlib.Data.List.Intervals

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

pp: case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
·

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

Goal state before:
pp: case cons.zero.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
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1

pp: case cons.succ.zero
α : 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
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

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 : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
·

Goal state after:
case cons.zero.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
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1
Module: Mathlib.Data.List.Intervals

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

Tactic:
·

Goal state after:
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.zero
α : 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
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

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 : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
·

Goal state after:
case cons.succ.zero
α : 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
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0
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 : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

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 : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1
Module: Mathlib.Data.List.Intervals

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

pp: case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ.refine_1
α : 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 | n ≤ tl.length}

pp: case cons.succ.succ.refine_2
α : 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 | n ≤ tl.length}

Tactic:
·

Goal state after:
case cons.succ.succ.refine_1
α : 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 | n ≤ tl.length}
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ.refine_2
α : 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 | n ≤ tl.length}

Tactic:
·

Goal state after:
case cons.succ.succ.refine_2
α : 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 | n ≤ tl.length}
Module: Mathlib.Data.List.Sections

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

pp: case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
Module: Mathlib.Data.List.Sections

Goal state before:
pp: case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f []

pp: case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
·

Goal state after:
case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f []
Module: Mathlib.Data.List.Sections

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

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections
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
⊢ Shortlex r s₁ (s₂ ++ t)

pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

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
⊢ Shortlex r s₁ (s₂ ++ t)
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
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

pp: case inr
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

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
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

pp: case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l

Tactic:
·

Goal state after:
case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l

Tactic:
·

Goal state after:
case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l
Module: Mathlib.Data.List.Shortlex

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

pp: case inr.cons.h_lex
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
·

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
i : ℕ
hi : i < ([].splitLengths l).length
⊢ ([].splitLengths l)[i].length ≤ [][i]

pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α) {i : ℕ} {hi : i < (tail✝.splitLengths l).length}, (tail✝.splitLengths l)[i].length ≤ tail✝[i]
l : List α
i : ℕ
hi : i < ((head✝ :: tail✝).splitLengths l).length
⊢ ((head✝ :: tail✝).splitLengths l)[i].length ≤ (head✝ :: tail✝)[i]

Tactic:
·

Goal state after:
case nil
α : Type u_1
l : List α
i : ℕ
hi : i < ([].splitLengths l).length
⊢ ([].splitLengths l)[i].length ≤ [][i]
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inl
α : 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
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p

pp: case intro.intro.inr
α : 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
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
⊢ Acc (Shortlex r) p

Tactic:
·

Goal state after:
case intro.intro.inl
α : 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
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

pp: case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]

Tactic:
·

Goal state after:
case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]