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

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α n.succ
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
property✝ : [].length = n
⊢ (tail ⟨[], property✝⟩).toList = (toList ⟨[], property✝⟩).tail

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
n : ℕ
f : α → β
x : Sym α n
⊢ (Multiset.map f ↑x).card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
head✝ : α
tail✝ : List α
property✝ : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, property✝⟩).toList = (toList ⟨head✝ :: tail✝, property✝⟩).tail

Tactic:
by

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

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x ↦ x) s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]

Tactic:
by

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

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ ¬v.toList.isEmpty = true

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a b : α
f : α → β
m : Multiset α
hc : m.card = n
⊢ (Multiset.map f m).card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ (map id v).toList = v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ v.toList.Nodup ↔ Function.Injective v.get

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
v : Vector α n
⊢ v.toList.reverse.length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ v.reverse.reverse = v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
⊢ map (⇑e.symm) (map (⇑e) x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).head = f 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (a ::ᵥ v).get 0 = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).get i.succ = v.get i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.head = v.last

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (List.scanl f b v.toList).length = n + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map (⇑e) (map (⇑e.symm) x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
⊢ scanl f b nil = b ::ᵥ nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ v = nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
⊢ (↑s).attach.card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (scanl f b v).head = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ (↑s + ↑s').card = n + n'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ s.append s' = (Sym.cast ⋯) (s'.append s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
⊢ {a}.card = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
l l' : { x // x.length = 1 }
⊢ (Subtype.instSetoid_mathlib fun x ↦ x.length = 1) l l' ↔ (List.isSetoid α) ↑l ↑l'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
l : { x // x.length = 1 }
⊢ 0 < (↑l).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
x✝¹ x✝ : { x // x.length = 1 }
val✝¹ : List α
property✝ : val✝¹.length = 1
val✝ : List α
h : val✝.length = 1
perm : ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩
⊢ (↑⟨val✝¹, property✝⟩).head ⋯ = (↑⟨val✝, h⟩).head ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b, f b = f true * f false

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
by

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

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i ↦ pure (f i)) = pure (ofFn f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x, f x = f a * f b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
⊢ RightInverse
    (fun s ↦
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯) s).liftOn
        (fun l ↦ (↑l).head ⋯) ⋯)
    fun a ↦ ⟨{a}, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f i = f a * ∏ i, f ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : (i : ι) → Finset (α i)
⊢ #(piFinset s) = ∏ i, #(s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
n : ℕ
v : Vector α n
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C v

Tactic:
by

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

Goal state before:
pp: α : Type u_7
s : Finset α
n : ℕ
⊢ #(piFinset fun x ↦ s) = #s ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (↑m).card < n + 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ j, #(Function.update s i {a} j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (filter (fun x ↦ a ≠ x) ↑m).card + ↑⟨count a ↑m, ⋯⟩ = (↑m).card

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ ↑m₁.fst = ↑m₂.fst

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
⊢ #(Function.update s i {a} j) = Function.update (fun j ↦ #(s j)) i 1 j

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ ∏ j, Function.update (fun j ↦ #(s j)) i 1 j = ∏ j ∈ univ.erase i, #(s j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ j ∈ univ.erase i, #(s j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ ∏ j ∈ univ.erase i, #s = #s ^ (card ι - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
⊢ #({f ∈ piFinset s | f i = a}) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then ∏ b ∈ univ.erase i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (List.Vector α n) = Fintype.card α ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ map (⇑e.symm) (map (⇑e) l) = l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map (⇑e) (map (⇑e.symm) l) = l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
j : Fin s
⊢ ↑j < a.length

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C u v w

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (fun j ↦ a.get ⟨↑j, ⋯⟩) ∈ univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
· exact fun a ha ha' => h <| ha'.symm ▸ ha

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : a ∉ s
⊢ count a ↑(fill a i s) = ↑i

Tactic:
simp [coe_fill, coe_replicate, hx]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : a ∉ s
⊢ count a ↑(fill a i s) = ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length = a.length

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ((↑v).insertIdx (↑i) a).length = n + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ decodeList 0, encodeList a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ ∀ (n : ℕ) (h₁ : n < (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length) (h₂ : n < a.length),
    (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).get ⟨n, h₁⟩ = a.get ⟨n, h₂⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
⊢ decode (encode s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ #(image List.ofFn univ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #(image List.ofFn univ) = Fintype.card α ^ s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ofNat (List α) 0 = []

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
u : List α
⊢ ((fun n ↦ replicate n default) u.length).length = u.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : Fin n), f ↑x = f ↑((equivSubtype.trans (Equiv.subtypeEquivRight ⋯)) x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i, f ↑i = ∏ i ∈ range n, f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n ⊕ Sym α n.succ
⊢ encode (decode s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default x : α
hx : x ∈ s
⊢ enumerateCountable h default (encode ⟨x, hx⟩) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable h default) ⊆ insert default s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable h default n ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
s : Set α
h : s.Countable
⊢ ∃ f, s ⊆ range f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
⊢ ¬univ.Countable ↔ Uncountable α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
⊢ ∃ f, s = range f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (f '' s).Countable

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i, c i = ∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Set.image2 f s t)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.UnivLE

Goal state before:
pp: ⊢ ¬UnivLE.{u + 1, u}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a, f ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | ¬p x} ↔ ¬p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ a, dite (p a) (f a) (g a) = (∏ a, f ↑a ⋯) * ∏ a, g ↑a ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ eraseIdx (⟨j, hj⟩.succAbove ⟨i, hi⟩) (insertIdx a ⟨j, hj⟩ v) =
    insertIdx a (⟨i, hi⟩.predAbove ⟨j, hj⟩) (eraseIdx ⟨i, hi⟩ v)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ (⋃ i, t i).Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i ⟨l, hl⟩) = insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
v : Vector α n
i : Fin n
a : α
⊢ ((↑v).set (↑i) a).length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).get i = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
⊢ (⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable

Tactic:
by

Goal state after: