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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
by

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

Goal state before:
pp: α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ (mulSupport f).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ i < n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ ⟨i + 2, h⟩ = ⟨i, ⋯⟩.succ.succ

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
⊢ vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1) = vecCons b (vecCons a x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ ↑k - 1 < n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ k = ⟨↑k - 1, ⋯⟩.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) = vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (x : α), f x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
⊢ (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y = ∏ k ∈ s, g k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support fun x ↦ r * f x) = support f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ ∀ (a b : Fin n), a + b = b + a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
⊢ ↑(⟨a, ha⟩ - ⟨b, hb⟩) = ↑(⟨a, ha⟩ + -⟨b, hb⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ (n - ↑⟨a, ha⟩ + a) % n = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a < a - b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a - b ≤ a ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
x : Fin (n + 2)
⊢ x < 1 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support fun x ↦ f x * r) = support f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
simp [fin_one_eq_zero k]

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ ¬k - 1 < k ↔ ¬0 < k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ -last n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ -↑n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (a + b).rev = a.rev - b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (a - b).rev = a.rev + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
ha : ↑a + 1 < n
⊢ a < a + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r

Tactic:
by

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport fun i ↦ f i a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a + b < a ↔ b.rev < a

Tactic:
by

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a
this : {a ∈ s | g a = b}.Nonempty
⊢ b ∈ g '' ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a) ⊆ ↑(image g s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n k : ℕ
h : k < n
⊢ (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ n < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i ↦ cons a v ((finRotate (n + 1)) i)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finRotate n.succ) 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑((finRotate (n + 1)) i) = ↑i + 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i < (finRotate (n + 1)) i ↔ i ≠ Fin.last n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i < (finRotate n.succ) i ↔ i ≠ -1

Tactic:
lt_finRotate_iff_ne_last,

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i ≠ Fin.last n ↔ i ≠ -1
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i < (finRotate n) i ↔ i ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (Equiv.symm (finRotate n)) i = i - 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n)) i = i - 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑((Equiv.symm (finRotate n)) i) = ↑i - 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n)) i < i ↔ i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k : Fin n
⊢ ⇑(finCycle k) = (⇑(finRotate n))^[↑k]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
⊢ ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ (mulSupport fun a ↦ f a ^ count a s) ⊆ ↑s.toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ (map f s).prod = ∏ᶠ (a : α), f a ^ count a s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ (↑b.repr).range = supported R R univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
m : M
⊢ b.repr m ∈ supported R R ↑(b.repr m).support ∧ (linearCombination R ⇑b) (b.repr m) = m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (⇑b '' s)
⊢ ↑(b.repr m).support ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial R
i : ι
s : Set ι
⊢ b i ∈ span R (⇑b '' s) ↔ i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : p = ⊤
⊢ ∀ (i : ι), b i ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
⊢ range ⇑b ⊆ ↑p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
⊢ p = ⊤ ↔ ∀ (i : ι), b i ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
⊢ Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
inst✝² : Semiring R₂
inst✝¹ : Module R₂ M'
inst✝ : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x✝¹ x✝ : M
hab : ((b.constr R₂) v) x✝¹ = ((b.constr R₂) v) x✝
⊢ (linearCombination R v) (b.repr x✝¹) = (linearCombination R v) (b.repr x✝)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
⊢ LinearIndependent R b.coord

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
⊢ (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
⊢ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)

Tactic:
by

Goal state after: