mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ x ∈ l → count x l = 1

Tactic:
rw [← count_pos_iff]; grind

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
⊢ (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t) →
    ∀ {m1 : Multiset α},
      (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ t → r a_2 b) → m1.card = (a ::ₘ t).card → Rel r m1 (a ::ₘ t)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
⊢ ∀ {m1 : Multiset α}, (∀ (a_1 b : α), a_1 ∈ m1 → b ∈ a ::ₘ t → r a_1 b) → m1.card = (a ::ₘ t).card → Rel r m1 (a ::ₘ t)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_not_mem h', nodup_cons]

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ l.Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
⊢ f y ::ₘ map f (s.erase x) = f y ::ₘ (map f s).erase (f x)

Tactic:
ih

Goal state after:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
⊢ f y ::ₘ (map f s).erase (f x) = f y ::ₘ (map f s).erase (f x)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : 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
h : x ∈ xs
⊢ (map f xs).dedup = map f xs.dedup

Tactic:
ih

Goal state after:
case pos
α : 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
h : x ∈ xs
⊢ map f xs.dedup = map f xs.dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ []
⊢ (a :: l₁).bagInter [] = a :: l₁.bagInter ([].erase a)

Tactic:
grind [List.bagInter]

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

Goal state before:
pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = a :: l₁.bagInter ((head✝ :: tail✝).erase a)

Tactic:
grind [List.bagInter]

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

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ (a :: l₁).bagInter [] = l₁.bagInter []

Tactic:
grind [List.bagInter]

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

Goal state before:
pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = l₁.bagInter (head✝ :: tail✝)

Tactic:
grind [List.bagInter]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
| cons a s IH =>

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

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

Tactic:
by
  rw [inter_comm]
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  by_cases h : a ∈ s
  · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
  · rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]

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

Goal state before:
pp: case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

Tactic:
simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 ↦ decide (b_1 = b)) l) = replicate (List.count b l) b

Tactic:
rw [List.filter_eq, coe_replicate]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
by
      rw [ndinsert_of_notMem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_notMem h,
          cons_erase m]
      exact l

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ s.ndunion t = s.dedup + t

Tactic:
by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup

Tactic:
rw [← ndinter_eq_inter d]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup
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✝
⊢ ndinter (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) a✝

Tactic:
quot_mk_to_coe'',

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ (↑a✝).ndinter (Quot.mk (⇑(isSetoid α)) b✝) = ↑a✝
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 (Quot.mk (⇑(isSetoid α)) b✝) = ↑a✝

Tactic:
quot_mk_to_coe'',

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

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

Tactic:
| cons a s IH =>

Goal state after:
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:
simp only [insert_eq, union_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False

Tactic:
exact H h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
rw [inter_comm, singleton_inter_of_mem h]

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

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt] <;> lia

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ i ≠ 0 → ↑(i - 1) = ↑i - 1

Tactic:
have := i.neZero

Goal state after:
n : ℕ
i : Fin n
this : NeZero n
⊢ i ≠ 0 → ↑(i - 1) = ↑i - 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = j.castSucc

Tactic:
rw [← h, castSucc_castPred]

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

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

Tactic:
Fin.modNat,

Goal state after:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ (ofFn fun i ↦ ofFn fun j ↦ a ⟨(↑i * m + ↑j) % m, ⋯⟩).flatten = (ofFn fun x ↦ ofFn a).flatten
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ image i.succAbove univ = {i}ᶜ

Tactic:
by
  ext m
  simp

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
  refine ⟨f, hf, fun m n hmn => ?_⟩
  grind +splitIndPred

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

Goal state before:
pp: n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin (n + 1)
h : snoc x x₀ i = snoc x x₀ j
⊢ i = j

Tactic:
induction i using lastCases with
  | cast i =>
    induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
  | last =>
    induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp

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

Goal state before:
pp: α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
⊢ Finite α

Tactic:
by
  rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩
  classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

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

Goal state before:
pp: case pos
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
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
cases hk

Goal state after:
case pos.refl
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
H₁ : i.succAbove j ≠ last n
⊢ ∀ (H₂ : i.succAbove j = i.succAbove j), H₂ ▸ p j = p j
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
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
cases hk

Goal state after:
case neg.refl
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
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove j = i.succAbove j), H₂ ▸ p j = p j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ s ∈ Set.range SetLike.coe → s.Finite

Tactic:
rintro ⟨t, rfl⟩

Goal state after:
α : Type u
t : Finset α
⊢ (↑t).Finite
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 γ
⊢ op (f (g x)) (fold op b f (image g xs)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
ih

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 ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a].reverse ↔ IsChain (fun a b ↦ R b a) [a]

Tactic:
| singleton a =>

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      IsChain R (l₂ :: L).flatten ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
isChain_flatten hL.2,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      ((∀ (l : List α), l ∈ l₂ :: L → IsChain R l) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1

Tactic:
List.prod_append,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod

Tactic:
List.prod_append,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
⊢ (∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b
⊢ ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ (n + 1) • s
⊢ a ∈ s

Tactic:
succ_nsmul,

Goal state after:
case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s + s
⊢ a ∈ s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s

Tactic:
succ_nsmul,

Goal state after:
case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s + s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
⊢ filter p (n • ha) = n • filter p ha → filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
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 xs.prod * op x = (map op xs).reverse.prod * op x

Tactic:
ih

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
⊢ (map op xs).reverse.prod * op x = (map op xs).reverse.prod * op x
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]

Goal state after:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s t : Multiset M
h : s ≤ t
⊢ s.prod ∣ t.prod

Tactic:
obtain ⟨z, rfl⟩ := exists_add_of_le h
  simp only [prod_add, dvd_mul_right]

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

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ op (fold op (b a) (t a)) (fold op (fold op b₀ (map b ha)) (ha.bind t)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha))

Tactic:
ih

Goal state after:
case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha))
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
⊢ (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
    (Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
ih : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
⊢ Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi⟩ = l.cyclicPermutations.get ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj

Goal state after:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
ih

Goal state after:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
Module: Mathlib.Data.Multiset.Pi

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

Tactic:
ih

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
⊢ (a ::ₘ s).Nodup → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → (t a_2).Nodup) → ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, a_2 ∈ m.pi t ∧ Pi.cons m a a_1 a_2 = f) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
ih

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
exact ht.image2_right ha (hft _ ha)

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ y ∈ ⋂ i, f '' s i

Tactic:
mem_iInter

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
intro i j hij x y

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
obtain ⟨b, hb⟩ := hst.of_image2_right

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ x ∈ ⋂ i, s i, ∀ y ∈ t, f x y ∈ ⋂ i, image2 f (s i) t

Tactic:
mem_iInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t