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

Goal state before:
pp: case neg
α : 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 x = 0 x

Tactic:
·

Goal state after:
case neg
α : 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 x = 0 x
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mp
α : 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 ∈ (linearCombination R v).range → x ∈ span R (Set.range v)

pp: case mpr
α : 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) → x ∈ (linearCombination R v).range

Tactic:
·

Goal state after:
case mp
α : 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 ∈ (linearCombination R v).range → x ∈ span R (Set.range v)
Module: Mathlib.Algebra.BigOperators.Finprod

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

pp: case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ Finite.toFinset h, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
·

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mpr
α : 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) → x ∈ (linearCombination R v).range

Tactic:
·

Goal state after:
case mpr
α : 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) → x ∈ (linearCombination R v).range
Module: Mathlib.Algebra.BigOperators.Finprod

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

pp: case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ HasFiniteSupport f

Tactic:
·

Goal state after:
case inl
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Subsingleton R
⊢ HasFiniteSupport f
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ HasFiniteSupport f
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:
rw [finprod_def, dif_pos hf]

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

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

pp: case neg
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
·

Goal state after:
case neg
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
ι : 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
h₂ : (mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

pp: case neg
ι : 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
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
·

Goal state after:
case pos
ι : 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
h₂ : (mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
ι : 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
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
·

Goal state after:
case neg
ι : 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
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: case mp
m n : ℕ
i : Fin (m + n)
⊢ i ∈ range (natAdd m) → i ∈ {i | m ≤ ↑i}

pp: case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)

Tactic:
·

Goal state after:
case mp
m n : ℕ
i : Fin (m + n)
⊢ i ∈ range (natAdd m) → i ∈ {i | m ≤ ↑i}
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h₁
α : 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 α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))

pp: case h₂
α : 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 α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)

Tactic:
·

Goal state after:
case h₁
α : 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 α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)

Tactic:
·

Goal state after:
case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
by lia

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

Goal state before:
pp: case h₂
α : 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 α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)

Tactic:
·

Goal state after:
case h₂
α : 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 α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case pos
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)

pp: case neg
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
·

Goal state after:
case pos
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case neg
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
·

Goal state after:
case neg
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t

pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Icc i j = Icc (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Icc_natAdd, image_preimage_eq_of_subset]
  exact Icc_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ 1 < ∏ i ∈ hf.toFinset, f i

pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset)

Tactic:
·

Goal state after:
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ 1 < ∏ i ∈ hf.toFinset, f i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : ↑i + m ≤ ↑j
⊢ ↑j - m < n

Tactic:
by lia

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

Goal state before:
pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ i ∈ hf.toFinset, 1 ≤ f i

pp: case hs
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∃ i ∈ hf.toFinset, 1 < f i

Tactic:
·

Goal state after:
case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ i ∈ hf.toFinset, 1 ≤ f i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' Ioi i = Ioi (i.addNat m)

Tactic:
by
  rw [← preimage_addNat_Ioi_addNat, image_preimage_eq_of_subset]
  exact Ioi_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: case hs
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∃ i ∈ hf.toFinset, 1 < f i

Tactic:
·

Goal state after:
case hs
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∃ i ∈ hf.toFinset, 1 < f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset)

Tactic:
·

Goal state after:
case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: case inl
ι : 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
h✝ : Subsingleton R
⊢ b.reindexRange ⟨b i, h⟩ = b i

pp: case inr
ι : 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
h✝ : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
·

Goal state after:
case inl
ι : 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
h✝ : Subsingleton R
⊢ b.reindexRange ⟨b i, h⟩ = b i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: case inr
ι : 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
h✝ : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
·

Goal state after:
case inr
ι : 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
h✝ : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i
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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (x y : M),
    (fun i ↦ (b.reindexRange.repr (x + y)) ⟨b i, ⋯⟩) =
      (fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩) + fun i ↦ (b.reindexRange.repr y) ⟨b i, ⋯⟩

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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)

Tactic:
·

Goal state after:
ι : 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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (x y : M),
    (fun i ↦ (b.reindexRange.repr (x + y)) ⟨b i, ⋯⟩) =
      (fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩) + fun i ↦ (b.reindexRange.repr y) ⟨b i, ⋯⟩
Module: Mathlib.Algebra.BigOperators.Finprod

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

pp: case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1

Tactic:
·

Goal state after:
case pos
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)

Tactic:
·

Goal state after:
ι : 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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
·

Goal state after:
case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)

Tactic:
·

Goal state after:
ι : 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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h
α : 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
⊢ ((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ

pp: case hf
α : 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
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0

Tactic:
·

Goal state after:
case h
α : 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
⊢ ((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case hf
α : 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
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0

Tactic:
·

Goal state after:
case hf
α : 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
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0
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
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

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
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j

Tactic:
·

Goal state after:
α : 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
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
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
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j

Tactic:
·

Goal state after:
α : 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
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j
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 : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, 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 : 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
⊢ x ∈ span R (v '' s)

Tactic:
·

Goal state after:
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 : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
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:
simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

Goal state after: