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

Goal state before:
pp: m k : ℕ+
⊢ ↑k * m.div k + ↑(m.mod k) = ↑m

Tactic:
exact div_add_mod _ _

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

Goal state before:
pp: case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m

Tactic:
rcases h with ⟨a, h⟩
    obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
      rintro rfl
      simp only [mul_zero, ne_zero] at h
    use ⟨n.succ, n.succ_pos⟩
    rw [← coe_inj, h, mul_coe, mk_coe]

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a * ↑n⌋ / n = ⌊a⌋

Tactic:
refine eq_of_forall_le_iff fun m ↦ ?_

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
⊢ m ≤ ⌊a * ↑n⌋ / n ↔ m ≤ ⌊a⌋
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
⊢ a ^ 2 + ↑2 * a ^ 1 * b + b ^ 2 = (a + b) ^ 2

Tactic:
simp [sq, add_mul, mul_add, two_mul, Hcomm.eq, add_assoc]

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
a : R
ha : -1 < a
⊢ 0 ≤ ⌈a⌉

Tactic:
rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]

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

Goal state before:
pp: q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
suffices (q.num : ℚ) < (q - fract q + 1) * q.den by
    have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]

Goal state after:
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {p} /ₛ {p} = {1}

Tactic:
rw [Set.singleton_sdiv_singleton, sdiv_self]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk (⇑(isSetoid α)) l = 0

Tactic:
rw [eq_nil_iff_forall_not_mem.mpr H]; rfl

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

Goal state before:
pp: α : 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
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs

Tactic:
simp [eq, hcs]

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:
refine ⟨?_, by aesop⟩

Goal state after:
α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 → ∃ a t, a ::ₘ t = s ∧ t.card = n
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x

Tactic:
have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))

Goal state after:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
rwa [card_erase_of_mem h, if_pos]

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

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

Tactic:
exact le_add_right _ _

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b

Tactic:
refine ⟨a, ha, ?_⟩

Goal state after:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (↑l).card b₂

Tactic:
map_const

Goal state after:
α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate (↑l).card b₂
⊢ b₁ ∈ replicate (↑l).card b₂
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x

Tactic:
ext y

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ y = z ∧ _root_.Disjoint x y

Tactic:
simpa only [and_comm] using add_eq_union_left_of_le h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a (s ∪ t) ≤ 1

Tactic:
count_union

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ max (count a s) (count a t) ≤ 1
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (map reverse (a :: l).reverse.inits).reverse

Tactic:
by simp [tails_eq_inits l]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Tactic:
exact And.intro

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x ∪ s) {t | Disjoint s t}

Tactic:
grind [Set.InjOn, union_sdiff_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ ∩ s = insert a ∅

Tactic:
insert_inter_of_mem H,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a (∅ ∩ s) = insert a ∅
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)

Tactic:
rintro x ⟨rfl, h⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Tactic:
rw [disjoint_erase_comm, erase_insert ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ insert x {x}ᶜ = univ

Tactic:
by
  rw [← compl_erase, erase_singleton, compl_empty]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = g ⟨i, hi⟩

Tactic:
Finset.union_symm_right h hi hi'

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g (Sum.inr ⟨i, hi⟩) = g ⟨i, hi⟩
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) = image (f ∘ Subtype.val) t

Tactic:
ext y

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ (e.finsetCongr.trans e'.finsetCongr) x✝ ↔ a✝ ∈ (e.trans e').finsetCongr x✝

Tactic:
simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
⊢ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) = {i | m ≤ ↑i + n}

Tactic:
ext y

Goal state after:
n m : ℕ
hmn : n ≤ m
y : Fin m
⊢ y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) ↔ y ∈ {i | m ≤ ↑i + n}
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
a b : Fin n
ha : ↑a < m
hab : b ≤ a
⊢ ↑(a - b) < m

Tactic:
rw [Fin.sub_val_of_le hab]
  exact sub_lt_of_lt ha

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
have H₂ : i / n < m := i.divNat.is_lt

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ↑i.rev.modNat = ↑i.modNat.rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
  have : s.image f ⊆ t := hf.finsetImage_subset
  exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

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

Goal state before:
pp: case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

pp: case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
· exact (ha rfl).elim

Goal state after:
case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n.succ)) =
    f 0 :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨m * ↑i + ↑j, ⋯⟩).flatten

Tactic:
simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i

Tactic:
predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h),

Goal state after:
n : ℕ
p i : Fin n
h : i ≤ p
⊢ i.castSucc.castPred ⋯ = i
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ Nonempty (Fintype α)

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
  exact ⟨.ofEquiv _ e.symm⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}

Tactic:
by rw [card_le_one.1 H y hy x hx, mem_singleton]

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

Goal state before:
pp: n : ℕ
p i : Fin n
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
by
  obtain h | h := p.le_or_gt i
  · rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]
  · rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
⊢ tail (update q i.succ y) = update (tail q) i y

Tactic:
ext j
  by_cases h : j = i
  · rw [h]
    simp [tail]
  · simp [tail, (Fin.succ_injective n).ne h, h]

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

Goal state before:
pp: α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction H s = H s fun t x ↦ strongInduction H t

Tactic:
by
  rw [strongInduction]

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

Goal state before:
pp: case last
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
exact .inl hi

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

Goal state before:
pp: case inl
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ i, P i

Tactic:
exact ⟨_, ‹_›⟩

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

Goal state before:
pp: case inr
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ i, P i

Tactic:
exact ⟨_, ‹_›⟩

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

Goal state before:
pp: case x
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
exact .inl hi

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

Goal state before:
pp: case inl
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ i, P i

Tactic:
exact ⟨_, ‹_›⟩

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

Goal state before:
pp: case inr
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ i, P i

Tactic:
exact ⟨_, ‹_›⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
insertionSort_cons

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (f x :: map f xs)

Tactic:
insertionSort_cons

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
⊢ range (p.insertNth x f) = Set.insert x (range f)

Tactic:
ext y

Goal state after:
n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
y : α
⊢ y ∈ range (p.insertNth x f) ↔ y ∈ Set.insert x (range f)
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
simp only [h, dedup_cons_of_mem, IH, fold_cons_left]

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
by
  have := Classical.decEq α
  rw [← toFinset_card, toFinset_ofPred, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x ↦ c) s = if s = ∅ then b else op b c

Tactic:
induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
inter_val,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
decide_eq_true_eq

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

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
  rw [contractNth, if_neg this, if_pos h]

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

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

Tactic:
exact And.intro

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
rcases trichotomous_of r a b with (ab | rfl | ab)

Goal state after:
case inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)

Tactic:
isChain_split,

Goal state after:
α : Type u_1
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ [b]) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun a b ↦ R b a) (b :: l)

Tactic:
isChain_split,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun a b ↦ R b a) (b :: l)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩; grind

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

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

Tactic:
rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne : ¬i = j
⊢ (∃ i_1 h, l[i_1] = l[i]) ∧ (∃ i h, l[i] = l[j]) ∧ ¬l[i] = l[j]

Tactic:
exact ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩

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

Goal state before:
pp: ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
⊢ {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
ext
  simpa using fun _ _ a ↦ (Ne.le_iff_lt a).symm

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a

Tactic:
simp only [this, pi_zero, mem_singleton, true_iff]

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ ∀ (a : α) (h : a ∈ 0), Pi.empty β a h ∈ t a