mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ InjOn f s ↔ BijOn f s s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l c : List α
a : α
hl : c <+ l
ha : ∀ (a' : α), a' ∈ c → r a a'
⊢ a :: c <+ orderedInsert r a l

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
by

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

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ cons a f ∘ rev = snoc (f ∘ rev) a

Tactic:
by

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

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

Tactic:
by

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)) = i.removeNth fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)

Tactic:
by

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ motive s hs

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
l : List α
⊢ List.foldl (fun x y ↦ op y x) b l = List.foldl op b l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = op (fold op b s) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p

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 : α p
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f p x) = p.removeNth 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)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f (p.succAbove i) x) = update (p.removeNth f) i x

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
⊢ range (p.insertNth x f) = Set.insert x (range f)

Tactic:
by

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 β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))

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
f : (i : Fin n) → α (p.succAbove i)
⊢ update (p.insertNth x f) p y = p.insertNth y f

Tactic:
by

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

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 α
⊢ ∀ (a : α) (s : Multiset α),
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (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)
x : α p
i : Fin n
y : α (p.succAbove i)
f : (j : Fin n) → α (p.succAbove j)
⊢ p.insertNth x (update f i y) = update (p.insertNth x f) (p.succAbove i) y

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ motive s hs

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ (fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f) = f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : (i : Fin (n + 1)) → α i
⊢ (fun f ↦ p.insertNth f.1 f.2) ((fun f ↦ (f p, p.removeNth f)) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
this : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
by

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 a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
⊢ (insertNthEquiv α 0).symm = (consEquiv α).symm

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_3
⊢ insertNthEquiv (fun x ↦ α) (last n) = snocEquiv fun x ↦ α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ⇑g) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : Set.InjOn g ↑s
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ fold op b f s = fold op b g s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
⊢ c <+ insertionSort r l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Fintype ↑s
f : α → β
inst✝ : Fintype ↑(f '' s)
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (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
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ univ.Infinite ↔ Infinite α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
⊢ l₁ <+ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
⊢ ∃ a ∈ s, a ∉ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₂ ⊆ l₁

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
⊢ ∃ a, a ∉ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a ?m.42

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x ↦ c) s = if s = ∅ then b else op b c

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) ⊆ s ∧
    (Finset.map (Embedding.subtype fun x ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))).card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r b c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ decide (r a c) = true

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite

Tactic:
by

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

Goal state before:
pp: m✝ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j✝ : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m j : ℕ
hm : j < n - m
⊢ j < n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b : α
⊢ (decide (r a b) || decide (r b a)) = true

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
by

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

Goal state before:
pp: m✝¹ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m✝ m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
⊢ 0 < m + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l'

Tactic:
by

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

Goal state before:
pp: m✝¹ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m✝ m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
hnm : ¬p ⟨n - (m + 1), ⋯⟩
⊢ ∀ (j : ℕ) (hm : j < n - m), ¬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✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise r (l.merge l' fun x1 x2 ↦ decide (r x1 x2))

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (range f).Infinite

Tactic:
by

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

Goal state before:
pp: m✝ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - 0), ¬p ⟨j, ⋯⟩
x✝ : ∃ k, p k
val✝ : ℕ
isLt✝ : val✝ < n
h✝ : p ⟨val✝, isLt✝⟩
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x ↦ m (f x)) s = m (fold op b f s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ decide (r x✝² x✝¹) = true → decide (r x✝¹ x✝) = true → decide (r x✝² x✝) = true

Tactic:
by

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

Goal state before:
pp: m n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
⊢ ∀ (j : ℕ) (hm : j < n - n), ¬p ⟨j, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), (decide (r a b) || decide (r b a)) = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ Pairwise r (l.mergeSort fun x1 x2 ↦ decide (r x1 x2))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLE ↔ Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedGE ↔ Pairwise (fun x1 x2 ↦ x1 ≥ x2) l

Tactic:
by

Goal state after: