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

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = replicate (n + 1) c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ Injective p.succAbove

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #t - #s

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ a.succAbove 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ (ofFn fun i ↦ ofFn fun j ↦ Fin.repeat n a ⟨↑i * m + ↑j, ⋯⟩).flatten = (ofFn fun x ↦ ofFn a).flatten

Tactic:
Fin.repeat,

Goal state after:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ (ofFn fun i ↦ ofFn fun j ↦ a ⟨↑i * m + ↑j, ⋯⟩.modNat).flatten = (ofFn fun x ↦ ofFn a).flatten
Module: Mathlib.Data.Finset.Card

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) + #s = #t

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #s ≤ #(t \ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #s ≤ #(s \ t) + #t

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (last n).succAbove = castSucc

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : #s < #t
⊢ (t \ s).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) ≤ #(t \ s) ↔ #s ≤ #t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) < #(t \ s) ↔ #s < #t

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) = #(t \ s) ↔ #s = #t

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.succ ≤ p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #(t ∪ u) ≤ #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
⊢ (t ∩ u).Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p < i.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ s ⊆ t ∧ t ⊆ t ∧ #t = #t

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
⊢ 0 < p.succAbove i

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Fin n
y : Fin (n + 1)
h : x.castSucc < y
h' : y.succAbove x ≠ last n
⊢ (y.succAbove x).castPred h' = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ x.castSucc
h' : y.succAbove x ≠ 0
⊢ (y.succAbove x).pred h' = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, y.succAbove z = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
⊢ (∃ z, x.succAbove z = y) → y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
⊢ f ⟨i, ⋯⟩ = b

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Set.range succ = {0}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
j : Fin n
hj : j < ⟨i, ⋯⟩
⊢ ¬p (f j) = true

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
⊢ (ofFn f)[↑i] = b

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ j < n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ (u \ s).Nonempty

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ ⟨j, ⋯⟩ < i

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ (!p (ofFn f)[j]) = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ s ⊆ u.erase a ∧ u.erase a ⊆ t ∧ #(u.erase a) = k

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ find? p (ofFn f) = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
i : Fin n
h : Function.Injective f
⊢ find? p (ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ f ≍ g

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ succAbove 1 1 = 2

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α : Fin 0 → Sort u
⊢ Unique ((i : Fin 0) → α i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove i.succ = i.succ.castPred ⋯

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ tail (cons x p) = p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃ a, s = {a}

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ count a (finRange n) = 1

Tactic:
by

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

Goal state before:
pp: k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃! a, a ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p < i
⊢ p.predAbove i.castSucc = i.castSucc.pred ⋯

Tactic:
by

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = p 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ #(t \ s) = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ⇑σ) ~ ofFn f

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = p (last n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ (p.pred hp).predAbove i = i.pred ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ Nonempty (Fintype α)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (finRange n).toFinset = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
⊢ Multiset.map f univ.val = ↑(List.ofFn f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
f : Fin n → α
⊢ image f univ = (List.ofFn f).toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n ↪ α
⊢ map f univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ image i.succAbove univ = {i}ᶜ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ image castSucc univ = {last n}ᶜ

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

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

Goal state before:
pp: n : ℕ
⊢ image castSucc univ = {last n}ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ 0 ∉ map { toFun := succ, inj' := ⋯ } univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ } univ) ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ last n ∉ map castSuccEmb univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons (last n) (map castSuccEmb univ) ⋯

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) = update (cons x p) i.succ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ univ = Finset.cons p (map p.succAboveEmb univ) ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ image l.get univ = l.toFinset

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun i ↦ f l[↑i]) univ = (List.map f l).toFinset

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hp : p ≠ last n
⊢ (p.castPred hp).predAbove i = i.castPred ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun x ↦ f (l.get x)) univ = (List.map f l).toFinset

Tactic:
by

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

Goal state before:
pp: a b : Fin 2
⊢ a = b → (a = 0 ↔ b = 0)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α
hx : x ∈ s
h : ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s = {x}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ (↑s).Subsingleton

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝ : Decidable p
x✝ : PLift p
h : p
⊢ { down := h } ∈ if h : p then {{ down := h }} else ∅

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z = cons z p

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝¹ : Decidable p
α : p → Type u_4
inst✝ : (hp : p) → Fintype (α hp)
hp : ¬p
h : (hp : p) → α hp
x : p
⊢ h x = ⋯.elim

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
⊢ predAbove 0 i = i.pred hi

Tactic:
by

Goal state after: