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

Goal state before:
pp: case pos
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
simp_all

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

Goal state before:
pp: case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : ¬head✝ ∈ l₂
⊢ tail✝.bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
rw [← mem_coe, coe_toList]

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop n xs ~ ys ∩ List.drop n xs
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a ↦ ¬p a) s = s

Tactic:
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t

Tactic:
rw [Multiset.add_comm, add_inter_distrib]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s

Tactic:
sub_cons,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s.erase a - t + a ::ₘ t ∩ s.erase a = s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + t ∩ s = s

Tactic:
sub_cons,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s.erase a - t + t ∩ s = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)

Tactic:
sub_cons,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s.erase a - t) = filter p s - filter p (a ::ₘ t)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp.nil
α : Type u_1
x y : α
bs : List α
h : [] ++ [x] ++ bs = [y]
⊢ x = y

Tactic:
simp_all

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

Goal state before:
pp: case mp.cons
α : Type u_1
x y head✝ : α
tail✝ bs : List α
h : head✝ :: tail✝ ++ [x] ++ bs = [y]
⊢ x = y

Tactic:
simp_all

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

Goal state before:
pp: case mp
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] → head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

Tactic:
rintro ⟨_ | _, _, h⟩

Goal state after:
case mp.nil
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ w✝ : List α
h : [] ++ head✝¹ :: head✝ :: tail✝ ++ w✝ = [x]
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

case mp.cons
α : Type u_1
xs : List α
x head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ w✝ : List α
h : head✝ :: tail✝ ++ head✝² :: head✝¹ :: tail✝¹ ++ w✝ = [x]
⊢ head✝² :: head✝¹ :: tail✝¹ = [] ∨ head✝² :: head✝¹ :: tail✝¹ = [x]
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
by
  rw [← subset_zero]; simp [subset_iff, disjoint_left]

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nontrivial
⊢ ∀ (a_1 : α), a_1 ∈ s ∧ a_1 ≠ a → a_1 ∈ s.erase a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ

Tactic:
refine Nat.succ_le_succ <| ihn ⟨?_⟩

Goal state after:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ Fin n ↪ Fin m
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : ∀ s' ≤ s.val, n < s'.card → ∃ a ∈ s', ¬P a
s' : Finset α
hs' : s' ⊆ s
h : n < #s'
⊢ s'.val ≤ s.val

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ b < a

Tactic:
simp [Fin.lt_def, -val_fin_lt] at *; lia

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : ¬last (n + 1) = 0
⊢ (last (n + 1)).pred h = last n

Tactic:
by simp_rw [← succ_last, pred_succ]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ ↑(i.castPred hi) = ↑(j.castPred hj) ↔ ↑i = ↑j

Tactic:
le_antisymm_iff,

Goal state after:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ ↑(i.castPred hi) ≤ ↑(j.castPred hj) ∧ ↑(j.castPred hj) ≤ ↑(i.castPred hi) ↔ ↑i ≤ ↑j ∧ ↑j ≤ ↑i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b < a.succ.castPred ⋯ ↔ b ≤ a

Tactic:
lt_castPred_succ_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
⊢ Set.range (succAbove 0) = {0}ᶜ

Tactic:
range_succAbove

Goal state after:
n : ℕ
⊢ {0}ᶜ = {0}ᶜ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ tail (cons x p) = p

Tactic:
simp +unfoldPartialApp [tail, cons]

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

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
⊢ cons x₀ x i = cons x₀ x j → i = j

Tactic:
cases i using Fin.cases

Goal state after:
case zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
⊢ cons x₀ x 0 = cons x₀ x j → 0 = j

case succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x j → i✝.succ = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s✝ : Finset α
n : ℕ
a : α
s : Finset α
x✝² : a ∉ s
x✝¹ : #s = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
x✝ : #(cons a s x✝²) = n + 1
⊢ ∃ (h : a ∉ s), cons a s h = cons a s x✝² ∧ #s = n

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩

Goal state after:
case mp
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Tactic:
rcases h with (⟨rfl | h⟩ | h)
    · simpa
    · exact h.cons_duplicate

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append (snoc xs x) ys = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = l'[f (ix + 1)]?

pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)

Tactic:
← hf

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (hd :: tl)[ix + 1]?

α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
⊢ ⋯ ▸ p ((i.succAbove j).pred ⋯) = p j

Tactic:
generalize_proofs H₀ H₁ H₂

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).pred H₁) = p j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
by
  rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊂ ht.toFinset ↔ ↑s ⊂ t

Tactic:
by
  rw [← Finset.coe_ssubset, Finite.coe_toFinset]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = l.get (f ⟨1, ⋯⟩)

Tactic:
← hf

Goal state after:
case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩
Module: Mathlib.Data.List.Sort

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
have : Std.Symm fun x y ↦ x ≠ y → R x y := { symm a b h hne := symm <| h hne.symm }

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
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 ≠ b

Tactic:
exact heq

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
← dropLast_concat_getLast (ne_nil_of_mem ha),

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ++ [l.getLast ⋯]
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)
Module: Mathlib.Data.List.Chain

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

Tactic:
simp_all

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

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

Tactic:
simp_all

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

Goal state before:
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:
simp_all

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)).length * (n / l.length)) = l.rotate' n

Tactic:
length_rotate',

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length + l.length * (n / l.length)) = l.rotate' n
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b
⊢ ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := ih

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
Module: Mathlib.Algebra.Order.Group.Multiset

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

Tactic:
by_cases h : a ∈ s <;> simp [h, hn]

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ (drop (n % l.length) l).length = (drop (n % l'.length) l').length

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
hf : (↑∅).PairwiseDisjoint f
⊢ Disjoint (∅.disjiUnion f hf) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (hf : (↑s✝).PairwiseDisjoint f), Disjoint (s✝.disjiUnion f hf) t ↔ ∀ i ∈ s✝, Disjoint (f i) t
hf : (↑(cons a✝¹ s✝ h✝)).PairwiseDisjoint f
⊢ Disjoint ((cons a✝¹ s✝ h✝).disjiUnion f hf) t ↔ ∀ i ∈ cons a✝¹ s✝ h✝, Disjoint (f i) t

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
β : Type v
t : Multiset β
⊢ map Prod.swap (0 ×ˢ t) = t ×ˢ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
β : Type v
t : Multiset β
a✝¹ : α
s✝ : Multiset α
a✝ : map Prod.swap (s✝ ×ˢ t) = t ×ˢ s✝
⊢ map Prod.swap ((a✝¹ ::ₘ s✝) ×ˢ t) = t ×ˢ (a✝¹ ::ₘ s✝)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
⊢ (map f (0 ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) 0).prod

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
a✝¹ : α
s✝ : Multiset α
a✝ : (map f (s✝ ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s✝).prod
⊢ (map f ((a✝¹ ::ₘ s✝) ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) (a✝¹ ::ₘ s✝)).prod

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : c = a
h✝¹ : c = b
h✝ : a = b
⊢ count b l + count a l + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 1) - (count a l + 1)

Tactic:
simp_all

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (b, b) l.offDiag = count b l * count b l - count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count b l ≤ count b l * count b l
h✝¹ : c = b
h✝ : a = b
⊢ count b l + count b l + (count b l * count b l - count b l) = (count b l + 1) * (count b l + 1) - (count b l + 1)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : c = a
h✝¹ : c = b
h✝ : ¬a = b
⊢ count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : c = a
h✝¹ : ¬c = b
h✝ : a = b
⊢ count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : c = a
h✝¹ : ¬c = b
h✝ : ¬a = b
⊢ count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0

Tactic:
simp_all

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count a l ≤ count a l * count a l
h✝¹ : c = a
h✝ : ¬a = b
⊢ count b l + count a l * count b l = (count a l + 1) * count b l
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : ¬c = a
h✝¹ : c = b
h✝ : a = b
⊢ 0 + count a l + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : ¬c = a
h✝¹ : c = b
h✝ : ¬a = b
⊢ 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0

Tactic:
simp_all

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count b l ≤ count b l * count b l
h✝² : ¬b = a
h✝¹ : c = b
h✝ : ¬a = b
⊢ count a l + count a l * count b l = count a l * (count b l + 1)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h✝² : ¬c = a
h✝¹ : ¬c = b
h✝ : a = b
⊢ 0 + 0 + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 0) - (count a l + 0)

Tactic:
simp_all

Goal state after: