mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ i, f i • v i + ∑ i, g i • v i

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ i, f i • v i + ∑ i, g i • v i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = (RingHom.id R) r • ∑ i, f i • v i

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = (RingHom.id R) r • ∑ i, f i • v i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (Fintype.linearCombination R v) (Pi.single i r) = r • v i

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (Fintype.linearCombination R v) (Pi.single i r) = r • v i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i, (b'.repr x) i • b' i)) i

Tactic:
[

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i, (b'.repr x) i • b' i)) i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ x ∈ span R ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x

Tactic:
by
    rw [mem_span_iff_exists_finset_subset]
    rintro ⟨f, t, hts, hf, rfl⟩
    refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
    simp +contextual [Function.support_subset_iff'.1 hf]

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

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

Tactic:
inter_left_comm

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ #{i | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList

Tactic:
[

Goal state after:
case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ #{i | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
⊢ x ∈ insert a s → x ∈ s
Module: Mathlib.Data.Fin.VecNotation

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

Tactic:
[

Goal state after:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
n i : ℕ
hi : i < n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
[

Goal state after:
case inl
n i : ℕ
hi : i < n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inr
n i : ℕ
hi : i ≥ n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
[

Goal state after:
case inr
n i : ℕ
hi : i ≥ n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1) i

Tactic:
[

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1) i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)

Tactic:
[

Goal state after:
n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1 + 1) i

Tactic:
[

Goal state after:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1 + 1) i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑↑(Fin.ofNat n (a.natMod ↑n)) = a

Tactic:
[

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑↑(Fin.ofNat n (a.natMod ↑n)) = a
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 → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Tactic:
[

Goal state after:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i
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 → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i

Tactic:
[

Goal state after:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i
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
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

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
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
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
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f
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
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
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
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
[

Goal state after:
α : 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
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
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:
[

Goal state after:
α : 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
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
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∪ g.support
⊢ f x✝ = g x✝

Tactic:
[

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∪ g.support
⊢ f x✝ = g x✝
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 ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s, (if i ∈ s then g i else 0) • v i

Tactic:
[

Goal state after:
ι : 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 ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s, (if i ∈ s then g i else 0) • v i
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
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
[

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ x ^ (⊤ * z) = (x ^ ⊤) ^ z

Tactic:
rw [top_mul z_0, epow_top x_2, top_epow z_0]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, cons x f i = x * ∏ i, f i

Tactic:
[

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, cons x f i = x * ∏ i, f i
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:
[

Goal state after:
ι : 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
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : 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 : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
hfg : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
[

Goal state after:
case mp
ι : 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 : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
hfg : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i
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
  rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
  · apply Fintype.prod_sum_type
  · intro x
    simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]

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:
[

Goal state after:
ι : 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
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:
simp [← map_castAddEmb_Ioc]

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 : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
s : ι
hs : s ∈ S
⊢ r₁ s = r₂ s

Tactic:
[

Goal state after:
ι : 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 : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
s : ι
hs : s ∈ S
⊢ r₁ s = r₂ s
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:
simp [← map_castSuccEmb_Iio]

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

Goal state before:
pp: case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).sum fun i a ↦ a • v i

Tactic:
[

Goal state after:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).sum fun i a ↦ a • v i
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 with i.castSucc ≤ j.castSucc, f i.castSucc j) * ∏ j with last n ≤ j.castSucc, f (last n) j) *
      ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j

Tactic:
Fin.prod_univ_succ

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ((∏ i, ∏ j with i.castSucc ≤ j.castSucc, f i.castSucc j) * ∏ j with last n ≤ j.castSucc, f (last n) j) *
      ((∏ j with j.castSucc < 0, f 0 j) * ∏ i, ∏ j with j.castSucc < i.succ, f i.succ j) =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j
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:
[

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case e'_2
ι : 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
x : ↑s
⊢ w ↑x = v ↑x

Tactic:
exact h.symm x.2

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ (∃ z, a = 0 + z • p) ↔ ∃ z, a = z • p

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ (∃ z, a = 0 + z • p) ↔ ∃ z, a = z • p
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a ≡ b + i • p [PMOD n • p]

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a ≡ b + i • p [PMOD n • p]
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ b ≡ a [PMOD p] ↔ ∃ i, i < n ∧ b ≡ a - i • p [PMOD n • p]

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ b ≡ a [PMOD p] ↔ ∃ i, i < n ∧ b ≡ a - i • p [PMOD n • p]