mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |a| na

Tactic:
by
  rw [pa.out]
  constructor
  simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
⊢ f '' mulSupport g ⊆ mulSupport (extend f g 1)

Tactic:
rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

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

Goal state before:
pp: ⊢ descFactorial 0 0 = 0!

Tactic:
by rw [descFactorial_zero, factorial_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : ↑q.num ≠ 0
⊢ ↑(q ^ z) = ↑q ^ z

Tactic:
by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · simp
  · simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]
    congr
    rw [cast_inv_of_ne_zero hq]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋

Tactic:
exact add_sub_sub_cancel _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case above
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := exists_int_gt x
    exact ⟨n, hn.le⟩

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ n - ↑d * (n / ↑d) = n - ↑d * ⌊↑n / ↑d⌋

Tactic:
Rat.floor_intCast_div_natCast

Goal state after:
n : ℤ
d : ℕ
⊢ n - ↑d * (n / ↑d) = n - ↑d * (n / ↑d)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ * (1 - a⁻¹) < 1

Tactic:
← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ < 1 / (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:
Rat.cast_id

Goal state after:
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
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
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ Archimedean K

Tactic:
rw [archimedean_iff_int_le]

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ ∀ (x : K), ∃ n, x ≤ ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ ∃ n, ↑x ≤ ↑y ^ n

Tactic:
simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a : Multiset α), a.Le a

Tactic:
rintro ⟨l⟩

Goal state after:
case mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l) (Quot.mk (⇑(isSetoid α)) l)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s

Tactic:
rintro ⟨l⟩

Goal state after:
case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case neg
α : Type u_1
a b : α
as bs : Multiset α
this✝³ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝² : a ∈ b ::ₘ bs
this✝¹ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this✝ : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs

Tactic:
simpa using this

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

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

Tactic:
exact cons_erase h

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

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → β
s t : Multiset α
⊢ s = t → (∀ (x : α), x ∈ t → f x = g x) → map f s = map g t

Tactic:
by
  rintro rfl h
  induction s using Quot.inductionOn
  exact congr_arg _ (List.map_congr_left h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys = ys

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a✝ : α
s t u : Multiset α
a : α
⊢ count a (s ⊔ t ⊓ u) = count a ((s ⊔ t) ⊓ (s ⊔ u))

Tactic:
by
    simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union,
      Multiset.count_union, Multiset.inf_eq_inter]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
· simp only [h, if_true]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t

Tactic:
by
  refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
  · simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)
  · rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_cons_left]

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
rw [← val_inj]
  rfl

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
⊢ ¬x ∈ map (fun x ↦ a + x) m

Tactic:
hxb

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s \ {a}) t ↔ Disjoint s (t \ {a})

Tactic:
disjoint_sdiff_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
⊢ #(image f s) ≤ #s

Tactic:
by
  simpa only [card_map] using! (s.1.map f).toFinset_card_le

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n

Tactic:
Fin.natCast_eq_last

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ

Tactic:
← succ_zero_eq_one'

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Tactic:
constructor
  · grind
  · rintro ⟨hst, h⟩
    obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)
    grind =>
      have : a ∈ t \ s
      have h : insert a s ⊆ t
      have := eq_of_subset_of_card_le h
      instantiate

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.cons (x 0) (tail x)) = motive x

Tactic:
cons_self_tail

Goal state after:
m n : ℕ
α : Fin (n + 1) → Sort u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x : (i : Fin n.succ) → α i
⊢ motive x = motive x
Module: Mathlib.Data.Fintype.Card

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

Tactic:
Finset.card_univ

Goal state after:
α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ Fintype.card α ≤ Fintype.card α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
rw [append_right]
      simp [castAdd_natAdd]

Goal state after:
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 : ℕ
⊢ image f^[i] (image f s) ⊆ image f^[i] s

Tactic:
hs.finsetImage_subset

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] 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
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j

Tactic:
cases j using lastCases with

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

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')

Goal state after:
case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
⊢ ∃ t, s ⊆ t ∧ #t = n + 1
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
generalize_proofs H₀ H₁ H₂; revert H₂
    generalize hk : pred (succAbove i j) H₁ = k
    rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
    intro; rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (b :: L) = count a L + if b = a then 1 else 0

Tactic:
count_cons

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
cases h.nonempty_fintype
  exact ⟨s.toFinset, fun _ => mem_toFinset⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Finset.univ.card - 1 = Fintype.card α - 1

Tactic:
Finset.card_univ

Goal state after:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card α - 1 = Fintype.card α - 1
Module: Mathlib.Data.List.ProdSigma

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
⊢ ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length

Tactic:
simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
      ← cons_append, isChain_append, and_assoc]
    simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' l.length = l

Tactic:
by
  rw [rotate'_eq_drop_append_take le_rfl]; simp

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

Goal state before:
pp: a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (a :: l).sum

Tactic:
simp [ranges, ← map_flatten, ranges_flatten, range_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
b : β
h : (↑s).PairwiseDisjoint t
⊢ b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Tactic:
by
  simp only [mem_def, disjiUnion_val, Multiset.mem_bind]

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

Goal state before:
pp: case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)

Tactic:
· simp [hn]

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ (map f m).prod = f i ^ count i m

Tactic:
by
  induction m using Quotient.inductionOn
  simp [List.prod_map_eq_pow_single i f hf]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ (map (fun b ↦ count a (f b)) S).sum

Tactic:
hm',

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ (count a (f x) ::ₘ m').sum
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂

Tactic:
by
  obtain ⟨n, rfl⟩ := h
  rw [map_rotate]
  use n

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = count y l

Tactic:
rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : LinearOrder α
⊢ #{x | x.1 < x.2} = (card α).choose 2

Tactic:
simpa using Finset.card_product_filter_lt (s := univ)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)

Tactic:
· exact hf _ _

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

Goal state before:
pp: α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s

Tactic:
by simpa only [Multiset.mem_cons, mem_insert] using! h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup

Tactic:
exact hs.2

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
simp only [pi_cons, nodup_bind]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ (∀ (a_1 : β a), a_1 ∈ t a → (Multiset.map (Pi.cons s a a_1) (s.pi t)).Nodup) ∧
    Pairwise (Disjoint on fun b ↦ Multiset.map (Pi.cons s a b) (s.pi t)) (t a)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
a b : α
⊢ (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : Group α
a b c : α
⊢ b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g f.range = (g.comp f).range

Tactic:
by
  rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f

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

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i : PLift ι
⊢ ∀ (y : PLift ι),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ K i.down) i) ((fun i ↦ K i.down) z) ∧
        (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ K i.down) y) ((fun i ↦ K i.down) z)

Tactic:
simp only [PLift.exists]

Goal state after:
case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i : PLift ι
⊢ ∀ (y : PLift ι), ∃ x, K i.down ≤ K x ∧ K y.down ≤ K x
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ y₁ * y₂ * (y₂⁻¹ * z₁ * y₂ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hx✝ : y * z ∈ closure (↑s ∪ ↑t)
⊢ y⁻¹ * (y * z⁻¹ * y⁻¹) = (y * z)⁻¹

Tactic:
simp [mul_assoc]

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)
  exact h.trans
    ⟨fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨y * z * y⁻¹, hs.conj_mem z hz y, y, hy, by simp [hp]⟩,
    fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨z, hz, z⁻¹ * y * z, hs.conj_mem' y hy z, by simp [mul_assoc, hp]⟩⟩

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

Tactic:
have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext : 1; simp

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
⊢ ∀ (a : Quotient s), Quotient.mk'' <$> decode (encode a.rep) = some a

Tactic:
rintro ⟨l⟩

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Quotient.mk'' <$> decode (encode (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
A : Type u_4
inst✝¹ : AddGroup A
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
⊢ (map H.subtype K).Characteristic

Tactic:
by
  refine characteristic_iff_map_eq.2 fun φ ↦ ?_
  have := congr_arg (map H.subtype) <| characteristic_iff_map_eq.1 hK (MulAut.characteristic H φ)
  simpa [Subgroup.map_map, MulAut.characteristic]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
g : G
hg : g ∈ s
⊢ ↑(MulAut.conj h) (h⁻¹ * g * h⁻¹⁻¹) = g

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ (f.prodMap g).ker = f.ker.prod g.ker

Tactic:
rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
⊢ ∀ (x y : G₂), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
intro x y
    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
    apply hg
    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
    simp only [hf _]

Goal state after: