mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b ≤ a ↔ b ≤ a

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ ↑a ≤ ↑a

Tactic:
]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a < b ↔ a < b

Tactic:
]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ a ≤ b ↔ a ≤ b

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ ↑a ≤ ↑a

Tactic:
]

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * ↑i + m

Tactic:
]

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

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑((a - b).castLT ⋯)

Tactic:
]

Goal state after:
n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑((a - b).castLT ⋯)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m

Tactic:
]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m

Tactic:
]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
⊢ [] = []

Tactic:
]

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i ↦ (a :: l).get i.succ) = a :: l

Tactic:
]

Goal state after:
α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i ↦ (a :: l).get i.succ) = a :: l
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ i = i

Tactic:
]

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ i = i

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List α
f : α → β
⊢ map f l = map f l

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p

Tactic:
]

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p

Tactic:
]

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
c : α
⊢ [] = []

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: ofFn fun x ↦ c
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
]

Goal state after:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j
Module: Mathlib.Data.Finset.Card

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
]

Goal state after:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j
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
⊢ #(t \ s) = #t - #s

Tactic:
]

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #t - #s
⊢ #(t \ s) = #t - #s
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:
]

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

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

pp: case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
Module: Mathlib.Data.Finset.Card

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

pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t

Tactic:
]

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

α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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)
⊢ b = last n ↔ b = last n

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ i.castSucc = i.castSucc

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ i.castSucc < p

Tactic:
]

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ i.castSucc < p
Module: Mathlib.Data.Finset.Card

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

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Tactic:
]

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (Fin.cons a f 0 :: ofFn fun i ↦ Fin.cons a f i.succ) = a :: ofFn f
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc

Tactic:
]

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #s = #s

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < i.succ

Tactic:
]

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < i.succ
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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
⊢ x.castSucc = x.castSucc

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true) ↔
    p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
⊢ j.succ.succ = j.succ.succ

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ.castSucc = j.succ.castSucc

pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ ≤ i

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ ≤ i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ.castSucc = j.succ.castSucc

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc.castSucc = j.castSucc.castSucc

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

Goal state after:
n : ℕ
j : Fin n
this : succAbove 1 j.succ = j.succ.succ
⊢ succAbove 1 j.succ = j.succ.succ
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯).Nodup

Tactic:
]

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯).Nodup
Module: Mathlib.Data.List.FinRange

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

pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Tactic:
· intro _
    exact Function.injective_of_subsingleton _

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
]

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (Fin.cons x₀ xs 0 :: ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
nodup_cons,

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬Fin.cons x₀ xs 0 ∈ ofFn fun i ↦ xs i) ∧ (ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n

Tactic:
]

Goal state after:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n
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 = cons x p (succ 0)

Tactic:
]

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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)) = cons x p (last n).succ

Tactic:
]

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = cons x p (last n).succ
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
⊢ i.castPred ⋯ = i.castPred ⋯

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↥s

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x = x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = map (⇑e) univ.val

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ last n = last n

Tactic:
]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x : (i : Fin n.succ) → α i
⊢ motive x = motive x

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i = i

Tactic:
]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
]

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cons (Fin.cons x₀ x 0) (tail (Fin.cons x₀ x)) = cons x₀ x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ last n = last n

Tactic:
]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ i.castPred hi = i.castPred hi

Tactic:
]

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

Goal state before:
pp: case neg
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ a, p.predAbove a = i

Tactic:
]

Goal state after:
case neg
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : i < p.castSucc
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : i < p.succ
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (Classical.choose ⋯)

Tactic:
]

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (Classical.choose ⋯)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
p i : Fin n
h : i < p
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ b = b

Tactic:
]

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ ∃ x ∈ s, ¬x i = ai

Tactic:
]

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ ∃ x ∈ s, ¬x i = ai
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i

Tactic:
]

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ b.succ.castPred ⋯ = b.succ.castPred ⋯

Tactic:
]

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

Goal state before:
pp: case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0

Tactic:
]

Goal state after:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (Classical.choose ⋯)

Tactic:
]

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (Classical.choose ⋯)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (q j') = g (q j')

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
]

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ b.castSucc.pred ⋯ = b.castSucc.pred ⋯

Tactic:
]

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ insert x (Set.range b) = insert x (Set.range b)

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ b = b

Tactic:
]

Goal state after: