mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩ → ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
h

Goal state after:
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✝⟩
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0

Tactic:
Nat.eq_zero_of_le_zero h

Goal state after:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.succ ≤ b.succ ↔ a ≤ b

Tactic:
succ_le_succ_iff

Goal state after:
n : ℕ
a b : Fin n
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
⊢ #s ≤ #t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ #∅ ≤ #t

case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)

Tactic:
by
  rw [← ofFn_id, map_ofFn, Function.comp_id]

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

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

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

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ¬1 < #s ↔ ¬s.Nontrivial

Tactic:
not_lt,

Goal state after:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬s.Nontrivial
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
h

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
h

Goal state after:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β

Tactic:
h

Goal state after:
α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ β ≃ β
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ #{x | p x} = 1

Tactic:
rw [Finset.card_eq_one]
  refine exists_congr fun x => ?_
  simp only [Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff, and_comm,
    mem_filter_univ]

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

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m

Tactic:
h

Goal state after:
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n + m = n + m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m

Tactic:
h

Goal state after:
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m = n + m
Module: Mathlib.Data.List.Duplicate

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

Tactic:
induction h with

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

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

Tactic:
induction h with

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

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

Tactic:
induction h with

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) j = update (init q) i y j

Tactic:
h

Goal state after:
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
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : x₀ = x j
⊢ last n = j.castSucc

Tactic:
h

Goal state after:
case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
j : Fin n
hx₀ : ¬x j ∈ Set.range x
h : x₀ = x j
⊢ last n = j.castSucc
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
⊢ i < j →
    (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
      (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) j

Tactic:
h

Goal state after:
case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
⊢ (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
    (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) j
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i ↦ if ↑i = 0 then n else m

Tactic:
rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
⊢ l₁.flatten <+ l₂.flatten

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x > min y z ↔ x > y ∨ x > z

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x > max y z ↔ x > y ∧ x > z

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
exact .rel ab

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

Goal state before:
pp: a : ℕ
l : List ℕ
hl : map length l.ranges = l
| l

Tactic:
← hl

Goal state after:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
| map length l.ranges
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

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

Tactic:
h

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ l.length - n % l'.length = l'.length - n % l'.length

Tactic:
h

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ l'.length - n % l'.length = l'.length - n % l'.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a ∈ some a

Tactic:
Option.mem_some_iff

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a = a
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r s.join t.join

Tactic:
induction h with

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ i % l.length = j % l.length

Tactic:
by
  rw [← rotate_mod l i, ← rotate_mod l j] at h
  simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
    hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Multiset β
g : β → Option γ
⊢ filterMap g (m.bind f) = m.bind fun a ↦ filterMap g (f a)

Tactic:
simp [bind, filterMap_join]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
induction s using Multiset.induction <;> simp [Nat.add_mod, *]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: F : Type u_1
ι : Type u_2
κ : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
O : Type u_7
M : Type u_8
n : ℕ
hn : n ≠ 0
x y : Multiset M
h : (fun a ↦ n • a) x = (fun a ↦ n • a) y
x✝ : M
⊢ n * count x✝ x = n * count x✝ y

Tactic:
by simp only [← Multiset.count_nsmul, h]

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

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations

Tactic:
· rintro ⟨k, rfl⟩
    rw [cyclicPermutations_rotate, mem_rotate]
    apply mem_cyclicPermutations_self

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

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup

Tactic:
rw [nodup_iff_injective_get]

Goal state after:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ Injective l.cyclicPermutations.get
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).offDiag ~ map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++ l.offDiag

Tactic:
simp only [offDiag, zipIdx_cons']
  have : map (fun x ↦ (x.fst, a)) l.zipIdx = map (·, a) l := by
    conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
  simp [append_assoc, perm_append_left_iff, flatMap_map,
    ← (map_append_flatMap_perm _ _ _).congr_left, this]

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)

Tactic:
apply Nat.one_lt_mul_iff

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
h

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ (a + b).choose a = (a + b).choose b
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
add_one_mul_choose_eq

Goal state after:
n k : ℕ
⊢ (n + 1).choose (k + 1) * (k + 1) = n.succ.choose k.succ * (k + 1)
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val) =
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup

Tactic:
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun f ↦ f a) (piFinset t) = t a

Tactic:
by
  refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_
  choose f hf using ht
  exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
⊢ ∀ (h : a✝ ∈ 0), Pi.empty β a✝ h ∈ t a✝

Tactic:
h

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj b b
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
h : a = 1
⊢ IsConj 1 a

Tactic:
h

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
h : a = 1
⊢ IsConj 1 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
by
  refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)
  injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ x, x⁻¹ ∈ s ∧ p x) ↔ ∃ x, x ∈ s ∧ p x⁻¹

Tactic:
rw [← (Equiv.inv _).exists_congr_right]

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ a, ((Equiv.inv α) a)⁻¹ ∈ s ∧ p ((Equiv.inv α) a)) ↔ ∃ x, x ∈ s ∧ p x⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
by simpa using pow_mem_pow hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t

Tactic:
prod_singleton,

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ (fun a ↦ (a, t)) '' S, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ closure {1} = ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton]

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
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
by
  rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : IsMulCommutative ↥H
a : G'
ha : f a ∈ H
b : G'
hb : f b ∈ H
⊢ f (a * b) = f (b * a)

Tactic:
simpa using setLike_mul_comm ha hb

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ PLift ι

Tactic:
exact PLift.up hι.some

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

Goal state before:
pp: m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp

Goal state after:
m n : ℕ
this : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
⊢ (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂ → H₁ = H₂

Tactic:
h

Goal state after:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
⊢ H₁ = H₂
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
x✝¹ x✝ : ↥(zpowers g)
val✝¹ : G
w✝¹ : ℤ
h₁ : (fun x ↦ g ^ x) w✝¹ = val✝¹
val✝ : G
w✝ : ℤ
h₂ : (fun x ↦ g ^ x) w✝ = val✝
⊢ ⟨val✝¹, ⋯⟩ * ⟨val✝, ⋯⟩ = ⟨val✝, ⋯⟩ * ⟨val✝¹, ⋯⟩

Tactic:
simp [← h₁, ← h₂, zpow_mul_comm]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
· exact (Classical.choose_spec (hf p p)).1

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑⊥ ↔ s ⊆ {1}

Tactic:
coe_bot

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ {1} ↔ s ⊆ {1}
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsIdempotentElem a
n : ℕ
hn : n ≠ 0
⊢ a ^ n = a

Tactic:
by
  obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
  exact h.pow_succ_eq _

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 : Set β
⊢ ⋃ g, g • s = ⋃ i, {x | i • x ∈ s}

Tactic:
← iUnion_inv_smul,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g⁻¹ • s = ⋃ i, {x | i • x ∈ s}
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 s (a • t) ↔ Disjoint (a⁻¹ • s) t

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
⊢ ∀ (g_1 : G), g_1 * g * g_1⁻¹ ∈ iInf a

Tactic:
h

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
⊢ h * g * h⁻¹ ∈ iInf a
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun x1 x2 ↦ x1 ≤ x2) l₁ l₂
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with

Goal state after: