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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (hd :: tl)[ix + 1]?

pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)

Tactic:
]

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (hd :: tl)[ix + 1]?

α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snoc x x₀ ≍ snoc x x₀

Tactic:
]

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ 0 < ix + 1

Tactic:
]

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ 0 < ix + 1
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
]

Goal state after:
case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
i : Fin n
hx₀ : ¬x i ∈ Set.range x
h : x i = x₀
⊢ i.castSucc = last n
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ hd :: tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'

Tactic:
← List.singleton_append

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ [hd] ++ tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ [hd] ++ tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'

Tactic:
]

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ [hd] ++ tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
]

Goal state after:
case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
j : Fin n
hx₀ : ¬x j ∈ Set.range x
h : x₀ = x j
⊢ last n = j.castSucc
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ (take (f 0).succ l')[f 0] ∈ take (f 0 + 1) l'

Tactic:
]

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ (take (f 0).succ l')[f 0] ∈ take (f 0 + 1) l'
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ x = x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False

Tactic:
]

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False
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, Set.range ⇑f ⊆ ↑s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s
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:
rw [← Fintype.card_coe] at h
  rcases nonempty_of_card_le h with ⟨f⟩
  exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩

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

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

Tactic:
]

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 ≠ Set.univ

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ s ≠ Set.univ
Module: Mathlib.Data.List.NodupEquivFin

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

Tactic:
]

Goal state after:
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ Classical.choose ⋯ = Classical.choose ⋯

Tactic:
]

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ n = n

Tactic:
]

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
]

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : ∃ h, l'[f i] = l[i]
⊢ f i < l'.length

Tactic:
]

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : ∃ h, l'[f i] = l[i]
⊢ f i < l'.length
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : n + 1 ≤ n
c : #s = n + 1
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : n + 1 ≤ n
c : #s = n + 1
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
]

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
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:
]

Goal state after:
α : 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
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
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l
Module: Mathlib.Data.List.Sort

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

pp: case cons.h
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b

Tactic:
]

Goal state after:
case cons.h
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b
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
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m
Module: Mathlib.Data.Set.Finite.Basic

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

pp: α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ Fintype ↑s

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi⟩ < ⟨j, hj⟩

Tactic:
]

Goal state after:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi⟩ < ⟨j, hj⟩
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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)
⊢ ⋯ ▸ p (j.castPred ⋯) = ⋯ ▸ p (j.castPred ⋯)

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ orderedInsert s (f x) (insertionSort s (map f xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

pp: case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

pp: case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))

Tactic:
]

Goal state after:
case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))
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)
⊢ ⋯ ▸ p (j.pred ⋯) = ⋯ ▸ p (j.pred ⋯)

Tactic:
]

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

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

Tactic:
]

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 ↑(s ∩ t)

Tactic:
]

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑(s ∩ t)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
]

Goal state after:
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m x_1, x = l.get n ∧ x = l.get m
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:
]

Goal state after:
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, ⋯⟩
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)
j : Fin n
⊢ p j ≍ cast ⋯ (p j)

Tactic:
]

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ cast ⋯ (p j)
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
]

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)
j : Fin n
⊢ j.castSucc = j.castSucc

Tactic:
]

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 ↑{x | x ∈ s ∧ x ∈ t}

Tactic:
]

Goal state after:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
]

Goal state after:
α : Type u
s t : Set α
hs : Finite ↑s
ht : Finite ↑t
⊢ (s ∪ t).Finite
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
]

Goal state after:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite
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
⊢ (f '' f ⁻¹' s).Finite

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' f ⁻¹' s).Finite
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:
simp [hc.comm]

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:
simp [hc.comm]

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 (op b a) s = fold op (op b a) s

Tactic:
]

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 (op a b) s = fold op (op a b) s

Tactic:
]

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₁ = op (fold op b₁ s₁) b₂

Tactic:
← fold_cons'_right,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂
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 b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)

Tactic:
]

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)
⊢ op (fold op b₁ s₁) (op a (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))

Tactic:
]

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))
⊢ op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
    op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a)))

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
]

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
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₁) (fold op b₂ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
]

Goal state after: