mathlib-initiative/mathlib-tactics huggingface dataset:
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'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| f n

Tactic:
hf

Goal state after:
α : 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'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| seqOfForallFinsetExistsAux P r h' n
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
⊢ (∀ (i : Fin n), cons x₀ x i.succ ≤ cons y₀ y i.succ) ↔ x ≤ y

Tactic:
by simp only [cons_succ, Pi.le_def]

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ ↑l = ↑(Fin.cast ⋯ (castAdd n l))

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ ∀ (x : α), x ∈ univ ↔ True

Tactic:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
simp

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

Goal state before:
pp: α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
simp

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

Goal state before:
pp: α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (fun i ↦
      if hi : ↑i < m then ⋯ ▸ (fun i ↦ f (castAdd n i)) (i.castLT hi)
      else ⋯ ▸ (fun i ↦ f (natAdd m i)) (subNat m (Fin.cast ⋯ i) ⋯)) =
    f

Tactic:
simp

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

Goal state before:
pp: case left
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin m
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (castAdd n i✝) = v (castAdd n i✝)

Tactic:
simp

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

Goal state before:
pp: case right
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin n
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (natAdd m i✝) = v (natAdd m i✝)

Tactic:
simp

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

Goal state before:
pp: case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
i : Fin m
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)

Tactic:
simp

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

Goal state before:
pp: case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
j : Fin n
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin m
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inl y)) = Sum.inl y

Tactic:
simp

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

Goal state before:
pp: case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin n
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inr y)) = Sum.inr y

Tactic:
simp

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (castAdd n i)) = castAdd n i

Tactic:
simp

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (natAdd m i)) = natAdd m i

Tactic:
simp

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

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

Tactic:
simp

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 β
hlt : card β < n
⊢ P β

Tactic:
exact ih (Fintype.card β) hlt _ rfl

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

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

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α i

Tactic:
rw [eq_last_of_not_lt h]

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

Goal state before:
pp: case last
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 (last n) = snoc p z (last n)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
f : α → α
hs : Set.MapsTo f ↑∅ ↑∅
⊢ ∃ n ≤ #∅, ∀ (m : ℕ), n ≤ m → image f^[m] ∅ = image f^[n] ∅

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0

Tactic:
simp

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

Goal state before:
pp: case succ.last
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) (last n).succ = snoc (cons a q) b (last n).succ

Tactic:
simp

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

Goal state before:
pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
rw [eq_last_of_not_lt h]

Goal state after:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)

Tactic:
simp

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

Goal state before:
pp: case zero
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
isLt✝ : 0 < n + 1 + m
⊢ (if h : 0 < n + 1 then cases a as ⟨0, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨0, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨0, isLt✝⟩)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
H : l.Nodup
x : { x // x ∈ l }
⊢ (fun i ↦ ⟨l.get i, ⋯⟩) ((fun x ↦ ⟨idxOf (↑x) l, ⋯⟩) x) = x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
a : α
⊢ (fun i ↦ l.get i) ((fun a ↦ ⟨idxOf a l, ⋯⟩) a) = a

Tactic:
simp

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

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
x : α✝ (last n)
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.castSucc
i : Fin n
y : α✝ i.castSucc
z : α✝ (last n)
α : Fin (n + 1) → Type u_2
f : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ (fun f ↦ (f (last n), init f)) ((fun f x ↦ snoc f.2 f.1 x) f) = f

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
x : α✝ (last n)
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.castSucc
i : Fin n
y : α✝ i.castSucc
z : α✝ (last n)
α : Fin (n + 1) → Type u_2
f : (i : Fin (n + 1)) → α i
⊢ (fun f x ↦ snoc f.2 f.1 x) ((fun f ↦ (f (last n), init f)) f) = f

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case mp.slnil
α : Type u_1
l l' : List α
⊢ ∃ f, ∀ (ix : ℕ), [][ix]? = [][f ix]?

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
x✝ : ℕ
⊢ ∀ ⦃b : ℕ⦄, x✝ < b → (fun x ↦ x + 1) x✝ < (fun x ↦ x + 1) b

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ

Tactic:
by
  rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]

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

Goal state before:
pp: case mp.cons_cons.refine_2.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ (a✝¹ :: l₁✝)[0]? = (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) 0]?

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
a : α
inst✝ : Infinite (β a)
x✝¹ x✝ : β a
⊢ (fun x ↦ ⟨a, x⟩) x✝¹ = (fun x ↦ ⟨a, x⟩) x✝ → x✝¹ = x✝

Tactic:
simp

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

Goal state before:
pp: case mp.refine_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (a b : Fin l.length), ⟨f ↑a, ⋯⟩ ≤ ⟨f ↑b, ⋯⟩ ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ l.get i = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) i)

Tactic:
apply Option.some_injective

Goal state after:
case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ some (l.get i) = some (l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) i))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝

Tactic:
simp

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:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
h : {x | p x}.Finite
⊢ h.toFinset = {x | p x}

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∩ ht.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∪ ht.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset \ ht.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinsetᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Fintype α
h : univ.Finite
⊢ h.toFinset = Finset.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u
h : ∅.Finite
⊢ h.toFinset = ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
a✝ : β
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f hs.toFinset

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ x = cons x (fun j ↦ cast ⋯ (p j)) 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f Finset.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset ∪ t.toFinset ↔ x ∈ s ∪ t

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | p a} ↔ x ∈ {a | a ∈ s ∧ p a}

Tactic:
simp

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✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset ∩ t.toFinset ↔ x ∈ s ∩ t

Tactic:
simp

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✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | a ∈ t} ↔ x ∈ s ∩ t

Tactic:
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 : (j : Fin n) → α ((last n).succAbove j)
⊢ x = snoc (fun j ↦ cast ⋯ (p j)) x (last n)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset \ t.toFinset ↔ x ∈ s \ t

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ ∀ (x : α), x ∈ ∅ ↔ x ∈ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
⊢ ∀ (x : α), x ∈ {a} ↔ x ∈ {a}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ 0 < (replicate 2 x).length

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ ∀ (x : α), x ∈ insert a s.toFinset ↔ x ∈ insert a s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ 1 < (replicate 2 x).length

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ ∀ (x : α), x ∈ { val := a ::ₘ s.toFinset.val, nodup := ⋯ } ↔ x ∈ insert a s

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
s : Set α
f : α → β
inst✝ : Fintype ↑s
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ ∀ (x : ℕ), x ∈ Finset.range n ↔ x ∈ {i | i < n}

Tactic:
simp

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u
t : Finset α
⊢ (↑t).Finite

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↑hs.toFinset = s

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ s.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
x✝ : Finset α
⊢ (fun s ↦ ⋯.toFinset) ((fun s ↦ ⟨↑s, ⋯⟩) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
x✝ : { s // s.Finite }
⊢ (fun s ↦ ⟨↑s, ⋯⟩) ((fun s ↦ ⋯.toFinset) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1.zero.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi hj : 0 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

Tactic:
simp

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

Goal state before:
pp: case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f i.rev.rev = i.rev.insertNth a (f ∘ rev) i.rev

Tactic:
simp

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

Goal state before:
pp: case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ i.succ.insertNth x (cons a p) i.succ = cons a (i.insertNth x p) i.succ

Tactic:
simp

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

Goal state before:
pp: case p.zero
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ cons a p 0 = cons a (i.insertNth x p) (i.succ.succAbove 0)

Tactic:
simp

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

Goal state before:
pp: case p.succ
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
i✝ : Fin n
⊢ cons a p i✝.succ = cons a (i.insertNth x p) (i.succ.succAbove i✝.succ)

Tactic:
simp

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:
simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Set α
a : α
hs : (insert a s).Finite
⊢ ∀ (a_1 : α), a_1 ∈ hs.toFinset ↔ a_1 ∈ insert a ⋯.toFinset

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = fun i_1 ↦
      (fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth (f p) (p.removeNth f) = f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
rw [← fold_add op, union_add_inter, fold_add op]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0

Tactic:
simp

Goal state after: