mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Torsor.Defs

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

Tactic:
inv_mul_cancel,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = 1 / g
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g⁻¹ * g) • 1 = 1

Tactic:
inv_mul_cancel,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ 1 • 1 = 1
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l[i] = l[j] ↔ i = j

Tactic:
by
  have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
  simpa

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a

Tactic:
by rw [← e]; exact bm

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

Goal state before:
pp: α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f x s)

Tactic:
rw [foldl_swap]
  exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

Goal state after:
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.erase a - t + a ::ₘ t ∩ s.erase a = s

Tactic:
add_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
⊢ a ::ₘ (s.erase a - t + t ∩ s.erase a) = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count, countP_map, ← this]

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ count x (filter (fun a ↦ f x = f a) s) = count x s
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
apply ext_getElem <;> (simp [take_take] <;> grind)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Tactic:
simp only [mem_inter, mem_insert, or_and_right, this, false_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) ↑sᶜ

Tactic:
coe_compl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) (↑s)ᶜ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset = ∅ ↔ s = ∅

Tactic:
by
  let A : Fintype (∅ : Set α) := Fintype.ofIsEmpty
  rw [← toFinset_empty, toFinset_inj]

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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
· rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]

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

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

Tactic:
Int.emod_eq_of_lt

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n = ↑↑u - ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u) - ↑n

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

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

Tactic:
Int.emod_eq_of_lt

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

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u)

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

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

Tactic:
Int.emod_eq_of_lt

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = ↑↑u - ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v < ↑n
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) % ↑n

Tactic:
Int.emod_eq_of_lt

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

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: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) % ↑n = ↑↑u + ↑↑v

Tactic:
Int.emod_eq_of_lt

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) = ↑↑u + ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v)

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) < ↑n
Module: Mathlib.Data.Fin.Basic

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

Tactic:
Int.emod_eq_of_lt

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n = ↑↑u + ↑↑v - ↑n

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v) - ↑n

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n < ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ #s = n

Tactic:
by
  classical
  have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'
  calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n
  apply card_image_of_injective
  intro ⟨i, hi⟩ ⟨j, hj⟩ eq
  exact Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

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

Goal state before:
pp: n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
rw [← val_castLE h]

Goal state after:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑(castLE h ((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩)) = ↑i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂

Tactic:
rw [pred_lt_castPred_iff, le_def]

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

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)

Tactic:
by
  have : b.castLT (lt_of_le_of_lt h ha) ≤ a.castLT ha := by simpa [← val_fin_le] using h
  simp [sub_val_of_le, h, this]

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove i.succ = i.succ.castPred ⋯

Tactic:
predAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)

Goal state after:
n : ℕ
p i : Fin n
h : i < p
⊢ i.succ.castPred ⋯ = i.succ.castPred ⋯
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
cases Fin.lt_or_le j.castSucc i with
  | inl h => rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]
  | inr h =>
    rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
⊢ «repeat» 1 a = a ∘ Fin.cast ⋯

Tactic:
generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  intro i
  simp [modNat, Nat.mod_eq_of_lt i.is_lt]

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

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

Goal state after:
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
z : α (last n)
j : Fin (n + 1)
⊢ update (snoc p x) (last n) z j = snoc p z j

Tactic:
cases j using lastCases <;> simp

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

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

Tactic:
toFinite_toFinset,

Goal state after:
α : Type u
s : Finset α
⊢ (↑s).toFinset = s
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂

Tactic:
← fold_cons_right op

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))

Tactic:
add_cons,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (s.domRestrict f) (f '' s) ⋯)

Tactic:
injective_codRestrict,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (s.domRestrict f)
Module: Mathlib.Data.List.Flatten

Goal state before:
pp: α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.head hl ≠ []
⊢ (l.head hl).head hl' = l.flatten.head ⋯

Tactic:
cases l with grind

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

Goal state before:
pp: case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
j.succAbove_of_castSucc_lt,

Goal state after:
case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g k.castSucc

case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j
Module: Mathlib.Data.List.Chain

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

Tactic:
by
  induction p with grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (head :: head' :: tail)

Tactic:
refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ R a b
Module: Mathlib.Algebra.Order.Group.Multiset

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

Tactic:
simp [h, hn]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

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

Tactic:
simp [h, hn]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
⊢ map f S.join = (map (map f) S).join

Tactic:
by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
S : Multiset (Multiset α)
⊢ S.join.prod = (map prod S).prod

Tactic:
by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
S : Multiset (Multiset α)
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p S.join = (map (filter p) S).join

Tactic:
by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
β : Type v
S : Multiset (Multiset α)
f : α → Option β
⊢ filterMap f S.join = (map (filterMap f) S).join

Tactic:
by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u
L : List α
hL : L ≠ []
⊢ L.getLast hL :: L.dropLast ~r L

Tactic:
induction L using List.reverseRecOn with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
simp_rw [disjoint_disjiUnion_left, disjoint_disjiUnion_right]
        intros i hi j hj
        specialize hfg' hi hj
        grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type v
a : α
s : Multiset α
t : Multiset β
⊢ (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
⊢ s ×ˢ 0 = 0

Tactic:
simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a ↦ (a, b)) s + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type v
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Tactic:
simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ (s ×ˢ t).card = s.card * t.card

Tactic:
simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
refine s.induction ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (∅.biUnion f) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.cyclicPermutations.get n = l) → l ~r l'

Tactic:
get_cyclicPermutations

Goal state after:
case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.rotate ↑n = l) → l ~r l'
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this : Finite α
⊢ Finite (α × β)

Tactic:
have := H.2 ⟨a⟩

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this✝ : Finite α
this : Finite β
⊢ Finite (α × β)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
push_cast
    exact Set.image_swap_prod _ _

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

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

Tactic:
push_cast
    exact Set.image_swap_prod _ _

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
⊢ Disjoint u v

Tactic:
grind [disjoint_left]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s

Tactic:
← Set.image_inv_eq_inv,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' (fun x ↦ x⁻¹) '' s = g '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

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

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

Tactic:
inv_mul_cancel,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ H ⊔ f.ker = ⊤ ⊔ f.ker ↔ H ⊔ f.ker = ⊤

Tactic:
top_sup_eq

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ H ⊔ f.ker = ⊤ ↔ H ⊔ f.ker = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ map f H = f.range ↔ Codisjoint H f.ker

Tactic:
rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
have h := (sup_comm t s) ▸ mem_sup_of_normal_right (s := t) (t := s) (x := x)

Goal state after:
G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd

Tactic:
simp only [shiftRight_eq_div_pow]

Goal state after:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n / 2 ^ 1 / 2 ^ m).bodd = (n / 2 ^ m).bodd
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Normal ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H

Tactic:
by
  simp_rw [← normalizer_eq_top_iff, Subgroup.eq_top_iff', mem_normalizer_iff_map_conj_eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ (normalizer ↑H).subgroupOf K = ⊤

Tactic:
subgroupOf_normalizer_eq h,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ normalizer ↑(H.subgroupOf K) = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

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

Tactic:
exact one_mem _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a * 1⁻¹ ∈ H

Tactic:
← one_mul a

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Tactic:
exact h 1

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a = 1 → IsIdempotentElem a

Tactic:
rintro rfl; exact .one

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
rw [normal_le_normalCore]
    apply iInf_le_of_le 1
    simp [MulAut.one_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, comap (↑(MulAut.conj g)) H

Tactic:
← (Equiv.inv G).iInf_comp,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ x, comap (↑(MulAut.conj ((Equiv.inv G) x))) H