mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 7 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
⊢ ∏ _i, x = x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
⊢ ∏ i, f (Fin.cast h i) = ∏ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
x✝ : a ≡ b [PMOD n • p]
k l : ℕ
h : k • n • p + a = l • n • p + b
⊢ (k * n) • p + a = (l * n) • p + b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ↑↑s → R
hfg : ∑ i, f i • v ↑i = ∑ i, g i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ s, (if hj : i ∈ s then f ⟨i, hj⟩ else 0) • v i = ∑ i ∈ s, (if hj : i ∈ s then g ⟨i, hj⟩ else 0) • v i

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ f 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ i, f i = (∏ i, f (castAdd b i)) * ∏ i, f (natAdd a i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i, (f ∘ Subtype.val) i • (v ∘ Subtype.val) i = ∑ i, (g ∘ Subtype.val) i • (v ∘ Subtype.val) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
t : Finset ↑s
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) ⊆ s

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i, f i = ∏ i, f (castAdd b i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ n • a ≡ n • b [PMOD n • p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
h : 0 < n + 1
x : M
p : Fin n → M
⊢ ∏ j, ⟨0, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
t : Finset ↑s
x : ↥t
⊢ ∀ ⦃a₂ : ↥t⦄, (fun x ↦ ⟨↑↑x, ⋯⟩) x = (fun x ↦ ⟨↑↑x, ⋯⟩) a₂ → x = a₂

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
i : ℕ
h : i < 0 + 1
x : M
p : Fin 0 → M
⊢ ∏ j, ⟨i, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
⊢ LinearIndependent R v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ LinearIndepOn R v s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : a ≡ b [PMOD p]
⊢ f a ≡ f b [PMOD f p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : Function.Injective ⇑f
⊢ f a ≡ f b [PMOD f p] ↔ a ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
a b p : M
inst✝ : IsAddTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndependent R (⇑f ∘ v)
⊢ LinearIndependent R v

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x : M
p : Fin (n + 1) → M
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
i : Fin (n + 1)
f : Fin (n + 1) → M
⊢ f i * ∏ j, i.removeNth f j = ∏ j, f j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Icc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Icc a b, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ico (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ico a b, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ioc a b, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : LinearIndependent R (⇑f ∘ v)
⊢ Disjoint (span R (range v)) f.ker

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (v '' s))
⊢ InjOn ⇑f ↑(span R (Set.range fun i ↦ v ↑i))

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioo (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ioo a b, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ uIcc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ uIcc a b, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ ∏ i ≥ Fin.cast h a, f i = ∏ i ≥ a, f (Fin.cast h i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι'
f : ι' → M
s : Set ι
⊢ (fun x ↦ f ↑x) ∘ ⇑(e.image s) = fun x ↦ (f ∘ ⇑e) ↑x

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ ∏ i > Fin.cast h a, f i = ∏ i > a, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ ∏ i ≤ Fin.cast h a, f i = ∏ i ≤ a, f (Fin.cast h i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : LinearIndependent R v
⊢ LinearIndepOn R id (range v)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ ∏ i < Fin.cast h a, f i = ∏ i < a, f (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Icc (castLE h a) (castLE h b), f i = ∏ i ∈ Icc a b, f (castLE h i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ico (castLE h a) (castLE h b), f i = ∏ i ∈ Ico a b, f (castLE h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioc (castLE h a) (castLE h b), f i = ∏ i ∈ Ioc a b, f (castLE h i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioo (castLE h a) (castLE h b), f i = ∏ i ∈ Ioo a b, f (castLE h i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ uIcc (castLE h a) (castLE h b), f i = ∏ i ∈ uIcc a b, f (castLE h i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a : Fin n
⊢ ∏ i ≤ castLE h a, f i = ∏ i ≤ a, f (castLE h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a : Fin n
⊢ ∏ i < castLE h a, f i = ∏ i < a, f (castLE h i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Icc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Icc a b, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Ico (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ico a b, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Ioc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ioc a b, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Ioo (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ioo a b, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ uIcc (castAdd m a) (castAdd m b), f i = ∏ i ∈ uIcc a b, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a : Fin n
⊢ ∏ i ≤ castAdd m a, f i = ∏ i ≤ a, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a : Fin n
⊢ ∏ i < castAdd m a, f i = ∏ i < a, f (castAdd m i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Icc a.castSucc b.castSucc, f i = ∏ i ∈ Icc a b, f i.castSucc

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ico a.castSucc b.castSucc, f i = ∏ i ∈ Ico a b, f i.castSucc

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ioc a.castSucc b.castSucc, f i = ∏ i ∈ Ioc a b, f i.castSucc

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ioo a.castSucc b.castSucc, f i = ∏ i ∈ Ioo a b, f i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ m, m • p = b - a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ uIcc a.castSucc b.castSucc, f i = ∏ i ∈ uIcc a b, f i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ m, b - a = m • p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i ≤ a.castSucc, f i = ∏ i ≤ a, f i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b : G
⊢ 1 • (b - a) + a = 0 • (b - a) + b

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i < a.castSucc, f i = ∏ i < a, f i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p : G
z : ℤ
⊢ -z • p = 0 - z • p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (a + z • p)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Icc a.succ b.succ, f i = ∏ i ∈ Icc a b, f i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (z • p + a)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ico a.succ b.succ, f i = ∏ i ∈ Ico a b, f i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD z • p]
⊢ a ≡ b [PMOD p]

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ioc a.succ b.succ, f i = ∏ i ∈ Ioc a b, f i.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ioo a.succ b.succ, f i = ∏ i ∈ Ioo a b, f i.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ uIcc a.succ b.succ, f i = ∏ i ∈ uIcc a b, f i.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i ≥ a.succ, f i = ∏ i ≥ a, f i.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i > a.succ, f i = ∏ i > a, f i.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i > 0, f i = ∏ j, f j.succ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∏ i, ∏ j, f i j = (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD p]
⊢ z • a ≡ z • b [PMOD z • p]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
p a b : G
z : ℤ
inst✝ : IsAddTorsionFree G
hn : z ≠ 0
⊢ z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a₁ a₂ b₁ b₂ : G
h : a₁ ≡ b₁ [PMOD p]
⊢ a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a₁ a₂ b₁ b₂ : G
h : a₂ ≡ b₂ [PMOD p]
⊢ a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b c : G
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
⊢ LinearIndepOn R g (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b c : G
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : ι → M
h : EqOn v w s
⊢ LinearIndepOn R v s ↔ LinearIndepOn R w s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ a ≡ 0 [PMOD p] ↔ ∃ z, a = z • p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p

Tactic:
by

Goal state after: