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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
by
  rw [Multiset.add_comm, singleton_add]
  constructor
  · rintro rfl
    exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩
  · rintro ⟨h, rfl⟩
    exact cons_erase h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
convert! List.count_erase_self (a := a) (l := l) <;> rw [← coe_count]

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (map f (hd :: tl)).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y

Tactic:
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d

Goal state after:
case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ m.card = 0

Tactic:
hc,

Goal state after:
case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ card 0 = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = filter p s - a ::ₘ filter p t

Tactic:
sub_cons

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u

Tactic:
by simp [zero_ndunion]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ ↑(cons a s hs) ⊆ ↑(cons a t ht) ↔ s ⊆ t

Tactic:
coe_cons,

Goal state after:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ insert a ↑s ⊆ ↑(cons a t ht) ↔ s ⊆ t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ insert a ↑s ⊆ ↑(cons a t ht) ↔ s ⊆ t

Tactic:
coe_cons,

Goal state after:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ insert a ↑s ⊆ insert a ↑t ↔ s ⊆ t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
exact cons a t ha ht (h ht)

Goal state after:
Module: Mathlib.Data.Finite.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite

Tactic:
simp_rw [← Set.finite_coe_iff, hst.finite_iff]

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

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))

Tactic:
rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]

Goal state after:
case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev ≤ j ↔ j.rev ≤ i

Tactic:
rw [← rev_le_rev, rev_rev]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i ≤ j.rev ↔ j ≤ i.rev

Tactic:
rw [← rev_le_rev, rev_rev]

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
val✝¹ : α
property✝¹ : val✝¹ ∈ s
val✝ : α
property✝ : val✝ ∈ s
h : (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
simpa using i_inj _ _ _ _ h

Goal state after:
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)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
exact ⟨⟨1, by lia⟩, h1⟩

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

Goal state before:
pp: n : ℕ
k : Fin n.succ
this : NeZero n.succ
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
cases n with
  | zero => simp only [Fin.isValue, Fin.zero_le]
  | succ n => rwa [Fin.le_iff_val_le_val, Fin.val_one, Nat.one_le_iff_ne_zero, val_ne_zero_iff]

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

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

Tactic:
← left_inv a1 h1,

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (n * (m - ↑i / n - 1) + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)

Tactic:
Nat.mul_add_mod,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
h : #s ≤ #t
⊢ image f s = t ↔ Set.BijOn f ↑s ↑t

Tactic:
by
  grind [injOn_of_surjOn_of_card_le, Set.BijOn, image_eq_iff_surjOn_mapsTo]

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

Goal state before:
pp: case cons_duplicate
α : Type u_1
l : List α
x y y✝ : α
l✝ : List α
h : x ∈+ l✝
a_ih✝ : l✝ ≠ [y]
⊢ y✝ :: l✝ ≠ [y]

Tactic:
simp [ne_nil_of_mem h.mem]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Tactic:
simp [modNat]

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

Goal state before:
pp: case refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (castAdd (m₂ * n) l)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m₂ * n) l))

Tactic:
simp [modNat]

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

Goal state before:
pp: case last
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (init q) (q (last n)) (last n) = q (last n)

Tactic:
simp [init]

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

Goal state before:
pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ snoc (init q) (q (last n)) i✝.castSucc = q i✝.castSucc

Tactic:
simp [init]

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) i = update (init q) i y i

Tactic:
simp [init]

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

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j

Tactic:
simp [init]

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

Goal state before:
pp: case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
simpa using h'

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l'

Tactic:
simpa using h'

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

Goal state before:
pp: m n : ℕ
p✝ q : Fin n → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
simp [Fin.find_spec]

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

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
simp [Fin.find_spec]

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

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

Tactic:
by
      rcases trichotomous_of r a b with (ab | rfl | ab)
      · exact Or.inl (rel ab)
      · exact (aux _ l₂ _ h).imp cons cons
      · exact Or.inr (rel ab)

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:
by
    rw [mem_cons, not_or, ← Ne] at hL
    rw [flatten_cons, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]
    rw [mem_cons, not_or, ← Ne] at hL
    simp only [forall_mem_cons, and_assoc, flatten_cons, head?_append_of_ne_nil _ hL.2.1.symm]
    exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (Disjoint on f) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
Pi.cons_ne _ h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f a' ⋯ = f a' h'
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
Nat.mul_assoc

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

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

Tactic:
Nat.mul_assoc

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

Goal state before:
pp: case neg.h
α : 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'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

pp: case neg.hf
α : 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'
⊢ ∀ (a_1 : β a),
    a_1 ∈ t a →
      ((t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a' ::ₘ m) a a_1 (Pi.cons m a' a_3 x)) n) ≍
        (t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a ::ₘ m) a' a_3 (Pi.cons m a a_1 x)) n

Tactic:
· rw [cons_swap a a']

Goal state after:
case neg.hf
α : 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'
⊢ ∀ (a_1 : β a),
    a_1 ∈ t a →
      ((t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a' ::ₘ m) a a_1 (Pi.cons m a' a_3 x)) n) ≍
        (t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a ::ₘ m) a' a_3 (Pi.cons m a a_1 x)) n
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.h
α : 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'
b : β a
a✝ : b ∈ t a
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

pp: case neg.hf.hf
α : 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'
b : β a
a✝ : b ∈ t a
⊢ ∀ (a_1 : β a'),
    a_1 ∈ t a' →
      map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n ≍
        map (fun x ↦ Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n

Tactic:
· rw [cons_swap a a']

Goal state after:
case neg.hf.hf
α : 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'
b : β a
a✝ : b ∈ t a
⊢ ∀ (a_1 : β a'),
    a_1 ∈ t a' →
      map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n ≍
        map (fun x ↦ Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.hf.h
α : 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'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

pp: case neg.hf.hf.hf
α : 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'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)

Tactic:
· rw [cons_swap a a']

Goal state after:
case neg.hf.hf.hf
α : 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'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
· exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
  · have : Nonempty α := ⟨a⟩
    simp
  · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (univ.pi t).Finite

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ (univ.pi t).Finite
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 α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ (∀ (a_1 : β a), a_1 ∈ t a → (Multiset.map (Pi.cons s a a_1) (s.pi t)).Nodup) ∧
    Pairwise (Disjoint on fun b ↦ Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Tactic:
refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩

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
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ Pairwise (Disjoint on fun b ↦ Multiset.map (Pi.cons s a b) (s.pi t)) (t a)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = f 0 ∪ iUnion (f ∘ Fin.succ)

Tactic:
by
  cases f using Fin.consCases
  simp [Function.comp_def]

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

Goal state before:
pp: case neg
α : 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
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
Pi.cons_ne _ h

Goal state after:
case neg
α : 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
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y

Tactic:
exact hf k (hi hx) (hj hy) hxy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j

Tactic:
simp_rw [preimage_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ y ∈ range f, f ⁻¹' {y} = univ

Tactic:
rw [biUnion_preimage_singleton, preimage_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Tactic:
rw [mem_iInter₂] at hx

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ i ∈ S ×ˢ T, x ∈ i.1 ×ˢ i.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.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
x : α
hx : x ∈ s
⊢ x = a

Tactic:
exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ ↑H ↔ x * n * x⁻¹ ∈ ↑H

Tactic:
rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ ↑(comap f (closure s))

Tactic:
rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx

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 : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

Tactic:
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: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
⊢ mker f.mrangeRestrict = mker f

Tactic:
by
  ext x
  change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
  simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.closure {x}) = Subgroup.closure {f x}

Tactic:
f.map_closure,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.closure (⇑f '' {x}) = Subgroup.closure {f x}