mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) / ↑n < y

Tactic:
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) / ↑n < y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]

Goal state after:
case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ y / δ ≤ ↑m

case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 1 / δ ≤ ↑m
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : (p₁ /ₛ p) / (p₂ /ₛ p) = 1
⊢ p₁ = p₂

Tactic:
sdiv_div_sdiv_cancel_right,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ /ₛ p₂ = 1
⊢ p₁ = p₂
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
split_ifs with h
  · exact count_eq_one_of_mem d h
  · exact count_eq_zero_of_notMem h

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
⊢ l.dedup = a :: l'

Tactic:
have hal : a ∈ l.dedup := mem_dedup.2 h.1

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ l.dedup = a :: l'
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
| cons x xs l_ih =>

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ s.strongDownwardInductionOn H a) = H s fun {t} ht _h ↦ t.strongDownwardInductionOn H ht

Tactic:
dsimp only [strongDownwardInductionOn]
  rw [strongDownwardInduction]

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

Goal state before:
pp: case none
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
h : f a = none
⊢ filterMap f (a ::ₘ s) = (Option.map singleton none).getD 0 + filterMap f s

Tactic:
simp [filterMap_cons_none a s h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun b ↦ decide (p b)) _l) = List.count a _l

Tactic:
apply count_filter

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
exact count_filter_of_neg h

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

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
⊢ l₁ <+: l₂

Tactic:
by rw [prefix_iff_eq_take] at *; nth_rw 1 [h, take_eq_left_iff]; tauto

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

Goal state before:
pp: α : Type u_1
l : List α
m n : ℕ
⊢ take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n

Tactic:
by
  simp [prefix_take_iff, take_prefix]; omega

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse l.inits).reverse

Tactic:
inits_eq_tails l

Goal state after:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.inits = l.reverse.tails.reverse

Tactic:
inits_eq_tails l

Goal state after:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse
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:
by
  simp_rw [← Set.finite_coe_iff, hst.finite_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s t

Tactic:
← erase_insert ha,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s ((insert a t).erase a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
← erase_insert ha,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint ((insert a s).erase a) t
Module: Mathlib.Data.Fin.Basic

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

Tactic:
intro H i

Goal state after:
case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
i : Fin n
⊢ r (f i.castSucc) (f i.succ)
Module: Mathlib.Data.List.OfFn

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

Tactic:
ofFn_succ',

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Tactic:
rw [succAbove_of_lt_succ _ _ h]
    exact Fin.ne_of_gt h

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #t - #s

Tactic:
by
  suffices #(t \ s) = #(t \ s ∪ s) - #s by rwa [sdiff_union_of_subset h] at this
  rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬p.succAbove i < p

Tactic:
succAbove_of_lt_succ _ _ H

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
simp [IH']

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 α
β : Type u_4
inst✝ : Fintype β
⊢ card β < card α → P β

Tactic:
hlt

Goal state after:
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 α
β : Type u_4
inst✝ : Fintype β
hlt : card β < card α
⊢ P β
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a ↦ s.strongDownwardInductionOn H a) = H s fun {t} ht x ↦ t.strongDownwardInductionOn H ht

Tactic:
dsimp only [strongDownwardInductionOn]
  rw [strongDownwardInduction]

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

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

Tactic:
rw [Function.comp_apply, snoc_castSucc]

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

Goal state before:
pp: case mp.cons_cons.refine_1
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (a b : ℕ), ((if a = 0 then 0 else (f a.pred).succ) ≤ if b = 0 then 0 else (f b.pred).succ) ↔ a ≤ b

Tactic:
rintro ⟨_ | a⟩ ⟨_ | b⟩

Goal state after:
case mp.cons_cons.refine_1.zero.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ((if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ≤ if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ↔ 0 ≤ 0

case mp.cons_cons.refine_1.zero.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔ 0 ≤ n✝ + 1

case mp.cons_cons.refine_1.succ.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ≤ if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ↔ n✝ + 1 ≤ 0

case mp.cons_cons.refine_1.succ.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝¹ n✝ : ℕ
⊢ ((if n✝¹ + 1 = 0 then 0 else (f (n✝¹ + 1).pred).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔
    n✝¹ + 1 ≤ n✝ + 1
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ #(map (natEmbedding α) (range n)) = n

Tactic:
card_map,

Goal state after:
α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ #(range n) = n
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

Tactic:
simp only [← Finset.coe_subset, Finite.coe_toFinset]

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

Goal state before:
pp: case pos
α : 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
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

Tactic:
exact absurd (h.trans hj) hi

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α

Tactic:
refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
by
  simp_rw [← not_lt, find_lt_iff, not_exists, not_and]

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:
by
      simp [Fin.find_spec]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGT ↔ l.SortedGT

Tactic:
← sortedLT_reverse,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).reverse.SortedLT ↔ l.reverse.SortedLT
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGT ↔ l.SortedGT

Tactic:
by
  simp_rw [← sortedLT_reverse, ← map_reverse, sortedLT_listMap]

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

Goal state before:
pp: case inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x < ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_lt, h]

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

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

Tactic:
by
  rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.prod

Tactic:
by
  conv_rhs => rw [← coe_toList s]
  rw [prod_coe]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l

Tactic:
induction l using twoStepInduction with
  | nil => grind
  | singleton a => grind
  | cons_cons a b l IH IH2 =>
    rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
⊢ ∀ (l : List M), op l.prod = (map op l).reverse.prod

Tactic:
intro l

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ s.card * count a t

Tactic:
← one_le_count_iff_mem.mpr <| mem_of_subset hsub has,

Goal state after:
case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ s.card * 1
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * ((↑s.toList).erase a).prod = (↑s.toList).prod

Tactic:
coe_erase,

Goal state after:
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (↑(s.toList.erase a)).prod = (↑s.toList).prod
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.toList).erase a)).prod = (map f ↑m.toList).prod

Tactic:
coe_erase,

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.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ l ~r [] ↔ [] = l

Tactic:
isRotated_nil_iff,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
simp only [Finset.Nonempty, mem_biUnion]
  rw [exists_comm]
  simp [exists_and_left]

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

Goal state before:
pp: α : Type u
l : List α
hn : l.Nodup
⊢ l.cyclicPermutations.Nodup

Tactic:
rcases eq_or_ne l [] with rfl | hl

Goal state after:
case inl
α : Type u
hn : [].Nodup
⊢ [].cyclicPermutations.Nodup

case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
← add_one_mul_choose_eq n,

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

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

Tactic:
← add_one_mul_choose_eq n,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})

Tactic:
← filter_product,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})

Tactic:
← filter_product,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
swap : #u = #v
⊢ #u = (#s).choose 2

Tactic:
grind [Nat.mul_sub_one, offDiag_card, Nat.choose_two_right]

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

Goal state before:
pp: case succ
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Tactic:
exact b_ih.trans (choose_le_succ (a + b_n) c)

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

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
refine h.elim fun f => ?_

Goal state after:
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite (α ↪ β)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.1.prod_right h.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f sᶜ = (f '' s)ᶜ

Tactic:
rw [kernImage_eq_compl, compl_compl]

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

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
refine ⟨Function.update z i y, ?_, update_self i y z⟩

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s✝ t : Set α
a : α
s : Set α
⊢ s⁻¹⁻¹ = s

Tactic:
by simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩
    exact empty_pow hn

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
by
  rw [div_eq_mul_inv]; exact subset_mul_right _ hs

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a}

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Nontrivial ↥H
⊢ ∃ x ∈ H, x ≠ 1

Tactic:
rwa [← Subgroup.nontrivial_iff_exists_ne_one]

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
⊢ mrange (inr M N) = ⊥.prod ⊤

Tactic:
by simpa only [mrange_eq_map] using map_inr ⊤

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y

Tactic:
← encodek,

Goal state after:
α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ decode (encode x) = some y