mathlib-initiative/mathlib-tactics huggingface dataset:
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
z a : ℤ
⊢ ⌈↑z⌉ ≤ a ↔ z ≤ a

Tactic:
by rw [ceil_le, Int.cast_le]

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
n : ℕ
a : ℤ
⊢ ↑↑n ≤ ↑a ↔ ↑n ≤ a

Tactic:
cast_le

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : ℤ
⊢ ↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False

Tactic:
by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx

Goal state after:
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
b : H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
rw [← map_zsmul_add, zsmul_one]

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

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

Tactic:
rintro ⟨l₁⟩ ⟨l₂⟩ h₁ h₂; exact Quot.sound (Subperm.antisymm h₁ h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
convert! List.count_erase_of_ne ab (l := l) <;> rw [← coe_count]

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t

Tactic:
by
  constructor
  · rintro ⟨a, ha, rfl, rfl⟩
    rw [← map_cons, Multiset.cons_erase ha]
  · intro h
    have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
    obtain ⟨a, h1, rfl⟩ := mem_map.mp this
    obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
    rw [map_cons, cons_inj_right] at h
    refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
    rw [Multiset.erase_cons_head, h]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
simpa only [dedup, forall_mem_ne, not_not] using this

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'

Tactic:
· refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
    have := count_pos_iff.2 ha
    have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
    rw [h, count_cons_self] at this
    lia

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (map f (x :: xs)).dedup = map f (x :: xs).dedup

Tactic:
rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ t

Tactic:
by
  induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]

Goal state after:
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
⊢ count (f x) (map f s) = count x s

Tactic:
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl

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
⊢ count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
⊢ l₁ <+: l₂

Tactic:
rw [prefix_iff_eq_take] at *

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
m n : ℕ
⊢ take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n

Tactic:
simp [prefix_take_iff, take_prefix]; omega

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ consPiProd f has (prodPiCons f has x✝) = x✝

Tactic:
ext _ hi <;> grind [prodPiCons, consPiProd]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map f.toEmbedding s ↔ f.symm b ∈ s

Tactic:
simp only [mem_map, Equiv.coe_toEmbedding]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
constructor <;> intro h x hx
  · simp only [mem_map_equiv] at hx
    simpa using h hx
  · simp only [mem_map_equiv]
    exact h (by simp [hx])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
⊢ image f s = image g s

Tactic:
by
  ext
  simp_rw [mem_image, ← bex_def]
  exact exists₂_congr fun x hx => by rw [h hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Set α
⊢ ↑s.toFinset = s

Tactic:
by classical exact s.coe_toFinset

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s s₁ s₂ : Finset α
ht : Set.InjOn f ↑s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ image f s₁ ⊆ image f s₂ ↔ s₁ ⊆ s₂

Tactic:
by
  exact_mod_cast ht.image_subset_image_iff (mod_cast h₁) (mod_cast h₂)

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Tactic:
exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
b : β
hb : b ∈ t
⊢ #t ≤ #s.attach

Tactic:
rwa [card_attach]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
by
  rw [← succAbove_ne_last_last ha, succAbove_right_inj]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

Tactic:
split_ifs with hi
  · rw [hi, predAbove_right_zero]
  · rw [predAbove_zero_of_ne_zero hi]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [card_eq_succ]
    grind [card_eq_two]

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = (u ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
Function.comp_apply

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
Function.comp_apply

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = (append a (append b c) ∘ Fin.cast ⋯) i

Tactic:
Function.comp_apply

Goal state after:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l

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

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)))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }

Tactic:
Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ),

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ #{x | p x}ᶜ.toFinset = card α - card { x // p x }

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α

Tactic:
· apply hstep
    intro β _ hlt
    rw [hn] at hlt
    exact ih (Fintype.card β) hlt _ rfl

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
⊢ xₙ = yₙ

Tactic:
by simpa using congr_fun h (last n)

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

Goal state before:
pp: case succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
· split_ifs with h
    · have : i < n := Nat.lt_of_succ_lt_succ h
      simp [addCases, this]
    · have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
      simp [addCases, this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
rcases nonempty_of_card_le h with ⟨f⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
f : α ↪ ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
by
    classical
      refine lt_irrefl (Fintype.card α) ?_
      calc
        Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
        _ = #s.toFinset := s.toFinset_card.symm
        _ < Fintype.card α :=
          Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Goal state after:
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.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:
rwa [Fin.val_fin_lt, f.lt_iff_lt]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (insert (g x) (image g xs)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
fold_insert_idem,

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b f (image g xs)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_and

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_and

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_3
l : List α
R : α → α → Prop
⊢ Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)

Tactic:
by
  refine l.pairwise_iff_getElem.trans ⟨fun h l' hne ⟨l₁, l₂, hl⟩ ↦ ?_, fun h i j hi hj hij ↦ ?_⟩
  · grind [getElem_append_left', getElem_append_right']
  · grind [h _ _ <| List.drop_suffix i _ |>.isInfix.trans <| l.take_prefix (j + 1) |>.isInfix]

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
h : l' < l
hl' : l' ≠ []
⊢ l'.head! ≤ l.head!

Tactic:
replace h : List.Lex (· < ·) l' l := h
  by_cases hl : l = []
  · simp [hl] at h
  · rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h
    exact head_le_of_lt h

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
l : List α
⊢ (map (fun x ↦ count x l) (filter p l.dedup)).sum = countP p l

Tactic:
by
  induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod,
    rotate_eq_drop_append_take_mod, h, zipWith_append, ← drop_zipWith, ←
    take_zipWith, List.length_zipWith, h, min_self]

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
by
  rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
  rcases l'.length.zero_le.eq_or_lt with hl | hl
  · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
  · rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
    · simp [← hn]
    · rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
      exact (Nat.mod_lt _ hl).le

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Tactic:
simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
    hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

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

Goal state before:
pp: n k : ℕ
hn : 0 < n
⊢ n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, n = l + 1 := Nat.exists_eq_add_of_le' hn
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Tactic:
← disjoint_coe,

Goal state after:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint ↑(s ×ˢ t) ↑(s' ×ˢ t') ↔ Disjoint ↑s ↑s' ∨ Disjoint ↑t ↑t'
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: 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))
⊢ Fintype ↑(S ^ n * Set.singleton a)

Tactic:
classical
      apply fintypeMul

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
⊢ IsPretransitive E G

Tactic:
by
  let _ : MulAction E G := MulAction.compHom _ f
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
  obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
  exact ⟨e, rfl⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (insert 1 s) = closure s

Tactic:
rw [insert_eq, closure_union]
  simp [one_mem]

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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → s.prod t ≤ u

Tactic:
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1
    have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2
    simpa using Submonoid.mul_mem _ h1' h2'

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ ↑(pi Set.univ S) = ↑⊥ ↔ ∀ (i : ι), ↑(S i) = ↑⊥

Tactic:
exact Set.univ_pi_eq_singleton_iff

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

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit false x✝¹ + bit true x✝

Tactic:
dsimp [bit]

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit false (x✝¹ + x✝) = bit false x✝¹ + bit false x✝

Tactic:
dsimp [bit]

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit true x✝¹ + bit false x✝

Tactic:
dsimp [bit]

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0

Tactic:
dsimp [bit]

Goal state after:
case false
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0

Tactic:
dsimp [bit]

Goal state after:
case true
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit true x✝¹ ≤ bit true x✝

Tactic:
dsimp [bit]

Goal state after:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ + 1 ≤ 2 * x✝ + 1
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit false x✝¹ ≤ bit false x✝

Tactic:
dsimp [bit]

Goal state after:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ ≤ 2 * x✝
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
b : Bool
h : m < n
⊢ bit false m < 2 * n

Tactic:
dsimp [bit]

Goal state after:
case false
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
m n : ℕ
b : Bool
h : m < n
⊢ bit true m < 2 * n

Tactic:
dsimp [bit]

Goal state after:
case true
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit false n

Tactic:
dsimp [bit]

Goal state after:
case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit true n

Tactic:
dsimp [bit]

Goal state after:
case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1