mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
d : (map f []).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → f x = f y → x = y

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
h : [][0]? = [].getLast?
⊢ [].reverse.tail.Nodup ↔ [].tail.Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : [].Nodup
i : ℕ
h : i < [].length
⊢ [].erase [][i] = [].eraseIdx i

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hl : [].Nodup
⊢ map (update f x y) [] = if x ∈ [] then (map f []).set (idxOf x []) y else map f []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].dedup = [] ↔ [] = []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ ([] ++ l₂).dedup = [] ∪ l₂.dedup

Tactic:
| nil =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
rw [dedup_cons_of_mem' h, insert_of_mem h]

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
⊢ (map f []).dedup = map f [].dedup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [] ⊆ ys
⊢ [] ∪ ys = ys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [].Disjoint ys
⊢ [] ∪ ys = [].dedup ++ ys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ <+ [] ∩ l₂

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ [].bagInter t₁ = [].bagInter t₂

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
by_cases h'' : n ≤ xs.length
  · let n' := xs.length - n
    have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
    have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]
    rw [h₁]
    apply (reverse_perm _).trans
    rw [inter_reverse]
    apply Perm.take_inter _ _ h'
    apply (reverse_perm _).trans; assumption
  · grind [drop_eq_nil_of_le]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - t + t ∩ s = s

Tactic:
IH

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : 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 α
⊢ filter p (s.erase a - t) = filter p s - filter p (a ::ₘ t)

Tactic:
IH

Goal state after:
α : 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 α
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
h : l₁ <+: []
⊢ [] = l₁ ++ drop l₁.length []

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
head✝ : α
tail✝ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝ → tail✝ = l₁ ++ drop l₁.length tail✝
h : [] <+: head✝ :: tail✝
⊢ head✝ :: tail✝ = [] ++ drop [].length (head✝ :: tail✝)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
⊢ [].tails.length = [].length + 1

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
h : n < [].tails.length
⊢ [].tails[n] = drop n []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
h : n < [].inits.length
⊢ [].inits[n] = take n []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial

Tactic:
exact Set.eq_singleton_or_nontrivial ha

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ ([] ++ l').toFinset = [].toFinset ∪ l'.toFinset

Tactic:
| nil =>

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

Goal state before:
pp: case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

Tactic:
have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
    specialize h _ this (e.symm _).is_lt
    simp only [Fin.eta, OrderIso.apply_symm_apply] at h
    rwa [h]

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

Goal state before:
pp: n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
⊢ ↑i - ↑1 = ↑i - 1

Tactic:
Fin.val_one',

Goal state after:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
⊢ ↑i - 1 % n.succ = ↑i - 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ image f s = t
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n.succ → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))

Tactic:
by
  induction n with
  | zero => rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
  | succ n IH =>
    rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
    simp only [succ_eq_add_one, Fin.castSucc_succ]

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

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
· exact succ_injective _ hij

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

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

Tactic:
by
  rw [← card_sdiff_of_subset] <;> grind

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

Goal state before:
pp: α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Tactic:
by
  simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn,
    Fin.forall_iff,
    Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]

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

Goal state before:
pp: case a
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ t ∪ u ⊆ s

Tactic:
exact union_subset hts hus

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

Goal state before:
pp: α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ f ≍ g

Tactic:
rw [ofFn_inj'] at h

Goal state after:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi
  exact predAbove_zero_succ

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ {x ∈ s | x i = ai} ⊂ s

Tactic:
rw [filter_ssubset]

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ ∃ x ∈ s, ¬x i = ai
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f

Tactic:
by
    simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj))

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []

Tactic:
| nil =>

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

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ l ↔ [x, x] <+ y :: l

Tactic:
IH

Goal state after:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case nil
α : Type u_1
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), [][ix]? = l'[f ix]?
⊢ [] <+ l'

Tactic:
| nil =>

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

Goal state before:
pp: 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

Tactic:
apply hx₀.elim (Set.mem_range_self j)

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
hi : insertionSort r l = []
⊢ orderedInsert r a [] = [a]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
hl : ∀ (a : α), a ∈ [] → ∀ (b : α), b ∈ [] → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r []) = insertionSort s (map f [])

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u
s : Finset α
⊢ ⋯.toFinset = s

Tactic:
by
  rw [toFinite_toFinset, toFinset_coe]

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t

Tactic:
by
  rw [← sep_eq_of_subset h]
  infer_instance

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
bs : List α
x : α
hb : Pairwise r bs
hs : [] <+ bs
⊢ orderedInsert r x [] <+ orderedInsert r x bs

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
hb : Pairwise r []
hs : a :: as <+ []
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x []

Tactic:
| nil =>

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

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

Tactic:
cases hs

Goal state after:
case cons.cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

case cons.cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x a then x :: a :: bs else a :: orderedInsert r x bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x (b :: bs)

Tactic:
unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih
      · simp_all
      · exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

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 grind

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
· have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: case nil
⊢ Pairwise Disjoint [].ranges

Tactic:
| nil =>

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

Goal state before:
pp: case nil
⊢ map length [].ranges = []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ ([] ×ˢ l₂).length = [].length * l₂.length

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []

Tactic:
| nil =>

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.prod

Tactic:
← coe_toList s

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
| (↑s.toList).prod
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
⊢ IsChain R [].reverse ↔ IsChain (fun a b ↦ R b a) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
M : Type u_8
inst✝ : CommMonoid M
h : IsUnit [].prod
⊢ ∀ (m : M), m ∈ [] → IsUnit m

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
⊢ (map (fun x ↦ count x []) (filter p [].dedup)).sum = countP p []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
hm : IsChain (fun x1 x2 ↦ x1 > x2) []
hmas : [] ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) [a]

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
ha : IsChain (fun x1 x2 ↦ x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ a > b

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = (map (fun a ↦ (l₂ a).length) []).sum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
⊢ IsChain (fun x1 x2 ↦ x1 = x2) [] ↔ ∀ (a : α), a ∈ [].head? → [] = replicate [].length a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
⊢ op [].prod = (map op []).reverse.prod

Tactic:
| nil =>

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

Goal state before:
pp: case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
⊢ ∀ {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod

Tactic:
T

Goal state after:
case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
⊢ a ∈ S → T ⊆ S → (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
haS : a ∈ S
a✝ : T ⊆ S
⊢ (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Tactic:
IH

Goal state after:
case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
haS : a ∈ S
a✝ : T ⊆ S
IH : (map g1 T).prod ∣ (map g2 T).prod
⊢ (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
hL : [] ≠ []
⊢ [].getLast hL :: [].dropLast ~r []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
n : ℕ
h : n < [].cyclicPermutations.length
⊢ [].cyclicPermutations[n] = [].rotate n

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + s ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
IH

Goal state after:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ (map (Sigma.mk a) (t a + u a) + s.sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
IH

Goal state after:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count (a, b) [].offDiag = count a [] * count b [] - if a = b then count a [] else 0

Tactic:
| nil =>

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

Goal state before:
pp: n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)

Tactic:
choose_succ_right _ _ hn,

Goal state after:
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]
  exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm

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

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (1 + 1).multichoose k = k + 1 + 1

Tactic:
IH

Goal state after:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
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:
rw [Pi.cons_ne _ h]
      apply hf'

Goal state after:
Module: Mathlib.Algebra.Group.Conj

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

Tactic:
have ha := mem_conjugatesOf_self (a := b)
    rwa [← h] at ha

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x} ⊔ closure {y} ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
mem_sup

Goal state after:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.bodd = n.bits.headI

Tactic:
by
  induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]

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

Goal state before:
pp: a b k : ℤ
⊢ (fun x ↦ x • a) k = b ↔ b = a * k

Tactic:
rw [mul_comm, eq_comm, ← smul_eq_mul]

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

Goal state before:
pp: z : ℤ
⊢ z ∈ AddSubgroup.zmultiples 1 ↔ z ∈ ⊤

Tactic:
simp [Int.mem_zmultiples_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
⊢ ∃ a, f a = d

Tactic:
have H := congr_arg length hb

Goal state after:
case mp.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
H : ((map f) 1).length = (of d).length
⊢ ∃ a, f a = d