mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case refine_3
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l < l + a

Tactic:
simpa

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

Goal state before:
pp: case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ x < ↑(↑z / ↑n)

Tactic:
simpa

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

Goal state before:
pp: case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ↑(↑z / ↑n) < y

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
by
  split_ifs with h
  · exact count_eq_one_of_mem d h
  · exact count_eq_zero_of_notMem h

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s ⊂ {a} ↔ s = 0

Tactic:
refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ {b} ⊆ s

Tactic:
rwa [singleton_subset]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
intro a m ih h
    exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

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

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

Tactic:
simpa

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
grind [List.pairwise_iff_getElem]

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

Goal state before:
pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
← Ne,

Goal state after:
case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl ≠ [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s

Tactic:
apply le_cons_self

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

Goal state before:
pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ 0 → q a
⊢ p (foldr f x 0)

Tactic:
simpa

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
⊢ (head✝ :: tail✝).bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
cons_bagInter

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
⊢ (if head✝ ∈ l₂ then head✝ :: tail✝.bagInter (l₂.erase head✝) else tail✝.bagInter l₂) <+ (head✝ :: tail✝) ∩ l₂
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0

Tactic:
List.Nodup.count <| nodup_dedup l,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (if a ∈ l.dedup then 1 else 0) = if a ∈ l then 1 else 0
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.dedup.toFinset = m.toFinset

Tactic:
toFinset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ { val := m.dedup.dedup, nodup := ⋯ } = { val := m.dedup, nodup := ⋯ }
Module: Mathlib.Data.Multiset.Filter

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

Tactic:
← this

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t

Tactic:
by
  rw [← add_eq_union_iff_disjoint]
  refine ⟨fun h0 ↦ ?_, ?_⟩
  · rw [and_iff_right_of_imp]
    · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h
    · rintro rfl
      exact h0
  · rintro ⟨h0, rfl⟩
    exact h0

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

Goal state before:
pp: α : Type u_1
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ (a :: t).inits ↔ s <+: a :: t

Tactic:
simpa

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ (↑a✝).ndinter ↑b✝ = ↑a✝

Tactic:
coe_ndinter,

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ↑(a✝ ∩ b✝) = ↑a✝
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
x✝ : α
⊢ ¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
by
    rw [Classical.not_imp, not_not]

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

Goal state before:
pp: a b : ℕ
⊢ range a + map (fun x ↦ a + x) (range b) = range a ∪ map (fun x ↦ a + x) (range b)

Tactic:
add_eq_union_iff_disjoint

Goal state after:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) (range b))
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ insert a s ∪ t = insert a (s ∪ t)

Tactic:
by
  simp only [insert_eq, union_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P ({x} ∪ s) a

Tactic:
apply union_of _ (symm hi)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P {x} a
Module: Mathlib.Data.Fintype.Defs

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

Tactic:
by rw [← coe_univ, coe_inj]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
by rw [mem_compl, not_not]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t

Tactic:
· simp only [mem_map_equiv]
    exact h (by simp [hx])

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ s = t

Tactic:
by rw [← s.coe_toFinset, h, t.coe_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
a : α
s : Finset α
ha : a ∉ s
⊢ ⟨a, ⋯⟩ ∉ map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach

Tactic:
simpa

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

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f ((image f)^[n] s) = image f^[n + 1] s

Tactic:
iterate_succ',

Goal state after:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f ((image f)^[n] s) = image (f ∘ f^[n]) s
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ ↑j.rev + ↑j = n

Tactic:
rw [Nat.add_comm, j.add_rev_cast]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = j.predAbove i.succ
⊢ i.succ ≤ j.castSucc

Tactic:
simpa

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

Goal state before:
pp: n m : ℕ
h : n = m
⊢ finCongr h = Equiv.cast ⋯

Tactic:
by subst h; simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.InjOn f ↑(range n)

Tactic:
simpa

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
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
⊢ #s.attach ≤ #t

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) = update (cons x p) i.succ y

Tactic:
ext j
  cases j using Fin.cases <;> simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [one_lt_card]
  simp only [exists_and_left]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
by simp [A]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ #univ = #univ + 1

Tactic:
simpa

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

Goal state before:
pp: case refine_2.inl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l

Tactic:
by
  induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

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

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

Tactic:
have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h

Goal state after:
case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
this : ¬i < n
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∀ {i : ℕ}, i < l.length → f i < l'.length

Tactic:
intro i hi

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
i : ℕ
hi : i < l.length
⊢ f i < l'.length
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
p : Finset α → Prop
x✝ : ∃ s, p s
s : Finset α
hs : p s
⊢ p ⋯.toFinset

Tactic:
simpa

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

Goal state before:
pp: case empty
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
hs : (↑∅).Finite
⊢ motive (↑∅) hs

Tactic:
simpa

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 : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ fold op b f s = fold op b g s

Tactic:
fold,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map f s.val) = fold op b g s
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 : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map f s.val) = fold op b g s

Tactic:
fold,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map f s.val) = Multiset.fold op b (Multiset.map g s.val)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x ↦ m (f x)) s = m (fold op b f s)

Tactic:
fold,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = m (fold op b f s)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = m (fold op b f s)

Tactic:
fold,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = m (Multiset.fold op b (Multiset.map f s.val))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ ↑⋯.toFinset ⊆ s

Tactic:
simpa

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ InjOn f ↑⋯.toFinset

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+: l
⊢ IsChain R l₁

Tactic:
by
  rcases h' with ⟨l₂, l₃, rfl⟩
  exact h.left_of_append.right_of_append

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)

Tactic:
rw [← mul_assoc, ← mul_assoc, h]

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

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (take (n % l.length) l)[m - (drop (n % l.length) l).length]? = l[(m + n) % l.length]?

Tactic:
getElem?_take_of_lt,

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (drop (n % l.length) l).length]? = l[(m + n) % l.length]?

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
⊢ rᶜ (l'.head ⋯) (l'.getLast ⋯)

Tactic:
have := wf.asymmetricₙ (by grind) <| h.infix <| l.reverse_reverse ▸ hsub.reverse

Goal state after:
α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
this : ¬r (l'.reverse.getLast ⋯) (l'.reverse.head ⋯)
⊢ rᶜ (l'.head ⋯) (l'.getLast ⋯)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
this : ¬r (l'.reverse.getLast ⋯) (l'.reverse.head ⋯)
⊢ rᶜ (l'.head ⋯) (l'.getLast ⋯)

Tactic:
simpa

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = (map op (x :: xs)).reverse.prod

Tactic:
List.map_cons,

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = (op x :: map op xs).reverse.prod
Module: Mathlib.Data.Multiset.Bind

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

Tactic:
by simp [SProd.sprod, product]

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

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

Tactic:
by simp [SProd.sprod, product]

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

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

Tactic:
by simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).sigma fun a ↦ ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
Multiset.sigma,

Goal state after:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = ↑(l₁.sigma l₂)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this✝ : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
this : 1 + List.count a l < List.count a l * List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l + List.count a l

Tactic:
simpa

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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
by
    rcases lt_or_eq_of_le hk with hk₁ | hk₁
    · have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
        rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
      have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
      rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]
    · rw [hk₁]; simp [Nat.mul_comm, choose, Nat.sub_self]

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

Goal state before:
pp: case succ
n k : ℕ
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
| succ k =>

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

Goal state after: