mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)

Tactic:
intro j ihj hij

Goal state after:
case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i < j.succ
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
x : β
hx : x ∈ ↑t
⊢ x ∈ f' '' ↑s.attach

Tactic:
simpa [f'] using hsurj x hx

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

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

Tactic:
Nat.add_mul_mod_self_right,

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, y.succAbove z = x

Tactic:
by
  obtain hxy | hyx := Fin.lt_or_lt_of_ne h
  exacts [⟨_, succAbove_castPred_of_lt _ _ hxy⟩, ⟨_, succAbove_pred_of_lt _ _ hyx⟩]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
exact card_le_one

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
by
  constructor
  · rw [card_eq_succ]
    grind [card_eq_one]
  · grind

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Tactic:
ext
  simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
    dite_eq_ite, apply_ite Fin.val, val_succ]
  split_ifs <;> lia

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

Goal state before:
pp: case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Tactic:
· rcases h with (⟨rfl | h⟩ | h)
    · simpa
    · exact h.cons_duplicate

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ update (snoc p x) (last n) z = snoc p z

Tactic:
by
  ext j
  cases j using lastCases <;> simp

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = l'[f 0 + 1 + (f (ix + 1) - (f 0 + 1))]?

Tactic:
Nat.add_sub_cancel',

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = l'[f (ix + 1)]?

α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
f : α ↪ ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth x p j = ⋯ ▸ p (j.castPred ⋯)

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(s ∪ t)

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝ : Fintype ↑s
⊢ Finite ↑(s ∪ t)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
⊢ Finite ↑(f '' s)

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑(f '' s)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
⊢ ∀ {s_1 : Set α},
    a ∉ s_1 →
      s_1.Finite → (∀ (hts : s_1 ⊆ s), motive s_1 ⋯) → ∀ (hts : Insert.insert a s_1 ⊆ s), motive (Insert.insert a s_1) ⋯

Tactic:
s

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
⊢ a ∉ s → s.Finite → (∀ (hts : s ⊆ s✝), motive s ⋯) → ∀ (hts : Insert.insert a s ⊆ s✝), motive (Insert.insert a s) ⋯
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.dropLast.reverse

Tactic:
mem_reverse

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.dropLast
Module: Mathlib.Data.List.Range

Goal state before:
pp: case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
⊢ IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: 0 :: map succ (range n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
isChain_cons_cons,

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 ∧ IsChain r (0 :: map succ (range n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : 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₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
by_cases ab : a = b
      · subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact .rel ab

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Tactic:
simp [List.sigma, mem_flatMap, mem_map, exists_and_left, and_left_comm,
    exists_eq_left, exists_eq_right]

Goal state after:
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:
isChain_cons_cons,

Goal state after:
α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ R a b ∧ IsChain R (b :: (l₁ ++ l₂)) ↔
    IsChain R (a :: 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 α
⊢ R a b ∧ IsChain R (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:
isChain_cons_cons,

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

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun a b ↦ R b a) (a :: b :: l)

Tactic:
isChain_cons_cons,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun a b ↦ R b a) (b :: l)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a // p a } → { a // p a } → Prop
⊢ IsChain r (l.attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l

Tactic:
induction l with grind +splitIndPred

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

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

Tactic:
intro c d e _ ih

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

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

Tactic:
rw [succ_nsmul, mem_add] at h

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

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

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:
· simp only [filter_zero, nsmul_zero]

Goal state after:
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)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f (m.erase a)).prod = (map f m).prod

Tactic:
← m.coe_toList,

Goal state after:
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f ((↑m.toList).erase a)).prod = (map f ↑m.toList).prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
m : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p m = m.bind fun a ↦ if p a then {a} else 0

Tactic:
induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filter_cons, ih]

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

Goal state before:
pp: case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + ((hd :: tl).length * n - n)) = hd :: tl

Tactic:
Nat.add_sub_cancel',

Goal state after:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate ((hd :: tl).length * n) = hd :: tl

case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n
Module: Mathlib.Data.Finset.Union

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

Tactic:
s

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.offDiag.length = l.length ^ 2 - l.length

Tactic:
by
  simp [length_offDiag', Nat.mul_sub, Nat.pow_two]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) ≍ cons (a ::ₘ m) a' b' (cons m a b f)

Tactic:
by
  apply hfunext rfl
  simp only [heq_iff_eq]
  rintro a'' _ rfl
  refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_
  rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
  on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
  all_goals simp [*, Pi.cons_same, Pi.cons_ne]

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

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

Tactic:
simp only [succ_add_sub_one]

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

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

Tactic:
s

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
⊢ (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
    (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
      (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
    refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
    rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
    exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
have hG : 0 < Fintype.card G := Fintype.card_pos
  rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)
  · refine fun k hk ↦ Fintype.card_congr ?_
    rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]
  have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
      (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
    refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
    rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
    exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))
  have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
    monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha
  refine fun _ ↦ Nat.stabilises_of_monotone mono (fun n ↦ set_fintype_card_le_univ (S ^ n))
    fun n h ↦ le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) ?_)
  replace h₂ : S ^ n * {a} = S ^ (n + 1) := by
    have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
    refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
    · exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)
    · convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)
  rw [pow_succ', ← h₂, ← mul_assoc, ← pow_succ', h₂, mul_singleton, forall_mem_image]
  intro x hx
  rwa [mul_inv_cancel_right]

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

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

Tactic:
by_cases i = k <;> simp_all

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H

Tactic:
simpa using mul_mem (inv_mem h) hab

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
hf : Injective ⇑f
M' : Submonoid M
⊢ Injective ⇑(f.submonoidMap M')

Tactic:
grind [Injective, submonoidMap_apply_coe]

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

Goal state before:
pp: x✝² x✝¹ x✝ : ℕ
hk : x✝ ≤ x✝¹
⊢ x✝² <<< (x✝¹ - x✝) = x✝² <<< x✝¹ >>> x✝

Tactic:
by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

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

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit false x✝¹ + bit true x✝

Tactic:
by dsimp [bit]; lia

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

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit false (x✝¹ + x✝) = bit false x✝¹ + bit false x✝

Tactic:
by dsimp [bit]; lia

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

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit true x✝¹ + bit false x✝

Tactic:
by dsimp [bit]; lia

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

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (fun n ↦ (decode n).getD d) (encode x) = x

Tactic:
by simp_rw [Encodable.encodek]; rfl

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

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit true x✝¹ ≤ bit true x✝

Tactic:
by dsimp [bit]; lia

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

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit false x✝¹ ≤ bit false x✝

Tactic:
by dsimp [bit]; lia

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

Goal state before:
pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Tactic:
apply Nat.add_lt_add_right; assumption

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}

Tactic:
exact mem_closure_singleton.symm

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ a * 1 * a⁻¹ ∈ H

Tactic:
rw [mul_one, mul_inv_cancel]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
by
  obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
  · exact ⟨1, by simp [hAB]⟩
  refine ⟨z, ?_⟩
  calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
by
  have : Nonempty S := Sne.to_subtype
  simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val]

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < (a :: b :: l).prod

Tactic:
simp only [forall_eq_or_imp, List.mem_cons] at hl₁
    rw [List.prod_cons]
    apply one_lt_mul_of_lt_of_le' hl₁.1
    apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
    grind

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

Goal state before:
pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
List.eq_replicate_iff.2 ⟨_, h⟩,

Goal state after:
M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ (replicate ?m.37 1).prod = 1

M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?m.37
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm '' t

Tactic:
e.symm.image_eq_preimage_symm

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}

Tactic:
exact mem_closure_singleton.symm

Goal state after: