mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' uIoo i j = uIoo i.rev j.rev

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
u v : α → M
⊢ linearCombination R (u + v) = linearCombination R u + linearCombination R v

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : b i ∈ range ⇑b
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : ↑(range ⇑b)
⊢ b.reindexRange x = ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
r : S
v : α → M
⊢ linearCombination R (r • v) = (RingHom.id S) r • linearCombination R v

Tactic:
by

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : HasFiniteMulSupport fun x ↦ 0
⊢ HasFiniteMulSupport fun x ↦ 1

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ 1

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ i ∈ Finite.toFinset hf ∪ ?m.37, f i) * ∏ i ∈ ?m.45 ∪ Finite.toFinset hg, g i

pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Finset α

pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Finset α

Tactic:
←
      Finset.prod_mul_distrib

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = ∏ x ∈ Finite.toFinset hf ∪ Finite.toFinset hg, f x * g x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x bi : M
i : ι
h : b i = bi
⊢ (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
⊢ ∀ (a : M), a ∈ range ⇑b ↔ (Equiv.refl M) a ∈ Finset.image (⇑b) Finset.univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, h⟩ = b i

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 g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝ : DivisionCommMonoid G
f g : α → G
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i

Tactic:
by

Goal state after:
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
x : α → R
⊢ (linearCombination R v) ((linearEquivFunOnFinite R R α).symm x) = (Fintype.linearCombination R v) x

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : ↥(Finset.image (⇑b) Finset.univ)
⊢ b.reindexFinsetRange x = ↑x

Tactic:
by

Goal state after:
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
⊢ (Fintype.linearCombination R v).range = span R (Set.range v)

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 g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
by

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

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

Tactic:
by

Goal state after:
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) = ⊤ ↔ Function.Surjective ⇑(Fintype.linearCombination R v)

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
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
by

Goal state after:
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✝ u v : α → M
⊢ Fintype.linearCombination R (u + v) = Fintype.linearCombination R u + Fintype.linearCombination R v

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
⊢ b.reindexFinsetRange.repr (b i) = single ⟨b i, ⋯⟩ 1

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
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i

Tactic:
by

Goal state after:
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 : S
v : α → M
⊢ Fintype.linearCombination R (r • v) = (RingHom.id S) r • Fintype.linearCombination R v

Tactic:
by

Goal state after:
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
inst✝ : DecidableEq α
i : α
r : R
⊢ ((Fintype.bilinearCombination R S) v) (Pi.single i r) = r • v i

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f g : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ ↑b.repr =
    linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr + linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ ↑b.repr

Tactic:
by

Goal state after:
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
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, ∑ i, c i • v i = x

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
c : S
f : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ ↑b.repr =
    (RingHom.id S) c • linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ (fun f i ↦ f (b i)) ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M →ₗ[R] M'
⊢ (fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) ((fun f i ↦ f (b i)) f) = f

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
G : Type u_4
s : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i

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
⊢ ∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((b.constr S) f) x = (b.repr x).sum fun b a ↦ a • f b

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M →ₗ[R] M'
i : ι
⊢ (b.constr S).symm f i = f (b i)

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ ((b.constr S) f) (b i) = f i

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ ((b.constr S) f).range = span R (range f)

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M' →ₗ[R] M'
v : ι → M'
i : ι
⊢ ((b.constr S) (⇑f ∘ v)) (b i) = (f ∘ₗ (b.constr S) v) (b i)

Tactic:
by

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

Goal state before:
pp: M' : Type u_7
inst✝⁸ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
S : Type u_14
inst✝³ : Semiring S
inst✝² : Module S M'
inst✝¹ : SMulCommClass R S M'
inst✝ : Fintype ι
b : Basis ι R M
f : ι → M'
x : M
⊢ ((b.constr S) f) x = ∑ i, b.equivFun x i • f i

Tactic:
by

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

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Module R M'
i : ι
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ (b.equiv b' e) (b i) = b' (e i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ (b.equiv b (Equiv.refl ι)) (b i) = (LinearEquiv.refl R M) (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝¹ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
a : ↥t
x✝ : a ∈ Finset.univ
⊢ v ↑a ∈ v '' s

Tactic:
by

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

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Module R M'
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι'
⊢ (b.equiv b' e) ((b.equiv b' e).symm (b' i)) = (b.equiv b' e) ((b'.equiv b e.symm) (b' i))

Tactic:
by

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

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁶ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
inst✝² : Module R M'
M'' : Type u_13
b' : Basis ι' R M'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
ι'' : Type u_14
b'' : Basis ι'' R M''
e : ι ≃ ι'
e' : ι' ≃ ι''
i : ι
⊢ (b.equiv b' e ≪≫ₗ b'.equiv b'' e') (b i) = (b.equiv b'' (e.trans e')) (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
⊢ x ∈ span R (v '' s) ↔ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
⊢ x ∈ span R (v '' ↑s) ↔ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
by

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

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ b.map (b.equiv b' e) = b'.reindex e.symm

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
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∃ c, ∑ i ∈ s, c i • v i = x

pp: case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
· refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩
    rw [← hc, ← Finset.sum_coe_sort (s := s)]
    simp

Goal state after:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∃ c, ∑ i, c i • v ↑i = x
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
⊢ x ∈ span R (v '' ↑s) ↔ ∃ c, ∑ i ∈ s, c i • v i = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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

Tactic:
by

Goal state after:
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
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) (repr R w x) = ↑x

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b') ∘ₗ (b.constr R) (f ∘ ⇑b)) (b i) = LinearMap.id (b i)

Tactic:
by

Goal state after:
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 : Set M
l : M →₀ R
hl : l ∈ supported R R s
⊢ ↑l.support ⊆ _root_.id '' s ∧
    Function.support ⇑l ⊆ ↑l.support ∧ ∑ a ∈ l.support, l a • a = (linearCombination R _root_.id) l

Tactic:
by

Goal state after: