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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
⊢ R (l.get a) (l.get b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h✝ : Pairwise R l
a b : α
h : R a b
⊢ Decidable.decide (R a b) = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h : Pairwise R l
⊢ Pairwise (fun a b ↦ Decidable.decide (R a b) = true) l

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ : List α
hab : ¬Lex r (a :: l₁) (b :: l₂)
hba : ¬Lex r (b :: l₂) (a :: l₁)
⊢ a :: l₁ = b :: l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
by

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

Goal state before:
pp: n m i : ℕ
H : i < (range' n m).length
⊢ (range' n m)[i] = n + i

Tactic:
by

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ

Tactic:
by

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
by

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : LT α
l l' : List α
⊢ l.lt l' ↔ Lex (fun x1 x2 ↦ x1 < x2) l l'

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
h : l' < l
hl' : l' ≠ []
⊢ l'.head! ≤ l.head!

Tactic:
by

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

Goal state before:
pp: l : List ℕ
⊢ Pairwise Disjoint l.ranges

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
⊢ a :: l' ≤ a :: l

Tactic:
by

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

Goal state before:
pp: l : List ℕ
⊢ map length l.ranges = l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
head✝ : α
l : List α
⊢ (head✝ :: l) ×ˢ [] = []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
head✝ : α
l : List α
⊢ ((head✝ :: l).sigma fun a ↦ []) = []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
l : List α
⊢ (a :: l = [] ∨ (∃ a_1, a :: l = [a_1]) ∨ ∃ a_1 b l_1, R a_1 b ∧ IsChain R (b :: l_1) ∧ a :: l = a_1 :: b :: l_1) ↔
    l = [] ∨ ∃ b l', R a b ∧ IsChain R (b :: l') ∧ l = b :: l'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b
p : IsChain R l
⊢ IsChain S l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ a ∈ l ∧ b ∈ l.tail ∧ R a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x y : α
⊢ IsChain R [x, y] ↔ R x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ [] ++ [a, b] ++ l = a :: b :: l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
x✝¹ x✝ : α
h : [x✝¹, x✝] <:+: b :: l
⊢ [a] ++ b :: l ++ [] = a :: b :: l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [c])) ∧ IsChain R (c :: l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ foldl (fun x y ↦ y * x) 1 s = foldl (fun x1 x2 ↦ x1 * x2) 1 s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (List.map f s.toList).prod = (map f s).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a : M
⊢ {a}.prod = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : M
⊢ {a, b}.prod = a * b

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = (filter (Eq a) s).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Multiset ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (map f ⟦l⟧).prod (map g ⟦l⟧).prod

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ (map (fun x ↦ 1) m).prod = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
hl₁ : IsChain R l
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a b : α), a ∈ l → b ∈ l → R a b → ∃ ha hb, S (f a ha) (f b hb)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
hl₂ : IsChain S (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
l : List β
hl : ∀ (b : β), b ∈ l → p b
a : β
ha : p a
⊢ ∀ (a_1 : β), a_1 ∈ a :: l → p a_1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
a : α
ha : p a
hl₁ : IsChain R (a :: l)
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a_1 b : α), a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → ∃ ha hb, S (f a_1 ha) (f b hb)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : IsChain S (f a ha :: pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
⊢ IsChain R l₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
inst✝ : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
h : IsChain R l
⊢ IsChain R l.tail

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
h : IsChain R l
hne : l.dropLast ≠ []
⊢ l ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
head✝² head✝¹ head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: head✝ :: tail✝)
hne : (head✝² :: head✝¹ :: head✝ :: tail✝).dropLast ≠ []
⊢ (head✝² :: head✝¹ :: head✝ :: tail✝).tail.dropLast ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
l_ne_nil : l ≠ []
hl : IsChain R l
h : R x (l.head l_ne_nil)
⊢ IsChain R (x :: l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R ([] ++ l) ↔ IsChain R [] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
l : List α
⊢ IsChain R ([a] ++ l) ↔ IsChain R [a] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: tail✝¹ ++ head✝ :: tail✝)
h₁ : head✝² :: head✝¹ :: tail✝¹ ≠ []
h₂ : head✝ :: tail✝ ≠ []
⊢ head✝¹ :: tail✝¹ ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: tail✝¹ ++ head✝ :: tail✝)
h₁ : head✝² :: head✝¹ :: tail✝¹ ≠ []
h₂ : head✝ :: tail✝ ≠ []
⊢ head✝ :: tail✝ ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+: l
⊢ IsChain R l₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
h : ¬IsChain R l
⊢ ∃ n h, ¬R l[n] l[n + 1]

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate (n % l.length) = l.rotate n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ [].rotate n = []

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ [].rotate' n = []

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' 0 = l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' n.succ = (l ++ [a]).rotate' n

Tactic:
by

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

Goal state before:
pp: α : Type u
x✝ : ℕ
⊢ ([].rotate' x✝).length = [].length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x✝ : ∀ (m : M), m ∈ [] → IsUnit m
⊢ IsUnit [].prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h :: t).prod

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≤ [].length
⊢ [].rotate' n = drop n [] ++ take n []

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : 0 ≤ l.length
⊢ l.rotate' 0 = drop 0 l ++ take 0 l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_8
inst✝ : CommMonoid M
L : List M
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
x✝¹ : [].prod = 1
x✝ : ℕ
⊢ ([].rotate x✝).prod = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ 0 < (a :: l).length

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: α : Type u
a : α
l : List α
m : ℕ
⊢ ((a :: l).rotate' 0).rotate' m = (a :: l).rotate' (0 + m)

Tactic:
by

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

Goal state before:
pp: α : Type u
n m : ℕ
⊢ ([].rotate' n).rotate' m = [].rotate' (n + m)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
n m : ℕ
⊢ (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + m + 1)

Tactic:
← rotate'_cons_succ,

Goal state after:
α : Type u
a : α
l : List α
n m : ℕ
⊢ (a :: l).rotate' (n + m).succ = (a :: l).rotate' (n + m + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' l.length = l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Tactic:
rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' (l.length * 0) = l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate' (l.length * (n + 1)) = (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a // p a } → { a // p a } → Prop
⊢ IsChain r (l.attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length = l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n

Tactic:
by

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

Goal state before:
pp: α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ [].rotate n ↔ x✝ ∈ []

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ (a :: l).rotate 0 ↔ x✝ ∈ a :: l

Tactic:
by

Goal state after: