mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
f : α ↪ ↥s
⊢ Set.range ⇑(f.trans (subtype fun x ↦ x ∈ s)) ⊆ ↑s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h : ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)), P fun i ↦ addCases vₘ vₙ i
v : (i : Fin (m + n)) → γ i
⊢ P v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
⊢ ∃ f, map f univ = s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
⊢ (∃ i, P i) → P (last n) ∨ ∃ i, P i.castSucc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ s.toFinset ⊂ univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Nonempty α

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
⊢ (P (last n) ∨ ∃ i, P i.castSucc) → ∃ i, P i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Fintype ℕ), False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
⊢ Infinite (Equiv.Perm α)

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∃ i, P i) → P p ∨ ∃ i, P (p.succAbove i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (P p ∨ ∃ i, P (p.succAbove i)) → ∃ i, P i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Injective (natEmbeddingAux α)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
L : List α
a : α
⊢ (orderedInsert r a L).length = L.length + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ orderedInsert r a l = takeWhile (fun b ↦ decide ¬r a b) l ++ a :: dropWhile (fun b ↦ decide ¬r a b) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∀ {i : ℕ}, i < l.length → f i < l'.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
⊢ Fintype ι

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
l : List α
x : α
hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)

Tactic:
by

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
⊢ some (l.get i) = some (l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) i))

Tactic:
simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin (n + 1) → β
i : Fin (n + 1)
x✝ : Fin n
⊢ (cons x p ∘ i.succ.succAbove) x✝.succ = cons x (i.removeNth p) x✝.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ insertionSort r l ~ l

Tactic:
by

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)
⊢ p.removeNth (p.insertNth a f) = f

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
⊢ removeNth 0 f = tail f

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth f = init f

Tactic:
by

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)
g : (j : Fin (n + 1)) → α j
⊢ p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ h.toFinset = s.toFinset

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
by

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)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ↑s' = s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
⊢ xₚ = yₚ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊂ ht.toFinset ↔ ↑s ⊂ t

Tactic:
by

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

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

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

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
⊢ h.toFinset = hs.toFinset ∩ ht.toFinset

Tactic:
by

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

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

Tactic:
by

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
⊢ h.toFinset = hs.toFinset ∪ ht.toFinset

Tactic:
by

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
⊢ h.toFinset = hs.toFinset \ ht.toFinset

Tactic:
by

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
⊢ h.toFinset = hs.toFinset ∆ ht.toFinset

Tactic:
by

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
⊢ h.toFinset = hs.toFinsetᶜ

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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
⊢ h.toFinset = Finset.image f hs.toFinset

Tactic:
by

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

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
⊢ h.toFinset = Finset.image f Finset.univ

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
by

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

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

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)
⊢ insertNth 0 x p = cons x fun j ↦ cast ⋯ (p j)

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ insertNth 0 x p = cons x p

Tactic:
by

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
h : t ⊆ s
⊢ Fintype ↑t

Tactic:
by

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

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

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

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

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

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

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
⊢ a ∉ s.toFinset.val

Tactic:
by

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

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

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 ∈ s.toFinset ↔ x ∈ insert a s

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
⊢ ∀ (x : α), x ∈ { val := Multiset.filterMap g (f '' s).toFinset.val, nodup := ⋯ } ↔ x ∈ s

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype ↑{i | i ≤ n}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
p : Finset α → Prop
h : ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
s : Finset α
⊢ p s

Tactic:
by

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

Goal state before:
pp: α : Type u
p : Finset α → Prop
x✝ : ∃ s, p s
s : Finset α
hs : p s
⊢ p ⋯.toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ∈ Set.range SetLike.coe → s.Finite

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Multiset α
⊢ {x | x ∈ s}.Finite

Tactic:
by

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

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

Tactic:
by

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

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

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

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

Tactic:
by

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✝ : Finite ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}

Tactic:
by

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)
⊢ (last n).insertNth x p = snoc (fun j ↦ cast ⋯ (p j)) x

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ (last n).insertNth x p = snoc p x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ Pairwise r l → insertionSort r l = l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
⊢ (orderedInsert r x []).erase x = []

Tactic:
grind [Std.Refl]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r x tail✝).erase x = tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝

Tactic:
grind [Std.Refl]

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Infinite
⊢ s ≠ ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
xs : List α
hx : ¬x ∈ xs
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Antisymm r
x : α
xs : List α
hx : x ∈ xs
hxs : Pairwise r xs
⊢ orderedInsert r x (xs.erase x) = xs

Tactic:
by

Goal state after: