mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℤ
⊢ f (x - n • a) = f x - n • b

Tactic:
simpa [sub_eq_add_neg] using map_add_zsmul f x (-n)

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q_inv.num - ⌊q_inv⌋ * ↑q_inv.den < ↑q_inv.den
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num

Tactic:
this.left,

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : ↑q.den - ⌊q_inv⌋ * ↑q_inv.den < ↑q_inv.den
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s

Tactic:
induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.dedup = [] ↔ l = []

Tactic:
by
  induction l with
  | nil => exact Iff.rfl
  | cons a l hl =>
    by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
cons_append

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ x :: (xs.dedup ++ ys) = x :: xs.dedup ++ ys

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∪ ys

Tactic:
cons_append

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ x :: (xs.dedup ++ ys) = x :: (xs.dedup ++ ys)

case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∪ ys
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
rw [tails_eq_inits l]

Goal state after:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
rw [tails_eq_inits l]

Goal state after:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits

Tactic:
induction l using reverseRecOn

Goal state after:
case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).inits = map (map g) [].inits

case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).inits = map (map g) l✝.inits
⊢ (map g (l✝ ++ [a✝¹])).inits = map (map g) (l✝ ++ [a✝¹]).inits
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails

Tactic:
induction l using reverseRecOn

Goal state after:
case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).tails = map (map g) [].tails

case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).tails = map (map g) l✝.tails
⊢ (map g (l✝ ++ [a✝¹])).tails = map (map g) (l✝ ++ [a✝¹]).tails
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
by
  rw [disjoint_singleton_left, mem_singleton]

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

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x ↦ a + x) (range b)

Tactic:
rw [range_add, add_eq_union_iff_disjoint]

Goal state after:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) (range b))
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by_cases h : a ∈ l <;> simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Tactic:
by
  classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_ofPred_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Tactic:
ext
  simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(Finset.filter P l.toFinset) = countP (fun b ↦ decide (P b)) l

Tactic:
rw [l.countP_eq_length_filter, l.filter_toFinset P]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(List.filter (fun b ↦ decide (P b)) l).toFinset = (List.filter (fun b ↦ decide (P b)) l).length
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
hab : a ≤ b
⊢ a ≠ last n

Tactic:
intro rfl

Goal state after:
n : ℕ
b : Fin (n + 1)
hb : b ≠ last n
hab : last n ≤ b
⊢ False
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt]

Goal state after:
case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v + ↑n

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin n
this : NeZero n
⊢ k ≠ 0 → 1 ≤ k

Tactic:
intro hk

Goal state after:
n : ℕ
k : Fin n
this : NeZero n
hk : k ≠ 0
⊢ 1 ≤ k
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
· rw [castPred_castSucc, coeSucc_eq_succ]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∀ k < #t, n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
· rw [h]
    simp [tail]

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ #univ = Fintype.card α

Tactic:
exact Finset.card_univ

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ S₂ ⊆ S₁ᶜ

Tactic:
rwa [Finset.subset_compl_iff_disjoint_left]

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

Goal state before:
pp: case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1

Goal state after:
case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54

Tactic:
by rwa [← e] at this

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j

Tactic:
let finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
    invFun i := @Fin.addCases m n (fun _ => Fin m ⊕ Fin n) Sum.inl Sum.inr i
    left_inv x := by rcases x with y | y <;> simp
    right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp }

Goal state after:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
· simp [h, snoc, castSucc_castLT]

Goal state after:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
this : DecidableEq α := Classical.decEq α
⊢ α ≃ β

Tactic:
letI := Classical.decEq β

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
this✝ : DecidableEq α := Classical.decEq α
this : DecidableEq β := Classical.decEq β
⊢ α ≃ β
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
by_cases h : a ≼ b
    · simp [h]
    · simpa [h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

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

Goal state before:
pp: α : Type u
s : Finset α
⊢ ⋯.toFinset = s

Tactic:
rw [toFinite_toFinset, toFinset_coe]

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (u '' Iio n)

Tactic:
image_eq_range

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (range fun x ↦ u ↑x)
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 α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
by_cases h : a ∈ s
  · rw [← insert_erase h]
    simp [← ha.assoc, hi.idempotent]
  · apply fold_insert h

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 max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
by
  change _ ≥ _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  change _ ≤ _ ↔ _
  exact max_le_iff

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:
rw [insert_eq_cons, prod_cons, prod_singleton]

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
⊢ (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod

Tactic:
mul_assoc,

Goal state after:
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
⊢ (take (n % (a :: l).length) (a :: l)).prod *
      ((drop (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod⁻¹) =
    (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : 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_right hm, getElem?_take_of_lt, length_drop]

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
apply ih b (List.isChain_cons_cons.1 hl).1

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

Goal state before:
pp: case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

Tactic:
rw [length_cyclicPermutations_of_ne_nil]

Goal state after:
case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.choose 2 = n * (n - 1) / 2

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]

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

Goal state before:
pp: case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
calc
    _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b

Tactic:
rw [h, Nat.add_sub_cancel_right] at this

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
x₀✝ : Set α
x✝ : Fin n → Set α
⊢ ⋃ i, Fin.cons x₀✝ x✝ i = Fin.cons x₀✝ x✝ 0 ∪ iUnion (Fin.cons x₀✝ x✝ ∘ Fin.succ)

Tactic:
simp [Function.comp_def]

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

Goal state before:
pp: case snoc
α : Type u_1
n : ℕ
xs✝ : Fin n → Set α
x✝ : Set α
⊢ ⋃ i, Fin.snoc xs✝ x✝ i = iUnion (Fin.snoc xs✝ x✝ ∘ Fin.castSucc) ∪ Fin.snoc xs✝ x✝ (Fin.last n)

Tactic:
simp [Function.comp_def]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

pp: case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
· exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)

Goal state after:
case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a * ↑c * ↑c⁻¹ = b
⊢ a = b

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a * (↑c * ↑c⁻¹) = b
⊢ a = b
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b

Tactic:
rwa [← h] at ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
by
  rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = ⇑m '' (⇑m ⁻¹' s * ⇑m ⁻¹' t)

Tactic:
by
    rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y

Tactic:
mul_assoc,

Goal state after:
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * (b * y)) = f (a * b) * f y
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ g * (n * g * g⁻¹) ∈ S ↔ g * n ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * (n * g⁻¹) ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f (y * y⁻¹ * x) = f y

Tactic:
mul_assoc,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f (y * (y⁻¹ * x)) = f y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Subgroup ↥H → Prop
⊢ (∀ (H' : Subgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.subgroupOf H)

Tactic:
simp [(MapSubtype.orderIso H).forall_congr_left]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑y.1⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * ↑y.2⁻¹ = 1
⊢ x = y

Tactic:
coe_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * ↑y.2⁻¹ = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * ↑y.2⁻¹ = 1
⊢ x = y

Tactic:
coe_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * (↑y.2)⁻¹ = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑(y.1⁻¹ * x.1) = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y

Tactic:
rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker 1 = ⊤

Tactic:
ext
  simp [mem_mker]

Goal state after: