mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ u = u

Tactic:
]

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
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0

Tactic:
]

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 α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (z.sum fun i a ↦ a • v i) ∈ 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 α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (z.sum fun i a ↦ a • v i) ∈ span R (v '' s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : 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
⊢ x ∈ s ↔ x ∈ t

Tactic:
]

Goal state after:
α : 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
⊢ x ∈ s ↔ x ∈ t
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
⊢ x ∈ map (linearCombination R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
]

Goal state after:
α : 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
⊢ x ∈ map (linearCombination R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ range (natAdd m)
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 ∈ s ∧ x ∈ mulSupport f

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 ∈ s ∧ x ∈ mulSupport f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ {i | m ≤ ↑i}

Tactic:
]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ {i | m ≤ ↑i}
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 ∈ ↑t ∧ x ∈ mulSupport f

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 ∈ ↑t ∧ x ∈ mulSupport f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) = Ioi (natAdd m i)

pp: n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i j : Fin n
⊢ Icc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Icc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
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 : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a ↦ a • (v ∘ Option.some) i

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a ↦ a • (v ∘ Option.some) i
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = s ∩ mulSupport f

Tactic:
]

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 α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (a : α), s.mulIndicator f a = 1

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (a : α), s.mulIndicator f a = 1
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (mulSupport (s.mulIndicator f)).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (mulSupport (s.mulIndicator f)).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), s.mulIndicator f a = ∏ᶠ (a : α), s.mulIndicator f a

Tactic:
]

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 α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ t), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
]

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

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.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) = Ici (i.addNat m)

pp: n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) ⊆ range fun x ↦ x.addNat m
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
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)

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
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
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 α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s)

Tactic:
]

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

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

pp: n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

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

pp: n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
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
R₁ : Type u_13
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)

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
R₁ : Type u_13
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) = Ico (i.addNat m) (j.addNat m)

pp: n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) = Ioc (i.addNat m) (j.addNat m)

pp: n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) = Ioo (i.addNat m) (j.addNat m)

pp: n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
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
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f i

Tactic:
]

Goal state after:
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ x✝ : M
⊢ f x✝¹ i + f x✝ i = f x✝¹ i + f x✝ i

Tactic:
]

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
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ (single j 1) i = (single j 1) i

Tactic:
]

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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = (lapply i ∘ₗ ↑b.repr) x

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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = (lapply i ∘ₗ ↑b.repr) x
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
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∑ x ∈ s, f x • g x = ∑ a ∈ s, f a • g a

pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
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
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ x • y • z = x • y • z

Tactic:
]

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
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
]

Goal state after:
α : 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
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
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 ≤ ∏ᶠ (x : α), 1

Tactic:
]

Goal state after:
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
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
⊢ 1 ≤ ∏ᶠ (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
⊢ 1 ≤ ∏ᶠ (x : α), 1
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 = ∏ x ∈ Finite.toFinset hf ∪ Finite.toFinset hg, f x * g x

Tactic:
]

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.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
⊢ r • v i = r • v i

Tactic:
]

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
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i
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 : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x 0 = 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 : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x 0 = 0
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 : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g 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) = span R (Set.range v)

Tactic:
]

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) = ⊤ ↔ span R (Set.range v) = ⊤

Tactic:
]

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

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1