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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ ∃ a ∈ s, f a = c

Tactic:
by

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

Goal state before:
pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
⊢ map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
⊢ (l.sum fun a ↦ single (f a)) (f x) = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → R
x : M
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f 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_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
c : R
a : α
⊢ (linearCombination R v) (single a c) = c • v a

Tactic:
by

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

Goal state before:
pp: ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
c : R
f : ι → M
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f 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_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : α →₀ R
⊢ (linearCombination R 0) x = 0

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 α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator 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 : α → M
a : α
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
i : α
x✝ : f i ≠ 0
hi : i ≠ a
⊢ f i • Pi.single a c i = 0

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 : α) (_ : a ∈ mulSupport f), f a = ∏ᶠ (a : α), f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
x✝ : f a = 0
⊢ 0 • Pi.single a c a = 0

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 : Finset α
h : mulSupport f ⊆ ↑s
⊢ mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport 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_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ (linearCombination R (Pi.single a c)) f = f a • c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
⊢ linearCombination R (⇑f ∘ v) = f ∘ₗ 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 : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v) l = l default • v default

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ Disjoint (supported M R s) (lmapDomain M R f).ker

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ (linearCombination R v) (single y 1) = 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_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
⊢ Function.Surjective ⇑(linearCombination R v)

Tactic:
by

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

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
s : Set α
t : Set α'
e : ↑s ≃ ↑t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R 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
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f 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
s : Set α
h : mulSupport f ⊆ s
hs : s.Finite
⊢ mulSupport f ⊆ ↑hs.toFinset

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 : Finset α
h : mulSupport f ⊆ ↑s
⊢ ⋯.toFinset ⊆ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g

Tactic:
by

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑(s.attachFin h) = Fin.val ⁻¹' ↑s

Tactic:
by

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ image Fin.val (s.attachFin h) = s

Tactic:
by

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ map Fin.valEmbedding (s.attachFin h) = s

Tactic:
by

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hst : s ⊆ t
ht : ∀ m ∈ t, m < n
⊢ s.attachFin ⋯ ⊆ t.attachFin ht

Tactic:
by

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

Tactic:
by

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hst : s ⊂ t
ht : ∀ m ∈ t, m < n
⊢ s.attachFin ⋯ ⊂ t.attachFin ht

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
⊢ range val = Iio n

Tactic:
ext; simp [Fin.exists_iff]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
⊢ range val = Iio n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Ici i = Ico (↑i) n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Iic i = Iic ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Ioi i = Ioo (↑i) n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Iio i = Iio ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Icc i j = Icc ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ico i j = Ico ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioc i j = Ioc ↑i ↑j

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
inst✝ : Decidable (HasFiniteMulSupport f)
⊢ ∏ᶠ (i : α), f i = if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioo i j = Ioo ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' uIcc i j = uIcc ↑i ↑j

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'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h : (fun b i ↦ b.repr.symm (single i 1)) f = (fun b i ↦ b.repr.symm (single i 1)) g
⊢ ↑f.repr.symm = ↑g.repr.symm

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' uIoc i j = uIoc ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' uIoo i j = uIoo ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iic i = val '' Iic (castLE h 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
hf : (mulSupport f).Infinite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iic i = val '' Iic (castLE h i)

Tactic:
by simp [image_image]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iio i = val '' Iio (castLE h i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iio i = val '' Iio (castLE h i)

Tactic:
by simp [image_image]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Icc i j = val '' Icc (castLE h i) (castLE h j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Icc i j = val '' Icc (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ico i j = val '' Ico (castLE h i) (castLE h j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
c : R
⊢ b.repr.symm (single i c) = b.repr.symm (c • single i 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ico i j = val '' Ico (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ (linearCombination R v).range = span R (Set.range v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioc i j = val '' Ioc (castLE h i) (castLE h j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
⊢ HasFiniteSupport f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioc i j = val '' Ioc (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(linearCombination R v)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
c : R
⊢ b.repr.symm (c • single i 1) = c • b i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioo i j = val '' Ioo (castLE h i) (castLE h j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioo i j = val '' Ioo (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIcc i j = val '' uIcc (castLE h i) (castLE h j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIcc i j = val '' uIcc (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (b.repr (b i)) j = if i = j then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoc i j = val '' uIoc (castLE h i) (castLE h j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoc i j = val '' uIoc (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoo i j = val '' uIoo (castLE h i) (castLE h j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoo i j = val '' uIoo (castLE h i) (castLE h j)

Tactic:
by simp [image_image]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr.symm v = b.repr.symm (v.sum single)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ↪ α'
l : α →₀ R
⊢ (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
⊢ val '' range (castAdd m) = val '' Iio (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ (v.sum fun i vi ↦ b.repr.symm (single i vi)) = (linearCombination R ⇑b) v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ici i = val '' Ico (castAdd m i) (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ioi i = val '' Ioo (castAdd m i) (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr ((linearCombination R ⇑b) v) = v

Tactic:
by

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

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = (linearCombination R Subtype.val).range

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, (c.sum fun i a ↦ a • v i) = x

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
by

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
α : Type u_7
F : Type u_8
inst✝² : Fintype α
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
g : α → M
⊢ f (∏ i, g i) = ∏ i, f (g i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin (m + n)
hi : m ≤ ↑i
⊢ ↑i - m < n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
⊢ range (natAdd m) = {i | m ≤ ↑i}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
⊢ range (natAdd m) = Ioi (castAdd n ⊤)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ (linearCombination R v) (single i 1) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ici (natAdd m i) = Ici i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ioi (natAdd m i) = Ioi 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
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
⊢ ∀ (x_1 : ι'), ((b.reindex e).repr x) x_1 = (mapDomain (⇑e) (b.repr x)) x_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
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ mulSupport (s.mulIndicator f) ⊆ ↑t

Tactic:
by

Goal state after: