mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
by
  rw [← rel_flip, rel_add_left]; simp [rel_flip]

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

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

Tactic:
by rw [← card_eq_one, ← card_map, h, card_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ∪ 0 = s

Tactic:
simp [union_def]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
rw [cons_inter_of_neg _ h]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
exact Multiset.add_le_add_right inter_le_left

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then 1 else 0) + (filter (fun a ↦ p (f a)) t).card

Tactic:
Nat.add_comm

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ (if p (f a) then 1 else 0) + (filter (fun a ↦ p (f a)) t).card =
    (if p (f a) then 1 else 0) + (filter (fun a ↦ p (f a)) t).card
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
n : l.Nodup
⊢ (↑l).Nodup

Tactic:
by rwa [Multiset.coe_nodup]

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

Goal state before:
pp: α : Type u_1
n m : ℕ
l : List α
⊢ take n l ++ drop (n + m) l = take n l ++ drop (n + m) l

Tactic:
Nat.add_comm

Goal state after:
α : Type u_1
n m : ℕ
l : List α
⊢ take n l ++ drop (m + n) l = take n l ++ drop (m + n) l
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Set.univ.Nonempty ↔ Nonempty α

Tactic:
Set.nonempty_iff_univ_nonempty

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ Set.univ.Nonempty ↔ Set.univ.Nonempty
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
simp [compl_eq_univ_sdiff]

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ a * (b / c) ≤ a * b / c

Tactic:
obtain rfl | hlt : c = 0 ∨ 0 < c := by lia

Goal state after:
case inl
a : Int
ha : 0 ≤ a
b : Int
hc : 0 ≤ 0
⊢ a * (b / 0) ≤ a * b / 0

case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n✝ m n : ℕ
⊢ NeZero (1 + n)

Tactic:
Nat.add_comm

Goal state after:
n✝ m n : ℕ
⊢ NeZero (n + 1)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i ≠ last n

Tactic:
by rw [← lt_last_iff_ne_last] at hj ⊢; exact Fin.lt_of_le_of_lt h hj

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

Goal state before:
pp: case inl
n : ℕ
a : Fin (n + 1)
hb : a ≠ last n
h : a ≤ a
⊢ ↑(a.castPred ⋯ - a.castPred hb) = ↑(a - a) - 1

pp: case inr
n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
h' : a < b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
· simp [val_sub, Nat.sub_add_cancel a.is_le]

Goal state after:
case inr
n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
h' : a < b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ predAbove 0 i.succ = i

Tactic:
by
  rw [predAbove_succ_of_le _ _ (Fin.zero_le _)]

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

pp: case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Tactic:
· rw [hi, predAbove_right_zero]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
by
  classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

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

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0

Tactic:
exact Fin.cons_zero _ _

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:
strongInduction

Goal state after:
α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ (H s fun t h ↦
      have this := ⋯;
      strongInduction H t) =
    H s fun t x ↦ strongInduction H t
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin m ⊕ Fin n
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) x) = x

Tactic:
by rcases x with y | y <;> simp

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

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

Tactic:
strongInduction

Goal state after:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ (H s fun t h ↦
      have this := ⋯;
      strongInduction H t) =
    H s fun t x ↦ strongInduction H t
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l

Tactic:
simpa [duplicate_cons_iff, hx.symm] using h

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l

Tactic:
simp_rw [nodup_iff_sublist, duplicate_iff_sublist]

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

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

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

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a

Tactic:
ext i
  refine Fin.lastCases ?_ (fun i ↦ ?_) i
  · simp only [Function.comp_apply]
    rw [snoc_last, natAdd_last, snoc_last]
  · simp only [comp_apply, snoc_castSucc]
    rw [natAdd_castSucc, snoc_castSucc]

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

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

Tactic:
rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ cons a f i.rev = snoc (f ∘ rev) a i

Tactic:
simpa using insertNth_rev 0 a f i

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ cons a f i.rev = snoc (f ∘ rev) a i

Tactic:
by
  simpa using insertNth_rev 0 a f i

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 α
a : α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
rw [cons_val, Multiset.map_cons, fold_cons_left]

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 α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
unfold fold
  rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]

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

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

Tactic:
rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]

Goal state after:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case refine_2
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ R l[i] l[j]

Tactic:
· grind [h _ _ <| List.drop_suffix i _ |>.isInfix.trans <| l.take_prefix (j + 1) |>.isInfix]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ R a b ∧ IsChain R (b :: l₁ ++ l₂) ↔
    (R a b ∧ IsChain R (b :: l₁)) ∧
      IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
isChain_append,

Goal state after:
α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    (R a b ∧ IsChain R (b :: l₁)) ∧
      IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
by
    rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
      ← cons_append, isChain_append, and_assoc]
    simp

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₁ ++ (l₂ :: L).flatten) ↔
    (∀ (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_append,

Goal state after:
α : 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)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[m + n % l.length]?

Tactic:
Nat.add_comm

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[m + n % l.length]? = l[m + n % l.length]?
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 : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
intro a ha 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: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
by
  rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ take (n % l'.length) l' ++ drop (n % l.length) l = l'

Tactic:
hd,

Goal state after:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ take (n % l'.length) l' ++ drop (n % l'.length) l' = l'
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
disjoint_disjiUnion_left,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ ∀ i ∈ s, Disjoint (f i) (s.disjiUnion g hg)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((k + ↑⟨n, hn⟩) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
Nat.add_comm

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (1 + n) * n ! = (n + 1) * n !

Tactic:
Nat.add_comm

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n + 1) * n ! = (n + 1) * n !
Module: Mathlib.Data.Finset.Prod

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

Tactic:
Set.disjoint_prod

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

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hm, Nat.zero_mul, Nat.choose_eq_zero_iff]
    exact Nat.pos_of_ne_zero hn

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · have hk := congr_fun h k
    have hl := congr_fun h l
    have hm := congr_fun h m
    have hn := congr_fun h n
    grind [mul_one, one_mul, mul_apply]
  · aesop (add simp [mulSingle_apply])

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = ⇑m '' (⇑m ⁻¹' s * ⇑m ⁻¹' t)

Tactic:
image_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = ⇑m '' ⇑m ⁻¹' s * ⇑m '' ⇑m ⁻¹' t
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ comap f H = f.ker ↔ Disjoint H f.range

Tactic:
by
  rw [← H.ker_le_comap f |>.ge_iff_eq', ← map_eq_bot_iff, map_comap_eq, disjoint_iff, inf_comm]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

Tactic:
have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext : 1; simp
  rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]

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
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u ↔ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
constructor
  · intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, Submonoid.one_mem _⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨Submonoid.one_mem _, hx⟩
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1
    have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2
    simpa using Submonoid.mul_mem _ h1' h2'

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (1 + m)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
Nat.add_comm

Goal state after:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n

Tactic:
exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

Tactic:
by
  simpa using disjoint_smul_set (a := a) (t := a⁻¹ • t)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ toLex y < toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 < x.2

Tactic:
rw [eq_comm, toLex_lt_toLex]

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → x = y

Tactic:
by rw [Subtype.ext_iff]; exact @Std.Trichotomous.trichotomous α r _ x y

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
| coe m =>

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = y

Tactic:
cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: case H
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s

Tactic:
| _ s ihs
   => 

Goal state after:
case H
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ [] = map (fun x ↦ [x]) []

Tactic:
map_nil

Goal state after:
α : Type u
l : List α
⊢ [] = []
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + l.length.choose n = l.length.choose n + l.length.choose n.succ

Tactic:
Nat.add_comm

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose n + l.length.choose (n + 1) = l.length.choose n + l.length.choose n.succ
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
⊢ #(eraseNone s) ≤ #s

Tactic:
rw [card_eraseNone_eq_card_erase]
  apply card_erase_le

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
⊢ #(eraseNone s) ≤ #s

Tactic:
by
  classical
  rw [card_eraseNone_eq_card_erase]
  apply card_erase_le

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, y ≤ x

Tactic:
simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, ∃ a_2, f a ≤ if a_2 ∈ s then f a_2 else sSup ∅