mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
this : Nonempty α
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (b.pred ⋯).castSucc

Tactic:
predAbove_castSucc_of_lt _ _ h,

Goal state after:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ b.castSucc.pred ⋯ = (b.pred ⋯).castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ insert x (Set.range (tail (cons x b))) = insert x (Set.range b)

Tactic:
tail_cons

Goal state after:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ insert x (Set.range b) = insert x (Set.range b)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4

Tactic:
· rw [card_eq_succ]
    grind [card_eq_three]

Goal state after:
case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

Tactic:
ext i

Goal state after:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = (append a (append b c) ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ append x₀ x = cons (x₀ 0) x ∘ Fin.cast ⋯

Tactic:
ext i

Goal state after:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (x₀ 0) x ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x

Tactic:
exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

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

Goal state before:
pp: case h
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α

Tactic:
| _ n ih
   => 

Goal state after:
case h
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ g (i + 1) ⊆ g i

Tactic:
simp_rw [g, Function.iterate_succ, ← image_image]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image f^[i] (image f s) ⊆ image f^[i] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ init (snoc p x) = p

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ init (snoc p x) i = p i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a

Tactic:
ext i

Goal state after:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) i = snoc (f ∘ natAdd m) a i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
⊢ tail (init q) = init (tail q)

Tactic:
ext i

Goal state after:
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
i : Fin n
⊢ tail (init q) i = init (tail q) i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) = snoc (cons a q) b

Tactic:
ext i

Goal state after:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc x (x₀ 0)

Tactic:
ext i

Goal state after:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH

Goal state after:
case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons_cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH

Goal state after:
case mp.cons_cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]

Goal state after:
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m x_1, x = l.get n ∧ x = l.get m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j

Tactic:
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc

n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x : α
p : Fin n → α
⊢ i.insertNth x p ∘ rev = i.rev.insertNth x (p ∘ rev)

Tactic:
by
  funext x
  apply insertNth_rev

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

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite ↑s
⊢ InjOn f s

Tactic:
exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

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

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

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
⊢ l₁ <+ l₂

Tactic:
by
  let ⟨_, h, h'⟩ := hp
  exact Sublist.trans (h.eq_of_pairwise' (hs₂.sublist h') hs₁ ▸ Sublist.refl _) h'

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLE ↔ Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
simp only [sortedLE_iff_monotone_get, monotone_iff_forall_lt, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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 : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)

Tactic:
by
  unfold fold
  rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLT ↔ l.SortedLT

Tactic:
sortedLT_iff_pairwise

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (⇑e) l) ↔ List.Pairwise (fun x1 x2 ↦ x1 < x2) l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGE ↔ l.SortedGE

Tactic:
by
  simp_rw [← sortedLE_reverse, ← map_reverse, sortedLE_listMap]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
by
  change _ > _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  change _ < _ ↔ _
  exact min_lt_iff

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

Goal state before:
pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
← List.cons_head!_tail hl

Goal state after:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
x✝ : α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x✝] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x✝]

Tactic:
| singleton =>

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
  induction l using twoStepInduction <;> simp_all

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

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

Tactic:
tail_cons

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
ha : IsChain (fun x1 x2 ↦ x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ a > b

Tactic:
simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim

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

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case singleton
α : Type u_1
x✝ : α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) [x✝] ↔ ∀ (a : α), a ∈ [x✝].head? → [x✝] = replicate [x✝].length a

Tactic:
| singleton =>

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map (op ∘ unop) l).reverse.reverse.prod

Tactic:
reverse_reverse,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map (op ∘ unop) l).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n).head? = l[n]?

Tactic:
rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

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

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

Tactic:
reverse_reverse,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < n % (x :: l).reverse.length

Tactic:
by simp_all! [k]

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ (m.bind fun a ↦ (if p a then {a} else 0).bind f) = m.bind fun a ↦ if p a then f a else 0

Tactic:
apply Multiset.bind_congr

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ (m.bind fun a ↦ ((Option.map singleton (f a)).getD 0).bind g) = m.bind fun a ↦ (Option.map g (f a)).getD 0

Tactic:
apply Multiset.bind_congr

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ ∀ (a : α), a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ a :: l ~r l ++ [a]

Tactic:
simpa using isRotated_append (l := [a])

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
rw [cons_sigma, IH]
    simp [add_comm, add_left_comm, add_assoc]

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

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩

Tactic:
simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
ext i

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
ext i

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

Tactic:
simpa using filter_product (fun _ : α => true) q

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n !

Tactic:
← factorial_mul_descFactorial h,

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = (n - k)! * n.descFactorial k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
r n : ℕ
b : r ≤ n
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r (n / 2) with a | h
    · apply choose_le_middle_of_le_half_left a
    · rw [← choose_symm b]
      apply choose_le_middle_of_le_half_left
      lia

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
ext i

Goal state after:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i✝ : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
i : ι
⊢ a i = b i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ a ∈ s, (fun b ↦ (a, b)) '' t

Tactic:
rw [iUnion_image_left, image2_mk_eq_prod]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ s.seq t = ⋃ f ∈ s, f '' t

Tactic:
seq_eq_image2,

Goal state after:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ image2 (fun f a ↦ f a) s t = ⋃ f ∈ s, f '' t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = (Prod.mk '' s).seq t

Tactic:
seq_eq_image2,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = image2 (fun f a ↦ f a) (Prod.mk '' s) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = (f '' s).seq t

Tactic:
seq_eq_image2,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = image2 (fun f a ↦ f a) (f '' s) t
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
rw [← SetLike.coe_set_eq]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ x, f x.1 x.2

Tactic:
← Nat.surjective_unpair.iSup_comp

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ x, f (unpair x).1 (unpair x).2
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ (Subgroup.map f H).Normal

Tactic:
by
  rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]
  exact le_normalizer_map _

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
xs : List (FreeMonoid α)
⊢ toList xs.prod = (List.map (⇑toList) xs).flatten

Tactic:
induction xs <;> simp [*]

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

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ max (f i✝) (g i✝)

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)

Tactic:
· apply le_max_left

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f a ⊓ f bᶜ = f a ⊓ (f b)ᶜ

Tactic:
map_compl'

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f a ⊓ (f b)ᶜ = f a ⊓ (f b)ᶜ
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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

Goal state before:
pp: α : Type u
l init tail : List α
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l

Tactic:
induction l generalizing init tail

Goal state after:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [].tails ↔ init ++ tail = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s

Tactic:
have H : s.max' hne ∈ s := max'_mem s hne

Goal state after:
case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive s
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
by
  rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists _ _ _ h)

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r

Tactic:
by
  rw [sublistsLen, ← sublistsLenAux_append]; rfl

Goal state after: