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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ ↑nb) (Int.negOfNat ne)

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ nb) (Int.negOfNat ne)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ ↑nb)⁻¹ (Int.negOfNat ne)

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ ↑nb) num den

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ nb) num den
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ ↑nb)⁻¹ num den

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ nb)⁻¹ num den
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ ↑nb) num den

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ nb) num den
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ ↑nb)⁻¹ num den

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ nb)⁻¹ num den
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f

Tactic:
by
  rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}

Tactic:
← subset_singleton_iff_eq,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ a ∈ s, a = ⊥) ↔ s ⊆ {⊥}
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}

Tactic:
by
  rw [Set.eq_singleton_iff_nonempty_unique_mem]
  rw [sSup_eq_bot] at h_sup
  exact ⟨hne, h_sup⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h

Tactic:
← iSup_sup_eq

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ (iSup f).swap = ⨆ i, (f i).swap

Tactic:
simp_rw [iSup, swap_sSup, ← range_comp, comp_def]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ ⨆ i, f i ≤ (⨆ i, g i) ⊔ ⨆ i, f i ∆ g i ∧ ⨆ i, g i ≤ (⨆ i, f i) ⊔ ⨆ i, f i ∆ g i

Tactic:
← iSup_sup_eq

Goal state after:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ ⨆ i, f i ≤ ⨆ x, g x ⊔ f x ∆ g x ∧ ⨆ i, g i ≤ ⨆ x, f x ⊔ f x ∆ g x
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
have ab := xa.trans (h ⟨xa, xb⟩).2
      exact lt_irrefl _ (h ⟨ab, h'⟩).2

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

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x

Tactic:
rw [le_sub_iff_add_le, zero_add]

Goal state after:
case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ ↑N)⁻¹ ≤ x

Tactic:
zpow_natCast

Goal state after:
case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ ≤ x
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 b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉ < b * a

Tactic:
calc
      ⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 → ∃ a t, a ::ₘ t = s ∧ t.card = n

Tactic:
induction s using Multiset.induction generalizing n with aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (x :: replicate (n + 1) x).dedup = [x]

Tactic:
dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate n.succ x).dedup = [x]
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'

Tactic:
simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x (N ∩ Q + (P - M)) = count x N

Tactic:
rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ min (count x N) (count x Q) + (count x P - count x M) = count x N
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint (t + u) s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
disjoint_add_left

Goal state after:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ _root_.Disjoint (map f s) (map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b

Tactic:
by
  simp [disjoint_iff_ne]

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

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
simp only [disjoint_left, mem_singleton, forall_eq]

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

Goal state before:
pp: α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
⊢ motive { val := s, nodup := nd }

Tactic:
by
    induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t

Tactic:
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a

Tactic:
exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.18
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p ↑x

Tactic:
simpa using (Finset.mem_filter.1 x.2).2

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

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))

Tactic:
conv_rhs => rw [range_add_one]
    rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
    simp

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

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

Tactic:
· rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
⊢ ∃ i, 1 < #(image (fun x ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
by
  simp_rw [one_lt_card_iff, Function.ne_iff] at h ⊢
  obtain ⟨a1, a2, h1, h2, i, hne⟩ := h
  refine ⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩
  rw [filter_ssubset]
  obtain rfl | hne := eq_or_ne (a2 i) ai
  exacts [⟨a1, h1, hne⟩, ⟨a2, h2, hne⟩]

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

Goal state before:
pp: 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 ∘ ⇑finSumFinEquiv) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))

Tactic:
Equiv.coe_fn_mk

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 ∘ Sum.elim (castAdd n) (natAdd m)) ↔
    Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
Module: Mathlib.Data.Finset.Card

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

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

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Tactic:
insert_subset_iff

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
⊢ Fin.find p h = i ↔ p i ∧ ∀ (j : Fin n), j < i → ¬p j

Tactic:
refine ⟨?_, fun ⟨hm, hlt⟩ => have := Fin.find_le_of_pos h hm; ?_⟩

Goal state after:
case refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
⊢ Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j

case refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
x✝ : p i ∧ ∀ (j : Fin n), j < i → ¬p j
hm : p i
hlt : ∀ (j : Fin n), j < i → ¬p j
this : Fin.find p h ≤ i
⊢ Fin.find p h = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
Option.get_dite

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ (if h : ∃ i, p i then some (Fin.find p h) else none).get ⋯ = Fin.find p h

Tactic:
Option.get_dite

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Tactic:
by
  simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, and_left_comm]

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ Injective fun l ↦ l.rotate n

Tactic:
rintro l l' (h : l.rotate n = l'.rotate n)
  have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
  rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
  obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
  rw [← take_append_drop _ l, ht, hd, take_append_drop]

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

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

Tactic:
rw [rotate_cons_succ, ← rotate_rotate, hn]

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → m.bind f = m.bind g

Tactic:
simp +contextual [bind]

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

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

Tactic:
by
  simp [bind, filterMap_join]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ l.length ∧ l.rotate n = l'

Tactic:
refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · simp
  · refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
    refine (Nat.mod_lt _ ?_).le
    simp

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

Goal state before:
pp: case empty
n : ℕ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

Tactic:
simp [Nat.mul_mod, *]

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

Goal state before:
pp: case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n

Tactic:
simp [Nat.mul_mod, *]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup

Tactic:
by
  ext x
  -- Porting note: was `simp_rw [count_dedup, mem_bind, mem_dedup]`
  simp_rw [count_dedup]
  congr 1
  simp

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

Goal state before:
pp: case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]

Tactic:
apply IsRotated.symm

Goal state after:
case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ l.offDiag.Nodup

Tactic:
by
  let := Classical.decEq α
  rw [nodup_iff_count_le_one]
  rintro ⟨x, y⟩
  rw [count_offDiag_eq_mul_sub_ite l x y]
  grind

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹.Finite ↔ s.Finite

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ ((fun x ↦ x⁻¹) '' s).Finite ↔ s.Finite
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Subsemigroup M
h : i ∈ s
⊢ b✝ ∈ i

Tactic:
apply Set.mem_iInter₂.1 hy i h

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ (fun x ↦ x⁻¹) '' s = ∅ ↔ s = ∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a}⁻¹ = {a⁻¹}

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ (fun x ↦ x⁻¹) '' {a} = {a⁻¹}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| (fun x ↦ x⁻¹) '' g '' s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
intro x hz hw
    exact ⟨⟨x, hz⟩, x, hw⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' op '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x⁻¹) '' (fun x ↦ a⁻¹ * x) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ x * a) '' (fun x ↦ x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
← image_inv_eq_inv,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x⁻¹) '' (fun x ↦ x * a⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Submonoid M
h : i ∈ s
⊢ b✝ ∈ i

Tactic:
apply Set.mem_iInter₂.1 hy i h

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✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' s⁻¹ = (⇑f '' s)⁻¹

Tactic:
← image_inv_eq_inv,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (⇑f '' s)⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ ↑n ∈ K

Tactic:
zpow_natCast

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K
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 : x / y ∈ f.ker
⊢ f x = f y

Tactic:
← div_mul_cancel x y,

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 : x / y ∈ f.ker
⊢ f (x / y * y) = f y
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
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f H = f.ker ↔ H = ⊥

Tactic:
by
  rw [comap_eq_ker, f.range_eq_top_of_surjective hf, disjoint_top]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
x✝ : Subgroup G
⊢ zpowers g⁻¹ ≤ x✝ ↔ zpowers g ≤ x✝

Tactic:
by simp only [zpowers_le, inv_mem_iff]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
| a ^ n.succ

Tactic:
rw [← h.eq]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
| (a * a) ^ n.succ
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
· rintro ⟨a, b, ⟨ha, hb⟩, H⟩
    have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
    exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩

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 // f.ker ≤ g.ker }
x✝ : G₁
⊢ ↑((fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g)) x✝ = ↑g x✝

Tactic:
simp only [comp_apply, liftOfRightInverseAux_comp_apply]

Goal state after: