mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Nonempty (α ≃ ↥t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
⊢ (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∀ x ∈ s \ {i}, f x = ?m.47 x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ #({i ∈ s | p i}) = ∑ i ∈ s, if p i then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (∏ i, if p i then a else 1) = if ∃ i, p i then a else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (∏ i, if p i then a else 1) = if ∃ i, p i then a else 1

Tactic:
by
  simp [prod_ite_one univ p (by simpa using h)]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (∏ j, if h : i = j then f j h else 1) = f i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (∏ j, if h : j = i then f j h else 1) = f i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p2, seq := s2, seqLeft := sl2, seqRight := sr2 }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if i = j then f j else 1) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if j = i then f j else 1) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : α
⊢ (f <$> pure x).run = (pure (f x)).run

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : Comp F G (α → β)
x : α
⊢ (f <*> pure x).run = ((fun g ↦ g x) <$> f).run

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
x : Comp F G α
f : Comp F G (α → β)
g : Comp F G (β → γ)
⊢ (g <*> (f <*> x)).run = (Function.comp <$> g <*> f <*> x).run

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : Comp F G α
⊢ (pure f <*> x).run = (f <$> x).run

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x <* y = const β <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x *> y = const α id <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ Prod.mk <$> x✝¹ <*> x✝ = (fun b a ↦ (a, b)) <$> x✝ <*> x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : Const α α✝
x✝ : Const α β✝
⊢ x✝¹ <* x✝ = Function.const β✝ <$> x✝¹ <*> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : Const α α✝
x✝ : Const α β✝
⊢ x✝¹ *> x✝ = Function.const α✝ id <$> x✝¹ <*> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : α✝ → β✝
x✝ : Const α α✝
⊢ pure x✝¹ <*> x✝ = x✝¹ <$> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : Const α (α✝ → β✝)
x✝ : α✝
⊢ x✝¹ <*> pure x✝ = (fun h ↦ h x✝) <$> x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ γ✝ : Type u_2
x✝² : Const α α✝
x✝¹ : Const α (α✝ → β✝)
x✝ : Const α (β✝ → γ✝)
⊢ x✝ <*> (x✝¹ <*> x✝²) = Function.comp <$> x✝ <*> x✝¹ <*> x✝²

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α α✝
x✝ : AddConst α β✝
⊢ x✝¹ <* x✝ = Function.const β✝ <$> x✝¹ <*> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α α✝
x✝ : AddConst α β✝
⊢ x✝¹ *> x✝ = Function.const α✝ id <$> x✝¹ <*> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : α✝ → β✝
x✝ : AddConst α α✝
⊢ pure x✝¹ <*> x✝ = x✝¹ <$> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α (α✝ → β✝)
x✝ : α✝
⊢ x✝¹ <*> pure x✝ = (fun h ↦ h x✝) <$> x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type u_2
x✝² : AddConst α α✝
x✝¹ : AddConst α (α✝ → β✝)
x✝ : AddConst α (β✝ → γ✝)
⊢ x✝ <*> (x✝¹ <*> x✝²) = Function.comp <$> x✝ <*> x✝¹ <*> x✝²

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
⊢ Finset.image f s' ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ InjOn f ↑s'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ {t | t ⊆ s} = s.powerset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s.powerset = univ ↔ s = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ {s | #s = k} = powersetCard k univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ card { s // #s = k } = (card α).choose k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map coeEmb.toEmbedding Finset.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Finite (Set α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h : ∀ (m : Fin n), get ⟨v, hv⟩ m = get ⟨w, hw⟩ m
⊢ (↑⟨v, hv⟩).length = (↑⟨w, hw⟩).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Fin 0 → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (ofFn f).toList = List.ofFn f

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ p a

Tactic:
exact hp.1

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ p a

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ ∀ (x : α), x ∈ v.toList → p x

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
ha : p a
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
⊢ (map f v).toList = List.map f v.toList

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).tail = map f v.tail

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : ℕ
hi : i < n
⊢ (map f v)[i] = f v[i]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).toList = List.pmap f v.toList hp

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head ∈ v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).head = f v.head ⋯

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 : α
s : Sym α n
⊢ (a ::ₘ ↑s).card = n.succ

Tactic:
by

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

Goal state before:
pp: α : Sort u
⊢ Uncountable α ↔ IsEmpty (α ↪ ℕ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (mk s hs)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α ⊕ β)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α × β)

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∃ s, p s) ↔ ∃ s, ∃ (hs : s.card = n), p (mk s hs)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Uncountable α
inst✝ : Nonempty β
⊢ Uncountable (α × β)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : Uncountable β
⊢ Uncountable (α × β)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty β
h : Countable (α × β)
⊢ Countable α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ↑(a ::ₛ ofVector v) = ↑(ofVector (a ::ᵥ v))

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty α
h : Countable (α × β)
⊢ Countable β

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Sigma π)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : ∀ (a : α), Uncountable (π a)
⊢ Uncountable (Sigma π)

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 α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (m.erase a).card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).tail = pmap f v.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 : α✝
α : Type u_3
n : ℕ
x✝ : List α
⊢ x✝.length = n ↔ Multiset.card ⟦x✝⟧ = n

Tactic:
by

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
⊢ Countable (Fin n → ℕ)

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
i : ℕ
hi : i < n
⊢ v[i] ∈ v.toList

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 : α✝
α : Type u_3
n : ℕ
x✝¹ x✝ : { l // l.length = n }
⊢ (Vector.Perm.isSetoid α n) x✝¹ x✝ ↔ (List.isSetoid α) ↑x✝¹ ↑x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ (a :: symEquivSym' s) = symEquivSym' (a ::ₛ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
i : ℕ
hi : i < n
⊢ (pmap f v hp)[i] = f v[i] ⋯

Tactic:
by

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable ((a : α) → π a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).get i = f i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

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 : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ ↑i + 1 < n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
⊢ m.card = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h : a ∈ s
⊢ ∃ t, s = a ::ₛ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ x.tail.get i = x.get ⟨↑i + 1, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).get ⟨i, h⟩ = get ⟨a :: l, e⟩ ⟨i, h⟩.succ

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✝ : Subsingleton α
n : ℕ
⊢ ∀ (a b : Sym α n), a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ ofFn (ofFn f).tail.get = ofFn fun i ↦ f i.succ

Tactic:
by

Goal state after: