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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk (⇑(isSetoid α)) l)) = filter (fun a ↦ p a ∧ q a) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ filter p (filter q s) = filter q (filter p s)

Tactic:
by simp [and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False

Tactic:
exact (lt_cons_self (s ∩ t) a).not_ge <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a

Tactic:
by
  fconstructor
  · intro H s' hs' s'_card
    by_contra! rid
    have card := card_le_card (monotone_filter_left P hs') |>.trans H
    exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)
  · contrapose!
    exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - 0) = filter p s - filter p 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn [] nil append_singleton = nil

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)

Tactic:
by simp

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

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

Tactic:
rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ ndinsert a s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ a ::ₘ s ≤ a ::ₘ t.erase a

Tactic:
cons_le_cons_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t.erase a
Module: Mathlib.Data.List.Infix

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).inits = [].inits ++ map (fun l ↦ [] ++ l) [].inits.tail

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).inits = [].inits ++ map (fun l ↦ [] ++ l) (a :: t).inits.tail

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).tails = map (fun l ↦ l ++ []) [].tails ++ [].tails.tail

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).tails = map (fun l ↦ l ++ a :: t) [].tails ++ (a :: t).tails.tail

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (s.erase a).erase a = s.erase a

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ range n.succ = n ::ₘ range n

Tactic:
rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
s t : Finset α
h : Disjoint s t
⊢ ∀ (x : α), x ∈ ↑(s.disjUnion t h) ↔ x ∈ ↑s ∪ ↑t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
h : Nodup ⟦[]⟧
⊢ ¬{ val := ⟦[]⟧, nodup := h }.Nontrivial

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ a ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ b ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ : α
s : Finset α
h : a✝ ∉ s
a : α
⊢ a ∈ cons a✝ s h ↔ a ∈ insert a✝ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
f : α → β
a : α
⊢ insert a ∅ = {a}

Tactic:
by simp

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

Goal state before:
pp: s : Finset ℕ
⊢ ∃ n, ∅ ⊆ range n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ j + k ∉ range k

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s \ t ⊆ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ s ∨ x ∈ ∅ ↔ x ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ ∅ ∨ x ∈ s ↔ x ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ x✝ ∈ ∅ ↔ x✝ ∈ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ ∅ ∧ x✝ ∈ s ↔ x✝ ∈ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ∪ t = s ∪ insert a t

Tactic:
insert_union,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∪ t) = s ∪ insert a t
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ univ.val

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∀ (a : α), a ∈ univ → p a) ↔ ∀ (a : α), p a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∃ a, a ∈ univ ∧ p a) ↔ ∃ a, p a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {true, false}.Nodup

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {lt, eq, gt}.Nodup

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach.Nonempty ↔ s.Nonempty

Tactic:
by
  simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α

Tactic:
rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s + t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ a ∈ {x | ¬p x}

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.isEmpty = true ↔ s = ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ univ ∩ s = s

Tactic:
ext a; simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ e.toEmbedding (e.symm b) = b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(filter p univ) = {x | p x}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p univ = univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ {x | x ∈ s} = s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
h : IsEmpty α
⊢ {∅} ⊆ Set.univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
x✝ : IsEmpty α
⊢ Set.univ = {∅}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x y : ↥s
⊢ (fun x ↦ ⟨f ↑x, ⋯⟩) x = (fun x ↦ ⟨f ↑x, ⋯⟩) y → x = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n i j : ℕ
⊢ (fun i ↦ i + 1) i = (fun i ↦ i + 1) j → i = j

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
⊢ (∀ y ∈ image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
⊢ (∃ y ∈ image f s, p y) ↔ ∃ x ∈ s, p (f x)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f : α → β
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(f '' s)
⊢ ↑(f '' s).toFinset = ↑(Finset.image f s.toFinset)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List α
hd : (List.map c l).Nodup
a : β
⊢ a ∈ image c { val := ↑l, nodup := ⋯ } ↔ a ∈ { val := Quot.mk (⇑(List.isSetoid β)) (List.map c l), nodup := hd }

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {True, False}.Nodup

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
b : β
⊢ b ∈ image f univ ↔ b ∈ Set.range f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
y : β
⊢ {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s

Tactic:
by
  simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
a : α
s : Finset α
ha : a ∉ s
x y : ↥s
⊢ (fun x ↦ ⟨↑x, ⋯⟩) x = (fun x ↦ ⟨↑x, ⋯⟩) y → x = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
s' s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (a a' b : α), b ∈ some a → b ∈ some a' → a = a'

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p a

Tactic:
rcases mem_map.1 h with ⟨x, _, rfl⟩

Goal state after:
α : Type u_1
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : (Embedding.subtype fun x ↦ p x) x ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p ((Embedding.subtype fun x ↦ p x) x)
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
xin : y ∈ {i | m ≤ ↑i + n}
⊢ ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) (subNat (m - n) (Fin.cast ⋯ y) ⋯) = y

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ min (↑a) n = ↑a

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ max (↑a) n = n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
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
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ ⟨a, ha⟩ ∈ s.attach ∧ i ↑⟨a, ha⟩ ⋯ = i a ha

Tactic:
by simp

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 % n.succ = ↑i - 1

Tactic:
Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))

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

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

Tactic:
simp only [eq]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = n

Tactic:
by simp

Goal state after:
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 ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₁, ha₁⟩ ∈ ↑s.attach

Tactic:
by simp

Goal state after:
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 ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₂, ha₂⟩ ∈ ↑s.attach

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
rw [succAbove_of_castSucc_lt _ _ h]
    exact Fin.ne_of_lt h

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.succ.succAbove 0 = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ #∅ ≤ n

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ image succ univ = {0}ᶜ

Tactic:
rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ p ∉ map p.succAboveEmb univ

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ (p.castPred ⋯).predAbove i = i.pred ⋯

Tactic:
by
  rw [predAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ x = y

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.11
β : Type ?u.10
inst✝² : DecidableEq α
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty β
a : α
⊢ a ∈ image Prod.fst univ

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.11
β : Type ?u.10
inst✝² : DecidableEq β
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty α
b : β
⊢ b ∈ image Prod.snd univ

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
x✝ : (a : α) ×' β a
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ {⟨⋯, ⋯⟩}

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : Nonempty α
inst✝ : Fintype α
⊢ ∃ x, x ∈ univ.val

Tactic:
by simp

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
α : Fin (n + 1) → Type u_1
f : α 0 × ((i : Fin n) → α i.succ)
⊢ (fun f ↦ (f 0, tail f)) ((fun f ↦ cons f.1 f.2) f) = f

Tactic:
by simp

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
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
⊢ (fun f ↦ cons f.1 f.2) ((fun f ↦ (f 0, tail f)) f) = f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∀ x ∈ ∅, P x

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (last n).predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
⊢ #∅ = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = ∅ ∧ #t = n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ Set.MapsTo f ↑univ ↑univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
a : α
⊢ f a ∈ Set.range f

Tactic:
by simp

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

pp: case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}

Tactic:
· rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩

Goal state after:
case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: n : ℕ
⊢ #univ = n

Tactic:
by simp

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
i : Fin n
⊢ cast ⋯ (p (i.castSucc.castLT ⋯)) = p i

Tactic:
convert! cast_eq rfl (p i)

Goal state after: