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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
⊢ (orderedInsert r x []).erase x = []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r x tail✝).erase x = tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
⊢ (orderedInsert r x []).erase x = []

case cons
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r x tail✝).erase x = tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
hx : ¬x ∈ []
⊢ (orderedInsert r x []).erase x = []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x head✝ : α
tail✝ : List α
tail_ih✝ : ¬x ∈ tail✝ → (orderedInsert r x tail✝).erase x = tail✝
hx : ¬x ∈ head✝ :: tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
hx : ¬x ∈ []
⊢ (orderedInsert r x []).erase x = []

case cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x head✝ : α
tail✝ : List α
tail_ih✝ : ¬x ∈ tail✝ → (orderedInsert r x tail✝).erase x = tail✝
hx : ¬x ∈ head✝ :: tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
⊢ [] <+ orderedInsert r x []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ <+ orderedInsert r x tail✝
⊢ head✝ :: tail✝ <+ orderedInsert r x (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
⊢ [] <+ orderedInsert r x []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ <+ orderedInsert r x tail✝
⊢ head✝ :: tail✝ <+ orderedInsert r x (head✝ :: tail✝)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
head✝ : α
tail✝ : List α
tail_ih✝ : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ orderedInsert r a (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
head✝ : α
tail✝ : List α
tail_ih✝ : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ orderedInsert r a (head✝ :: tail✝)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case p.zero
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ cons a p 0 = cons a (i.insertNth x p) (i.succ.succAbove 0)

pp: case p.succ
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
i✝ : Fin n
⊢ cons a p i✝.succ = cons a (i.insertNth x p) (i.succ.succAbove i✝.succ)

Tactic:
<;>

Goal state after:
case p.zero
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ cons a p 0 = cons a (i.insertNth x p) (i.succ.succAbove 0)

case p.succ
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
i✝ : Fin n
⊢ cons a p i✝.succ = cons a (i.insertNth x p) (i.succ.succAbove i✝.succ)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

pp: case cons.cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x a then x :: a :: bs else a :: orderedInsert r x bs

Tactic:
<;>

Goal state after:
case cons.cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

case cons.cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x a then x :: a :: bs else a :: orderedInsert r x bs
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
j : Fin n
x : α (p.succAbove j)
⊢ p.removeNth (update f (p.succAbove j) x) j = update (p.removeNth f) j x j

pp: case inr
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
hne : j ≠ i
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j

Tactic:
<;>

Goal state after:
case inl
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
j : Fin n
x : α (p.succAbove j)
⊢ p.removeNth (update f (p.succAbove j) x) j = update (p.removeNth f) j x j

case inr
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
hne : j ≠ i
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case fst
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).1 = f.1

pp: case snd
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
x✝ : Fin n
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).2 x✝ = f.2 x✝

Tactic:
<;>

Goal state after:
case fst
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).1 = f.1

case snd
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
x✝ : Fin n
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).2 x✝ = f.2 x✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
bs : List α
x : α
hb : Pairwise r bs
a : α
as : List α
hs : a :: as <+ bs
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs

Tactic:
cases bs with

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case fst
n : ℕ
α : Fin (n + 1) → Type u_3
x✝ : (i : Fin (n + 1)) → α i
⊢ ((insertNthEquiv α 0).symm x✝).1 = ((consEquiv α).symm x✝).1

pp: case snd
n : ℕ
α : Fin (n + 1) → Type u_3
x✝¹ : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ ((insertNthEquiv α 0).symm x✝¹).2 x✝ = ((consEquiv α).symm x✝¹).2 x✝

Tactic:
<;>

Goal state after:
case fst
n : ℕ
α : Fin (n + 1) → Type u_3
x✝ : (i : Fin (n + 1)) → α i
⊢ ((insertNthEquiv α 0).symm x✝).1 = ((consEquiv α).symm x✝).1

case snd
n : ℕ
α : Fin (n + 1) → Type u_3
x✝¹ : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ ((insertNthEquiv α 0).symm x✝¹).2 x✝ = ((consEquiv α).symm x✝¹).2 x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
⊢ Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j

pp: case refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
x✝ : p i ∧ ∀ (j : Fin n), j < i → ¬p j
hm : p i
hlt : ∀ (j : Fin n), j < i → ¬p j
this : Fin.find p h ≤ i
⊢ Fin.find p h = i

Tactic:
<;>

Goal state after:
case refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
⊢ Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j

case refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
x✝ : p i ∧ ∀ (j : Fin n), j < i → ¬p j
hm : p i
hlt : ∀ (j : Fin n), j < i → ¬p j
this : Fin.find p h ≤ i
⊢ Fin.find p h = i
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
apply fold_insert h

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p 0) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ

Tactic:
h0,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬False) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin n → Bool
h✝ : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h✝)

pp: case neg
n : ℕ
p : Fin n → Bool
h✝ : ¬∃ i, p i = true
⊢ find? p = none

Tactic:
<;>

Goal state after:
case pos
n : ℕ
p : Fin n → Bool
h✝ : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h✝)

case neg
n : ℕ
p : Fin n → Bool
h✝ : ¬∃ i, p i = true
⊢ find? p = none
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l

pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
<;>

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l

case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
H : [].length ≤ l₂.length
h : [] ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] l₂

pp: case cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
l₂ : List α
H : (head✝ :: tail✝).length ≤ l₂.length
h : head✝ :: tail✝ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) l₂

Tactic:
<;>

Goal state after:
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
H : [].length ≤ l₂.length
h : [] ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] l₂

case cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
l₂ : List α
H : (head✝ :: tail✝).length ≤ l₂.length
h : head✝ :: tail✝ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) l₂
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
⊢ IsChain R [] ↔ Forall₂ R [].dropLast [].tail

pp: case singleton
α : Type u_1
R : α → α → Prop
x✝ : α
⊢ IsChain R [x✝] ↔ Forall₂ R [x✝].dropLast [x✝].tail

pp: case cons_cons
α : Type u_1
R : α → α → Prop
x✝ y✝ : α
xs✝ : List α
a✝¹ : IsChain R xs✝ ↔ Forall₂ R xs✝.dropLast xs✝.tail
a✝ : ∀ (y : α), IsChain R (y :: xs✝) ↔ Forall₂ R (y :: xs✝).dropLast (y :: xs✝).tail
⊢ IsChain R (x✝ :: y✝ :: xs✝) ↔ Forall₂ R (x✝ :: y✝ :: xs✝).dropLast (x✝ :: y✝ :: xs✝).tail

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
R : α → α → Prop
⊢ IsChain R [] ↔ Forall₂ R [].dropLast [].tail

case singleton
α : Type u_1
R : α → α → Prop
x✝ : α
⊢ IsChain R [x✝] ↔ Forall₂ R [x✝].dropLast [x✝].tail

case cons_cons
α : Type u_1
R : α → α → Prop
x✝ y✝ : α
xs✝ : List α
a✝¹ : IsChain R xs✝ ↔ Forall₂ R xs✝.dropLast xs✝.tail
a✝ : ∀ (y : α), IsChain R (y :: xs✝) ↔ Forall₂ R (y :: xs✝).dropLast (y :: xs✝).tail
⊢ IsChain R (x✝ :: y✝ :: xs✝) ↔ Forall₂ R (x✝ :: y✝ :: xs✝).dropLast (x✝ :: y✝ :: xs✝).tail
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a] ↔ [] = [] ∨ Forall₂ R (a :: [].dropLast) []

pp: case cons
α : Type u_1
R : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ IsChain R (a :: head✝ :: tail✝) ↔ head✝ :: tail✝ = [] ∨ Forall₂ R (a :: (head✝ :: tail✝).dropLast) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a] ↔ [] = [] ∨ Forall₂ R (a :: [].dropLast) []

case cons
α : Type u_1
R : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ IsChain R (a :: head✝ :: tail✝) ↔ head✝ :: tail✝ = [] ∨ Forall₂ R (a :: (head✝ :: tail✝).dropLast) (head✝ :: tail✝)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
⊢ IsChain R (map f []) ↔ IsChain (fun a b ↦ R (f a) (f b)) []

pp: case singleton
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ : β
⊢ IsChain R (map f [x✝]) ↔ IsChain (fun a b ↦ R (f a) (f b)) [x✝]

