mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : Option α → M
s : Finset α
⊢ ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ map Embedding.some (eraseNone s), Option.elim' 1 f x = ∏ x ∈ s.erase none, Option.elim' 1 f x

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∀ (z : γ × α), (z ∈ s.biUnion fun x ↦ map (Embedding.sectR x α) (t x)) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Tactic:
by

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

Goal state before:
pp: κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : Fintype ι
⊢ ∀ (x : (i : ι) × κ i), x ∈ univ.sigma fun x ↦ univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
_hx : x ∈ univ
⊢ p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
_hx : x ∈ univ
⊢ ¬p ↑x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ f <$> x <*> g <$> y = ((fun x ↦ x ∘ g) ∘ f) <$> x <*> y

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑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
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
⊢ (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x, f ↑x ⋯) * ∏ x, g ↑x ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
⊢ (fun x ↦ pure f <*> x) = fun x ↦ 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
f g : ι → M
⊢ (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x

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
⊢ p1 = p2

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
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, g ↑i ⋯

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
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, 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
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
⊢ s1 = s2

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (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
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, 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 ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : [].length = n.succ
⊢ cons (head ⟨[], h⟩) (tail ⟨[], h⟩) = ⟨[], h⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
p : α → Prop
n m : ℕ
l₁ : List α
h₁ : l₁.length = n
l₂ : List α
h₂ : l₂.length = m
⊢ (l₁ ++ l₂).length = n + m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β
l : List α
h : l.length = n
⊢ (List.map f l).length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : (a : α) → p a → β
l : List α
h : l.length = n
hp : ∀ (x : α), x ∈ toList ⟨l, h⟩ → p x
⊢ (List.pmap f l hp).length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → φ
x : List α
property✝¹ : x.length = n
y : List β
property✝ : y.length = n
⊢ (zipWith f x y).length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.drop i l).length = n - i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.take i l).length = min i n

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 ι
a : ι
b : (x : ι) → a = x → M
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

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
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ F1 = F2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (l.eraseIdx ↑i).length = n - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → σ → σ × β
x : List α
px : x.length = n
c : σ
res : σ × List β := List.mapAccumr f x c
⊢ res.snd.length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → σ → σ × φ
x : List α
px : x.length = n
y : List β
py : y.length = n
c : σ
res : σ × List φ := List.mapAccumr₂ f x y c
⊢ res.snd.length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ n - i + min n i = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ min n i + min (n - i) n = n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n m : ℕ
v : Vector α m
⊢ (drop n v).toList = List.drop n v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n m : ℕ
v : Vector α m
⊢ (take n v).toList = List.take n v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < n
⊢ i < v.toList.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < v.toList.length
⊢ i < n

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 ι
a : ι
b : (x : ι) → x = a → M
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b 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 ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if a = x then b x else 1) = b a

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 ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if x = a then b x else 1) = b a

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : (fun {α} ↦ η.app α) = fun {α} ↦ η'.app α
⊢ η = η'

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} ↦ η.app α) x = (fun {α} ↦ η'.app α) x
⊢ (fun {α} ↦ η.app α) = fun {α} ↦ η'.app α

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} ↦ η.app α) (x <$> y) = x <$> (fun {α} ↦ η.app α) y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
⊢ (fun {α} ↦ η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} ↦ η.app α

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
⊢ ∀ {α : Type u} (x : α), id (pure x) = pure x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ id (x <*> y) = id x <*> id y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝² : Applicative F
G : Type u → Type w
inst✝¹ : Applicative G
H : Type u → Type s
inst✝ : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ : Type u
x : α✝
⊢ (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) (pure x)) = pure x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝² : Applicative F
G : Type u → Type w
inst✝¹ : Applicative G
H : Type u → Type s
inst✝ : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) (x <*> y)) =
    (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) x) <*> (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) y)

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 t : Finset ι
f g : ι → M
⊢ ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g 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
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f 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
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (x : α ⊕ β), x ∈ univ.disjSum univ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toLeft = univ ↔ map Function.Embedding.inl univ ⊆ u

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toRight = ∅ ↔ u ⊆ map Function.Embedding.inl univ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
u : Finset (α ⊕ β)
⊢ u.toRight = univ ↔ map Function.Embedding.inr univ ⊆ u

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
u : Finset (α ⊕ β)
⊢ u.toLeft = ∅ ↔ u ⊆ map Function.Embedding.inr univ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ univ.toLeft = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ univ.toRight = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
x✝ : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)

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 : ι
f : ι → M
h : i ∉ s → f i = 1
⊢ ∏ x ∈ s, f x = f i * ∏ 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
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ i ∉ s → f i = 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 ι
i : ι
h : i ∈ s
f : ι → M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ = (image b univ).erase k

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
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i ↦ b ↑i) univ ⊂ image b univ

Tactic:
by

Goal state after: