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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < n.descFactorial 0

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 0 → n.descFactorial 0 < n ^ 0

Tactic:
rintro ⟨⟩

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ 0 < ↑q.den

Tactic:
case =>

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b ≤ (1 - b) * ↑⌊a⌋

Tactic:
← div_le_iff₀' (by linarith),

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b / (1 - b) ≤ ↑⌊a⌋
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✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f (l + n • a))

Tactic:
refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (k + 1) • a))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ
⊢ q ≤ ↑q

Tactic:
rw [Rat.cast_id]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) * (p₃ /ₛ p₁)⁻¹ = p₁ /ₛ p₂

Tactic:
inv_sdiv_eq_sdiv_rev,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) * (p₁ /ₛ p₃) = p₁ /ₛ p₂
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α),
    countP p (b ::ₘ Quot.mk (⇑(isSetoid α)) a) = countP p (Quot.mk (⇑(isSetoid α)) a) + if p b then 1 else 0

Tactic:
by simp [List.countP_cons]

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

Goal state before:
pp: α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Tactic:
case =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
hl : [] ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ [] ∈ range (map f)

Tactic:
exact ⟨[], rfl⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a

Tactic:
exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
· rintro ⟨h, rfl⟩
    exact cons_erase h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
⊢ filter p (s ∪ t) = filter p s ∪ filter p t

Tactic:
simp [(· ∪ ·), union]

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

Goal state before:
pp: α : Type u_1
x : α
xs x✝¹ x✝ : List α
⊢ x✝¹ ++ [x] ++ x✝ = xs ↔ xs = x✝¹ ++ x :: x✝

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a : α
⊢ {a} = univ

Tactic:
by
  ext b; simp [Subsingleton.elim a b]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
hs : s.Nontrivial
hf : Set.InjOn f ↑s
⊢ (image f s).Nontrivial

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := hs
  exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = i.rev.succ.rev

Tactic:
rev_succ,

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = i.rev.rev.castSucc
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a : ℕ
ha : a < n + 2
⊢ 1 = ⟨a, ha⟩ ↔ a = 1

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Type u
c : α
⊢ (ofFn fun x ↦ c) = replicate 0 c

Tactic:
rw [ofFn_zero, replicate_zero]

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

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)

Tactic:
exact σ.map_finRange_perm.map f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ y = x

Tactic:
simp [eq_comm]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
predAbove_last_of_ne_last hi

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ i.castPred hi = i.castPred hi
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ ∃! x, x ∉ image f univ

Tactic:
by
    simpa using existsUnique_notMem_image_of_injOn_of_card_eq_add_one
      (s := .univ) (t := .univ) (Set.injOn_of_injective hf) (by simp) (by simpa)

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

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

Tactic:
simp only [Function.comp_apply]
    rw [snoc_last, natAdd_last, snoc_last]

Goal state after:
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 β
⊢ α ≃ β

Tactic:
by
  letI := Classical.decEq α
  letI := Classical.decEq β
  exact (truncEquivOfCardEq h).out

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

Goal state before:
pp: case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ f ⟨i, hi⟩ < f ⟨j, hj⟩

Tactic:
f.lt_iff_lt

Goal state after:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi⟩ < ⟨j, hj⟩
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ hs.toFinset.Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, Finite.coe_toFinset]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

Tactic:
isChain_cons_cons

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
case =>

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]) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
isChain_cons_cons

Goal state after:
α : Type u_1
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
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])) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
isChain_cons_cons

Goal state after:
α : Type u_1
R : α → α → Prop
a b c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂) ↔
    IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
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:
filter_eq,

Goal state after:
M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = (replicate (count a s) a).prod
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₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (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:
isChain_cons_cons

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
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:
rotate'_length,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (l.length * n) = l
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s

Tactic:
rw [succ_nsmul, mem_add]

Goal state after:
case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s
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
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

Tactic:
congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      lia

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod

Tactic:
← s.coe_toList,

Goal state after:
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * ((↑s.toList).erase a).prod = (↑s.toList).prod
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
a✝ : β
⊢ a✝ ∈ s.disjiUnion (fun a ↦ {f a}) ⋯ ↔ a✝ ∈ map { toFun := f, inj' := hf } s

Tactic:
simp [eq_comm]

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

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun i ↦ fold op (b i) (t i)) (a ::ₘ ha))

Tactic:
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ b a, b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
simp [exists_and_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a

Tactic:
by
  constructor
  · simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp,
      mem_pi]
    rintro g hg hgf a
    rw [← hgf]
    exact hg a
  · simp only [piFinset, mem_map, forall_prop_of_true, mem_univ, mem_pi]
    exact fun hf => ⟨fun a _ => f a, hf, rfl⟩

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

Goal state before:
pp: case inr
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))
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
hx : x ∈ S ^ (n + 1)
⊢ x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
mul_inv_cancel_right

Goal state after:
case inr
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))
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
hx : x ∈ S ^ (n + 1)
⊢ x ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
s : Set M
inst✝ : Mul N
f g : M →ₙ* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
by simp [*]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
simp [eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ (∀ ⦃x : M⦄, x ∈ p₁ → x ∈ p₂ → x ∈ ⊥) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
mem_bot

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

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ g * n ∈ S ↔ g * n ∈ S
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case inl
n : ℕ
h : n % 2 = 0
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
| _ h =>

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case inr
n : ℕ
h : n % 2 = 1
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
| _ h =>

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

Tactic:
case =>

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
ih : (m + n).bodd = (m.bodd ^^ n.bodd)
⊢ (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)

Tactic:
case =>

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
exact (Classical.choose_spec (hf p p)).1

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ g ∈ ⊥ ↔ g = 1

Tactic:
mem_bot

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
⊢ g = 1 ↔ g = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ map f (normalizer ↑H) ≤ normalizer ↑(map f H)

Tactic:
by
  intro x hx
  obtain ⟨y, hy, rfl⟩ := Subgroup.mem_map.mp hx
  have : .comp (MulAut.conj (f y)) f = f.comp (MulAut.conj y) := by ext; simp -- todo: extract lemma
  rw [mem_normalizer_iff_map_conj_eq] at hy ⊢
  rw [map_map, this, ← map_map, hy]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
· exact conjugatesOfSet_subset h hx

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

Tactic:
case =>

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ tl.prod
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * tl.prod

Tactic:
case =>

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]

Tactic:
simp [eq_comm]

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

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case succ.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (some (ofNat α n)) = n + 1

Tactic:
encode_some,

Goal state after:
case succ.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (encode (ofNat α n)).succ = n + 1
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.inl.trans f) s) (map (Embedding.inr.trans f) t)

Tactic:
simpa only [← map_map]
            using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ List.countP (fun x ↦ decide (x ∈ s)) (List.range ↑x) = #({y ∈ range ↑x | y ∈ s})

Tactic:
List.countP_eq_length_filter

Goal state after:
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (List.range ↑x)).length = #({y ∈ range ↑x | y ∈ s})
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
  exact s.min'_lt_max' ha hb hab

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

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

Tactic:
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 = s.sup (WithBot.some ∘ ⇑toDual)

Tactic:
exact congr_fun WithBot.map_id _

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

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

Tactic:
case =>

Goal state after: