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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ xs ∪ ys = ys

Tactic:
ih <| subset_of_cons_subset h

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ ys = ys
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
Multiset.count_add,

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t), t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
intro t ht

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t

Tactic:
simp [ndinter, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s).ndinter t = s.ndinter t

Tactic:
simp [ndinter, h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
apply univ_map_subtype

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (filter p univ).val

Tactic:
by
  rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]

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

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

Tactic:
let A : Fintype (∅ : Set α) := Fintype.ofIsEmpty

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Image

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ_apply', iterate_succ', ih, image_image]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
by
  obtain h | h := (rev p).succ_le_or_le_castSucc i
  · rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
  · rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]

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

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ a.pred ⋯ ≤ b.pred ⋯

Tactic:
simp only [le_iff_val_le_val, val_pred]

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.pred ⋯ ≤ b.castPred ⋯

Tactic:
simp only [le_iff_val_le_val, val_pred]

Goal state after:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ a.castPred ⋯ ≤ b.pred ⋯

Tactic:
simp only [le_iff_val_le_val, val_pred]

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯

Tactic:
simp only [le_iff_val_le_val, val_pred]

Goal state after:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
exact ⟨0, h0⟩

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ (j - i).castLT ⋯ ≠ 0

Tactic:
refine Ne.symm (ne_of_val_ne ?_)
  simp [coe_sub_iff_le.mpr (Fin.le_of_lt hij)]
  lia

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ castLE h ↑a = ↑(a % m)

Tactic:
ext
  simp only [val_castLE, val_natCast]
  rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
h : i ≠ last n
⊢ i.castPred h = 0 ↔ i = 0

Tactic:
by
  rw [← castPred_zero, castPred_inj]

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = ↑i * n + 1 * n

Tactic:
Nat.one_mul

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = ↑i * n + n
Module: Mathlib.Data.List.OfFn

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

Tactic:
simp_rw [ofFn_succ', succ_mul]

Goal state after:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun i ↦ f (Fin.cast ⋯ i)) =
    ((ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i.castSucc * n + ↑j, ⋯⟩).concat
        (ofFn fun j ↦ f ⟨↑(Fin.last m) * n + ↑j, ⋯⟩)).flatten
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ Injective p.succAbove

Tactic:
rintro i j hij
  unfold succAbove at hij
  split_ifs at hij with hi hj hj
  · exact castSucc_injective _ hij
  · rw [hij] at hi
    cases hj <| Nat.lt_trans j.castSucc_lt_succ hi
  · rw [← hij] at hj
    cases hi <| Nat.lt_trans i.castSucc_lt_succ hj
  · exact succ_injective _ hij

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

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

Tactic:
by
  rw [← succ_zero_eq_one']
  exact succ_succAbove_succ i 0

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ S₂ ⊆ S₁ᶜ

Tactic:
Finset.subset_compl_iff_disjoint_left

Goal state after:
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ Disjoint S₁ S₂
Module: Mathlib.Data.Finset.Card

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

Tactic:
three_lt_card_iff,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = append (snoc xs y) ys ∘ Fin.cast ⋯

Tactic:
rw [append_left_snoc]

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ t, s ⊆ t ∧ #t = 0

Tactic:
exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩

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

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ i.succ.insertNth x (cons a p) (i.succ.succAbove j) = cons a (i.insertNth x p) (i.succ.succAbove j)

Tactic:
simp only [insertNth_apply_succAbove]

Goal state after:
case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ cons a p j = cons a (i.insertNth x p) (i.succ.succAbove j)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i, h⟩ ≤ l.get ⟨i_1, h_1⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
grind [pairwise_iff_getElem]

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i_1, h_1⟩ ≤ l.get ⟨i, h⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 ≥ x2) l

Tactic:
grind [pairwise_iff_getElem]

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i, h⟩ < l.get ⟨i_1, h_1⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 < x2) l

Tactic:
grind [pairwise_iff_getElem]

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i_1, h_1⟩ < l.get ⟨i, h⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 > x2) l

Tactic:
grind [pairwise_iff_getElem]

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 : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
· rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt 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 : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
induction s using Finset.induction_on with

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 α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
H : [].length ≤ l₂.length
h : [] ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] l₂

Tactic:
rcases l₂ with - | ⟨b, l₂⟩

Goal state after:
case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] []

case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] (b :: l₂)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
l₂ : List α
H : (head✝ :: tail✝).length ≤ l₂.length
h : head✝ :: tail✝ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) l₂

Tactic:
rcases l₂ with - | ⟨b, l₂⟩

Goal state after:
case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
⊢ (range a).Disjoint (map (fun x ↦ a + x) s')

Tactic:
intro u

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
⊢ u ∈ range a → u ∈ map (fun x ↦ a + x) s' → False
Module: Mathlib.Data.List.Range

Goal state before:
pp: a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ {a_1 b : List ℕ}, a_1.Disjoint b → (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)

Tactic:
intro u

Goal state after:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u : List ℕ
⊢ ∀ {b : List ℕ}, u.Disjoint b → (map (fun x ↦ a + x) u).Disjoint (map (fun x ↦ a + x) b)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate n.succ = l

Tactic:
rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
rw [count_bind, hm', sum_cons]

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (f x) + m'.sum
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
choose_succ_succ' (n + 1) (k + 1),

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = ((n + 1).choose (k + 1) + (n + 1).choose (k + 1 + 1)) * (k + 1 + 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n.choose k

Tactic:
choose_eq_factorial_div_factorial hk,

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n ! / (k ! * (n - k)!)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
by_cases eq : a = a'

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Tactic:
exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

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

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

Tactic:
by
  induction m using Multiset.induction_on with
  | empty =>
    have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
    simp only [this, pi_zero, mem_singleton, true_iff]
    intro _ h; exact (notMem_zero _ h).elim
  | cons a m ih => ?_
  simp_rw [pi_cons, mem_bind, mem_map, ih]
  constructor
  · rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
    by_cases h : a' = a
    · subst h
      rwa [Pi.cons_same]
    · rw [Pi.cons_ne _ h]
      apply hf'
  · intro hf
    refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
    rw [Pi.cons_eta]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t

Tactic:
image_inter_preimage,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
rw [sInter_eq_biInter]
  apply image_iInter₂_subset

Goal state after:
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
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb

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
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
Module: Mathlib.Algebra.Group.Subgroup.Defs

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

Tactic:
by
    rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
⊢ f.ker = ⊤ ↔ f = 1

Tactic:
simp [ker, ← top_le_iff, SetLike.le_def, f.ext_iff]

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

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rintro y (h | h)
      · exact ⟨y, h, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, y, h, by simp⟩

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s

Tactic:
by simp [mem_prod, MonoidHom.coe_fst]

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

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a + (b₁ + a * a) < a + b₂ * b₂

Tactic:
Nat.add_lt_add_iff_left

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ + a * a < b₂ * b₂
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
· simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
    by_cases h₂ : a < b₂; swap; · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
    rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
    exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
x : G × N
⊢ x ∈ K.prod ⊤ ↔ x ∈ comap (MonoidHom.fst G N) K

Tactic:
by simp [mem_prod, MonoidHom.coe_fst]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x2 ↦ 1 • x2) '' s = s

Tactic:
one_smul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun a ↦ a) '' s = s
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : (map f l).prod < (map g l).prod
⊢ ∃ i, i ∈ l ∧ f i < g i

Tactic:
by
  contrapose! h
  exact prod_le_prod' h

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a b : α), True → True → f (a * b) ≤ f a * f b

Tactic:
by simp [h_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
rw [← SetLike.le_def]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S

Tactic:
exact le_iSup _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
rw [← SetLike.le_def]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S