pp: case cons_cons
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ y✝ : β
xs✝ : List β
a✝¹ : IsChain R (map f xs✝) ↔ IsChain (fun a b ↦ R (f a) (f b)) xs✝
a✝ : ∀ (y : β), IsChain R (map f (y :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (y :: xs✝)
⊢ IsChain R (map f (x✝ :: y✝ :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (x✝ :: y✝ :: xs✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
⊢ IsChain R (map f []) ↔ IsChain (fun a b ↦ R (f a) (f b)) []

case singleton
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ : β
⊢ IsChain R (map f [x✝]) ↔ IsChain (fun a b ↦ R (f a) (f b)) [x✝]

case cons_cons
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ y✝ : β
xs✝ : List β
a✝¹ : IsChain R (map f xs✝) ↔ IsChain (fun a b ↦ R (f a) (f b)) xs✝
a✝ : ∀ (y : β), IsChain R (map f (y :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (y :: xs✝)
⊢ IsChain R (map f (x✝ :: y✝ :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (x✝ :: y✝ :: xs✝)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
hl : ∀ (a : α), a ∈ [] → p a
⊢ IsChain S (pmap f [] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) []

pp: case singleton
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ : α
hl : ∀ (a : α), a ∈ [x✝] → p a
⊢ IsChain S (pmap f [x✝] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) [x✝]

pp: case cons_cons
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ y✝ : α
xs✝ : List α
a✝¹ :
  ∀ (hl : ∀ (a : α), a ∈ xs✝ → p a), IsChain S (pmap f xs✝ hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) xs✝
a✝ :
  ∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs✝ → p a),
    IsChain S (pmap f (y :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (y :: xs✝)
hl : ∀ (a : α), a ∈ x✝ :: y✝ :: xs✝ → p a
⊢ IsChain S (pmap f (x✝ :: y✝ :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (x✝ :: y✝ :: xs✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
hl : ∀ (a : α), a ∈ [] → p a
⊢ IsChain S (pmap f [] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) []

case singleton
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ : α
hl : ∀ (a : α), a ∈ [x✝] → p a
⊢ IsChain S (pmap f [x✝] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) [x✝]

case cons_cons
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ y✝ : α
xs✝ : List α
a✝¹ :
  ∀ (hl : ∀ (a : α), a ∈ xs✝ → p a), IsChain S (pmap f xs✝ hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) xs✝
a✝ :
  ∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs✝ → p a),
    IsChain S (pmap f (y :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (y :: xs✝)
hl : ∀ (a : α), a ∈ x✝ :: y✝ :: xs✝ → p a
⊢ IsChain S (pmap f (x✝ :: y✝ :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (x✝ :: y✝ :: xs✝)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
⊢ [].rotate' 0 = []

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate' 0 = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ [].rotate' 0 = []

case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate' 0 = head✝ :: tail✝
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
flatten_cons,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ IsChain R (l₁ ++ (l₂ :: L).flatten) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
by
    have hnl : n ≤ l.length := le_of_succ_le_succ h
    have hnl' : n ≤ (l ++ [a]).length := by
      rw [length_append, length_cons, List.length]; exact le_of_succ_le h
    rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
        drop_append_of_le_length hnl, take_append_of_le_length hnl]; simp

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

Goal state before:
pp: α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n

Tactic:
by rw [length_rotate, length_replicate]

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

Goal state before:
pp: case nil
α : Type u_3
R : α → α → Prop
v : α
hl : IsChain R []
hv : ∀ (lne : [] ≠ []), R v ([].head lne)
⊢ IsChain R [v]

pp: case cons
α : Type u_3
R : α → α → Prop
v head✝ : α
tail✝ : List α
hl : IsChain R (head✝ :: tail✝)
hv : ∀ (lne : head✝ :: tail✝ ≠ []), R v ((head✝ :: tail✝).head lne)
⊢ IsChain R (v :: head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_3
R : α → α → Prop
v : α
hl : IsChain R []
hv : ∀ (lne : [] ≠ []), R v ([].head lne)
⊢ IsChain R [v]

case cons
α : Type u_3
R : α → α → Prop
v head✝ : α
tail✝ : List α
hl : IsChain R (head✝ :: tail✝)
hv : ∀ (lne : head✝ :: tail✝ ≠ []), R v ((head✝ :: tail✝).head lne)
⊢ IsChain R (v :: head✝ :: tail✝)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 0 a)

pp: case one
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 1 a)

pp: case more
α : Type u_1
r : α → α → Prop
a : α
h : r a a
n✝ : ℕ
a✝¹ : IsChain r (replicate n✝ a)
a✝ : IsChain r (replicate (n✝ + 1) a)
⊢ IsChain r (replicate (n✝ + 2) a)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 0 a)

case one
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 1 a)

case more
α : Type u_1
r : α → α → Prop
a : α
h : r a a
n✝ : ℕ
a✝¹ : IsChain r (replicate n✝ a)
a✝ : IsChain r (replicate (n✝ + 1) a)
⊢ IsChain r (replicate (n✝ + 2) a)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}

pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}

case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ countP p (0 • s) = 0 * countP p s

pp: case succ
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n✝ : ℕ
a✝ : countP p (n✝ • s) = n✝ * countP p s
⊢ countP p ((n✝ + 1) • s) = (n✝ + 1) * countP p s

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ countP p (0 • s) = 0 * countP p s

case succ
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n✝ : ℕ
a✝ : countP p (n✝ • s) = n✝ * countP p s
⊢ countP p ((n✝ + 1) • s) = (n✝ + 1) * countP p s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (n • s).dedup = count a s.dedup
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a (0 • s) = 0 * count a s

pp: case succ
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n✝ : ℕ
a✝ : count a (n✝ • s) = n✝ * count a s
⊢ count a ((n✝ + 1) • s) = (n✝ + 1) * count a s

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a (0 • s) = 0 * count a s

case succ
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n✝ : ℕ
a✝ : count a (n✝ • s) = n✝ * count a s
⊢ count a ((n✝ + 1) • s) = (n✝ + 1) * count a s
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s t : Multiset M
l₁ l₂ : List M
⊢ (⟦l₁⟧ + ⟦l₂⟧).prod = prod ⟦l₁⟧ * prod ⟦l₂⟧

Tactic:
simp [List.prod_append]

Goal state after: