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

Goal state before:
pp: case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

pp: case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
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
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0

Tactic:
rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', zero_mul,
      tsub_nonpos, ← neg_eq_neg_one_mul, neg_lt_sub_iff_lt_add, ← cast_add, cast_lt, cast_le]
    exact ⟨(mod_lt _ hr).trans_le (by simp), not_lt.mp h⟩

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

Goal state before:
pp: case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

pp: case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

pp: case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

pp: case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    (dropWhile p l.reverse).reverse

pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    l ++ [x]

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    (dropWhile p l.reverse).reverse

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    l ++ [x]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    (takeWhile p l.reverse).reverse ++ [x]

pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    []

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    (takeWhile p l.reverse).reverse ++ [x]

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    []
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:
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
  split_ifs with h <;> simp [h]

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

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

pp: case append_singleton
α : Type u_1
p : α → Bool
l l✝ : List α
a✝¹ : α
a✝ : rtakeWhile p l✝ = [] ↔ ∀ (hl : l✝ ≠ []), ¬p (l✝.getLast hl) = true
⊢ rtakeWhile p (l✝ ++ [a✝¹]) = [] ↔ ∀ (hl : l✝ ++ [a✝¹] ≠ []), ¬p ((l✝ ++ [a✝¹]).getLast hl) = true

Tactic:
<;>

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

case append_singleton
α : Type u_1
p : α → Bool
l l✝ : List α
a✝¹ : α
a✝ : rtakeWhile p l✝ = [] ↔ ∀ (hl : l✝ ≠ []), ¬p (l✝.getLast hl) = true
⊢ rtakeWhile p (l✝ ++ [a✝¹]) = [] ↔ ∀ (hl : l✝ ++ [a✝¹] ≠ []), ¬p ((l✝ ++ [a✝¹]).getLast hl) = true
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left' f (head✝ :: tail✝) [] = (map (fun a ↦ f a none) (head✝ :: tail✝), [])

Tactic:
<;>

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

case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left' f (head✝ :: tail✝) [] = (map (fun a ↦ f a none) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right' f [] (head✝ :: tail✝) = (map (f none) (head✝ :: tail✝), [])

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right' f [] [] = (map (f none) [], [])

case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right' f [] (head✝ :: tail✝) = (map (f none) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : β
tail✝ : List β
⊢ zipWith f [] (head✝ :: tail✝) = []

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → β → γ
⊢ zipWith f [] [] = []

case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : β
tail✝ : List β
⊢ zipWith f [] (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) [] = []

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → β → γ
⊢ zipWith f [] [] = []

case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) [] = []
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft' [] = (map (fun a ↦ (a, none)) (head✝ :: tail✝), [])

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipLeft' [] = (map (fun a ↦ (a, none)) [], [])

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft' [] = (map (fun a ↦ (a, none)) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight' (head✝ :: tail✝) = (map (fun b ↦ (none, b)) (head✝ :: tail✝), [])

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipRight' [] = (map (fun b ↦ (none, b)) [], [])

case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight' (head✝ :: tail✝) = (map (fun b ↦ (none, b)) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left f (head✝ :: tail✝) [] = map (fun a ↦ f a none) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left f [] [] = map (fun a ↦ f a none) []

case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left f (head✝ :: tail✝) [] = map (fun a ↦ f a none) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right f [] (head✝ :: tail✝) = map (f none) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right f [] [] = map (f none) []

case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right f [] (head✝ :: tail✝) = map (f none) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft [] = map (fun a ↦ (a, none)) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipLeft [] = map (fun a ↦ (a, none)) []

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft [] = map (fun a ↦ (a, none)) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

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

Tactic:
zipLeft'

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.Palindrome

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ [].reverse = []

pp: case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

pp: case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
⊢ [].reverse = []

case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])
Module: Mathlib.Data.List.Map2

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

Tactic:
cases bs with

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

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

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

Tactic:
<;>

Goal state after:
case cons.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
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ 0 = m

case cons.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
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ n✝ + 1 = m
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = map (fun b ↦ (none, b)) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipRight [] = map (fun b ↦ (none, b)) []

case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = map (fun b ↦ (none, b)) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

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

pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
bs : List β
⊢ (head✝ :: tail✝).zipRight bs = ((head✝ :: tail✝).zipRight' bs).fst

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = ([].zipRight' bs).fst

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
bs : List β
⊢ (head✝ :: tail✝).zipRight bs = ((head✝ :: tail✝).zipRight' bs).fst
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case nil.nil
α : Type u
β : Type v
⊢ [].zipRight [] = ([].zipRight' []).fst

pp: case nil.cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = ([].zipRight' (head✝ :: tail✝)).fst

pp: case cons.nil
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
⊢ (head✝ :: tail✝).zipRight [] = ((head✝ :: tail✝).zipRight' []).fst

pp: case cons.cons
α : Type u
β : Type v
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), tail✝¹.zipRight bs = (tail✝¹.zipRight' bs).fst
head✝ : β
tail✝ : List β
⊢ (head✝¹ :: tail✝¹).zipRight (head✝ :: tail✝) = ((head✝¹ :: tail✝¹).zipRight' (head✝ :: tail✝)).fst

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u
β : Type v
⊢ [].zipRight [] = ([].zipRight' []).fst

case nil.cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = ([].zipRight' (head✝ :: tail✝)).fst

case cons.nil
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
⊢ (head✝ :: tail✝).zipRight [] = ((head✝ :: tail✝).zipRight' []).fst

case cons.cons
α : Type u
β : Type v
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), tail✝¹.zipRight bs = (tail✝¹.zipRight' bs).fst
head✝ : β
tail✝ : List β
⊢ (head✝¹ :: tail✝¹).zipRight (head✝ :: tail✝) = ((head✝¹ :: tail✝¹).zipRight' (head✝ :: tail✝)).fst
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ ([].splitLengths l).length = [].length

pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (tail✝.splitLengths l).length = tail✝.length
l : List α
⊢ ((head✝ :: tail✝).splitLengths l).length = (head✝ :: tail✝).length

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
⊢ ([].splitLengths l).length = [].length

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (tail✝.splitLengths l).length = tail✝.length
l : List α
⊢ ((head✝ :: tail✝).splitLengths l).length = (head✝ :: tail✝).length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = true
⊢ splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []

pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
<;>

Goal state after:
case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = true
⊢ splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []

case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l

pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l

Tactic:
<;>

Goal state after:
case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l

case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
x✝ : splitBy r l = []
⊢ l = []

pp: case refine_2
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ l = [] → splitBy r l = []

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
x✝ : splitBy r l = []
⊢ l = []

case refine_2
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ l = [] → splitBy r l = []
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), b ∈ [].head? → r b a = true

pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun y x ↦ r x y = true) []

Tactic:
<;>

Goal state after:
α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), b ∈ [].head? → r b a = true

α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun y x ↦ r x y = true) []
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 → a = 0

pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ a = 0 → mulLeftLinearMap n R a = 0

Tactic:
<;>

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 → a = 0

case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ a = 0 → mulLeftLinearMap n R a = 0
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ([].reverse ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]

pp: case cons.h
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) ([].reverse ++ a :: l)

pp: case cons.ha
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ∀ (x : α), x ∈ [].head? → r ((a :: l).getLast ⋯) x = false

Tactic:
<;>

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ([].reverse ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]

case cons.h
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) ([].reverse ++ a :: l)

case cons.ha
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ∀ (x : α), x ∈ [].head? → r ((a :: l).getLast ⋯) x = false