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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
s : Multiset α
l : List α
h : ∃ x, x ∈ ⟦l⟧
x✝ : ∃ x, x ∈ ⟦[]⟧
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
j : Fin (n + 1)
h : j ≠ 0
⊢ (predAbove 0 j).succ = j

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.8
inst✝¹ : Nonempty α
inst✝ : Fintype α
⊢ ∃ x, x ∈ univ.val

Tactic:
by

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

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

Tactic:
by

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
α : Fin (n + 1) → Type u_1
f : α 0 × ((i : Fin n) → α i.succ)
⊢ (fun f ↦ (f 0, tail f)) ((fun f ↦ cons f.1 f.2) f) = f

Tactic:
by

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 = univ.val

Tactic:
by

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
⊢ y ∈ {x}

Tactic:
by

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
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
⊢ (fun f ↦ cons f.1 f.2) ((fun f ↦ (f 0, tail f)) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∀ x ∈ ∅, P x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  split_ifs with hi
  · rw [hi, predAbove_right_zero]
  · rw [predAbove_zero_of_ne_zero hi]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ Nonempty α

Tactic:
by

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 (Fin.cons (x 0) (tail x)) = motive x

Tactic:
rw [cons_self_tail]

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

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

Tactic:
by

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 (Fin.cons (x 0) (tail x)) = motive x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
← exists_castSucc_eq

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.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ #s ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
by

Goal state after:
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
⊢ consCases cons (Fin.cons x₀ x) = cons x₀ x

Tactic:
by

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
α : Sort u_1
motive : {n : ℕ} → (Fin n → α) → Sort v
elim0 : motive Fin.elim0
cons : {n : ℕ} → (x₀ : α) → (x : Fin n → α) → motive x → motive (Fin.cons x₀ x)
x : Fin 0 → α
⊢ motive x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
⊢ #(t \ image f s) = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
⊢ Surjective p.predAbove

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
by

Goal state after:
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'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ ¬x₀ ∈ Set.range x ∧ Injective x

Tactic:
by

Goal state after:
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'
⊢ ∀ (n : ℕ), P (f n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
⊢ tail (update q 0 z) = tail q

Tactic:
by

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)
h : 1 < #s
⊢ ∃ i, 1 < #(image (fun x ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
⊢ #∅ = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = ∅ ∧ #t = n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ : Finset α
n : ℕ
a : α
s : Finset α
x✝² : a ∉ s
x✝¹ : #s = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
x✝ : #(cons a s x✝²) = n + 1
⊢ ∃ (h : a ∉ s), cons a s h = cons a s x✝² ∧ #s = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
x✝ : ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
a : α
t : Finset α
w✝ : a ∉ t
hs : cons a t w✝ = s
right✝ : #t = n
⊢ #s = n + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
inst✝ : DecidableEq α
h : #s = n + 1
a : α
has : a ∈ s
⊢ #(s.erase a) = n

Tactic:
by

Goal state after:
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
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
⊢ g ∘ tail q = tail (g ∘ q)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
j : Fin n
⊢ q j.succ ≤ cons x p j.succ ↔ tail q j ≤ p j

Tactic:
by

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
⊢ (∀ (i : Fin n), cons x₀ x i.succ ≤ cons y₀ y i.succ) ↔ x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
by

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

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

Tactic:
by

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
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin m
⊢ m ≤ m + n

Tactic:
by

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
by

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
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β

Tactic:
by

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

Goal state before:
pp: α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ #univ ≤ #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ → #s = Fintype.card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #(univ \ s) = Fintype.card α - #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #sᶜ + #s = Fintype.card α

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ S₂ ⊆ S₁ᶜ

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ #S₁ᶜ ≤ #S₂

Tactic:
by

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
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ card ↑Set.univ = card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ card { _a // True } = card α

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ map { toFun := f, inj' := h } univ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ Set.MapsTo f ↑univ ↑univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ #univ = #univ + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ ∃! x, x ∉ image f univ

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
a : α
⊢ f a ∈ Set.range f

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a ↦ ⟨f a, ⋯⟩) a = ⟨val✝, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = 0 ↔ IsEmpty α

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ {a, b, c} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ {a, b, c} = {a, b, c}

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ #{x | p x} = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Injective f ↔ Bijective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ append x₀ x = cons (x₀ 0) x ∘ Fin.cast ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ Set.range Subtype.val

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
⊢ cons x xs = append (cons x elim0) xs ∘ Fin.cast ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidablePred p
⊢ card { x // p x } = #{x | p x}

Tactic:
by

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
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
by

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
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m

Tactic:
by

Goal state after: