awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
v : α → M
f : α' → α
h :
  ∀ (a : α'),
    Eq.{u_2 + 1} (α := M) ((linearCombination R (v ∘ f) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      (((linearCombination R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a : (a : R) → M) 1 : M)
⊢ Eq (α := (α' →₀ R) →ₗ[R] M) (linearCombination R (v ∘ f)) (linearCombination R v ∘ₗ lmapDomain R R f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
v : α → M
f : α' → α
a : α'
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R (v ∘ f) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    (((linearCombination R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a : (a : R) → M) 1 : M)

Tactic:
simp [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' (↑l.support : Set α'))
rw :
  Eq.{u_2 + 1} (α := M) ((comapDomain f l hf).sum fun (i : α) (a : R) ↦ a • v i)
    (∑ i ∈ l.support.preimage f hf, HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α') → R) (f i) : R) (v i))
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) (comapDomain f l hf) : M)
    (∑ i ∈ l.support.preimage f hf, HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α') → R) (f i) : R) (v i) : M)

Tactic:
rw [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' (↑l.support : Set α'))
⊢ Eq.{u_2 + 1} (α := M) ((comapDomain f l hf).sum fun (i : α) (a : R) ↦ a • v i)
    (∑ i ∈ l.support.preimage f hf, HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α') → R) (f i) : R) (v i))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
simp : Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R g : (a : α →₀ R) → M) (onFinset s f hf) : M) (∑ x ∈ s, f x • g x : M)

Tactic:
simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]

Premises used: Finsupp.onFinset_apply, Finsupp.support_onFinset, Finsupp.sum, Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
rw : ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
⊢ Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)

Tactic:
rw [Finset.sum_filter_of_ne]

Premises used: Finset.sum_filter_of_ne
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
_ : x ∈ s → f x • g x ≠ 0 → f x ≠ 0
⊢ x ∈ s → f x • g x ≠ 0 → f x ≠ 0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
h_1 : x ∈ s
h : f x • g x ≠ 0
contrapose : ∀ (h : f x = 0), f x • g x = 0
⊢ f x ≠ 0

Tactic:
contrapose h
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
h_1 : x ∈ s
h : f x = 0
⊢ f x • g x = 0

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
simp : Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)
simp₁ simp₂ : ∀ x ∈ s, ∀ (h : f x • g x ≠ 0), f x ≠ 0
simp₃ : ∀ x ∈ s, ∀ (h : f x = 0), f x • g x = 0
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R g : (a : α →₀ R) → M) (onFinset s f hf) : M) (∑ x ∈ s, f x • g x : M)

Tactic:
classical
  simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
  rw [Finset.sum_filter_of_ne]
  intro x _ h
  contrapose h
  simp [h]

Premises used: Finsupp.onFinset_apply, Finsupp.support_onFinset, Finsupp.sum, Finsupp.linearCombination_apply, Finset.sum_filter_of_ne
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : 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_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
M' : Type u_8
inst_8 : AddCommMonoid M'
inst_9 : Module R M'
v_1 : α → M
v' : α' → M'
inst_10 : Module S M
inst_11 : SMulCommClass R S M
u v : α → M
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M) ((linearCombination R (u + v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      ((HAdd.hAdd (α := (α →₀ R) →ₗ[R] M) (linearCombination R u) (linearCombination R v) ∘ₗ lsingle a : (a : R) → M)
          1 :
        M)
⊢ linearCombination R (u + v) = HAdd.hAdd (α := (α →₀ R) →ₗ[R] M) (linearCombination R u) (linearCombination R v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : 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_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
M' : Type u_8
inst_8 : AddCommMonoid M'
inst_9 : Module R M'
v_1 : α → M
v' : α' → M'
inst_10 : Module S M
inst_11 : SMulCommClass R S M
u v : α → M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R (u + v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((HAdd.hAdd (α := (α →₀ R) →ₗ[R] M) (linearCombination R u) (linearCombination R v) ∘ₗ lsingle a : (a : R) → M) 1 :
      M)

Tactic:
simp [Pi.add_apply, smul_add]

Premises used: Pi.add_apply, smul_add
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : 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_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
M' : Type u_8
inst_8 : AddCommMonoid M'
inst_9 : Module R M'
v_1 : α → M
v' : α' → M'
inst_10 : Module S M
inst_11 : SMulCommClass R S M
r : S
v : α → M
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M) ((linearCombination R (r • v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      ((HSMul.hSMul (α := S) (β := (α →₀ R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (linearCombination R v) ∘ₗ
              lsingle a :
            (a : R) → M)
          1 :
        M)
⊢ linearCombination R (r • v) =
    HSMul.hSMul (α := S) (β := (α →₀ R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (linearCombination R v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : 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_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
M' : Type u_8
inst_8 : AddCommMonoid M'
inst_9 : Module R M'
v_1 : α → M
v' : α' → M'
inst_10 : Module S M
inst_11 : SMulCommClass R S M
r : S
v : α → M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R (r • v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((HSMul.hSMul (α := S) (β := (α →₀ R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (linearCombination R v) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)

Tactic:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
⊢ Eq (α := (α →₀ R) →ₗ[R] M) ((bilinearCombination R S : (a : α → M) → (α →₀ R) →ₗ[R] M) v : (α →₀ R) →ₗ[R] M)
    (linearCombination R v : (α →₀ R) →ₗ[R] M)

Tactic:
rfl

Premises used: Finsupp.linearCombination, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
f g : α → R
simp_rw : Eq.{u_2 + 1} (α := M) (∑ i : α, (f + g) i • v i) (∑ x : α, (f x + g x) • v x)
⊢ ∑ i : α, (f + g) i • v i = HAdd.hAdd (α := M) (∑ i : α, f i • v i) (∑ i : α, g i • v i)

Tactic:
simp_rw [← Finset.sum_add_distrib, ← add_smul]

Premises used: Finset.sum_add_distrib, add_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
f g : α → R
⊢ Eq.{u_2 + 1} (α := M) (∑ i : α, (f + g) i • v i) (∑ x : α, (f x + g x) • v x)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
r : R
f : α → R
simp_rw :
  Eq.{u_2 + 1} (α := M) (∑ i : α, (r • f) i • v i)
    (∑ x : α, HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (f x) • v x)
⊢ ∑ i : α, (r • f) i • v i = HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R) (∑ i : α, f i • v i)

Tactic:
simp_rw [Finset.smul_sum, smul_smul]

Premises used: smul_smul, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ Eq.{u_2 + 1} (α := M) (∑ i : α, (r • f) i • v i)
    (∑ x : α, HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (f x) • v x)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
f : α → R
⊢ Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R v : (a : α → R) → M) f : M) (∑ i : α, f i • v i : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
inst_4 : DecidableEq α
i : α
r : R
simp_rw : (∑ x : α, if x = i then r • v x else 0) = r • v i
⊢ (Fintype.linearCombination R v : (a : α → R) → M) (Pi.single (M := fun (a : α) ↦ R) i r) = r • v i

Tactic:
simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]

Premises used: Pi.single_apply, zero_smul, ite_smul, Fintype.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
inst_4 : DecidableEq α
i : α
r : R
rw : (if Membership.mem (γ := Finset α) Finset.univ i then r • v i else 0) = r • v i
rw₁ rw₂ : r • v i = r • v i
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i

Tactic:
rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Premises used: Finset.mem_univ, Finset.sum_ite_eq', if_pos
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : α → R
h :
  Subset.{u_1} (α := Finset α)
    (support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x))
    Finset.univ
hf :
  ∀ (x_1 : α),
    Membership.mem (γ := Finset α) Finset.univ x_1 →
      x_1 ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x) →
        Eq.{u_2 + 1} (α := M)
          ((fun (i : α) ↦
              ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M))
            x_1
            ((((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x : α →₀ R) : (a : α) → R) x_1))
          0
⊢ Eq.{u_2 + 1} (α := M)
    ((linearCombination R v : (a : α →₀ R) → M)
        ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x : α →₀ R) :
      M)
    ((Fintype.linearCombination R v : (a : α → R) → M) x : M)

Tactic:
apply Finset.sum_subset

Premises used: Finset.sum_subset
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : α → R
⊢ Subset.{u_1} (α := Finset α)
    (support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x))
    Finset.univ

Tactic:
Finset.subset_univ _

Premises used: Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : α → R
⊢ Subset.{u_1} (α := Finset α)
    (support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x))
    Finset.univ

Tactic:
exact Finset.subset_univ _

Premises used: Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x_1 : α → R
x : α
hf :
  Membership.mem (γ := Finset α) Finset.univ x →
    x ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1) →
      Eq.{u_2 + 1} (α := M)
        ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M))
          x ((((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1 : α →₀ R) : (a : α) → R) x))
        0
⊢ Membership.mem (γ := Finset α) Finset.univ x →
    x ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1) →
      Eq.{u_2 + 1} (α := M)
        ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M))
          x ((((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1 : α →₀ R) : (a : α) → R) x))
        0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x_1 : α → R
x : α
h : Membership.mem (γ := Finset α) Finset.univ x
hx : x ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1)
hf :
  Eq.{u_2 + 1} (α := M)
    ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M)) x
      0)
    0
⊢ Eq.{u_2 + 1} (α := M)
    ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M)) x
      ((((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1 : α →₀ R) : (a : α) → R) x))
    0

Tactic:
rw [Finsupp.notMem_support_iff.mp hx]

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x_1 : α → R
x : α
h : Membership.mem (γ := Finset α) Finset.univ x
hx : x ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1)
⊢ Eq.{u_2 + 1} (α := M)
    ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M)) x
      0)
    0

Tactic:
zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x_1 : α → R
x : α
h : Membership.mem (γ := Finset α) Finset.univ x
hx : x ∉ support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1)
⊢ Eq.{u_2 + 1} (α := M)
    ((fun (i : α) ↦ ((⇑((fun (i : α) ↦ (smulRight LinearMap.id (v i) : R →ₗ[R] M)) i) : (a : R) → M) : (a : R) → M)) x
      0)
    0

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
⊢ Eq (α := (α → R) →ₗ[R] M)
    (linearCombination R v ∘ₗ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) : (α → R) →ₗ[R] α →₀ R))
    (Fintype.linearCombination R v)

Tactic:
LinearMap.ext <| linearCombination_eq_fintype_linearCombination_apply R v

Premises used: LinearMap.ext, Finsupp.linearCombination_eq_fintype_linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
rw :
  Eq (α := Submodule R M)
    (LinearMap.range
      (Finsupp.linearCombination R v ∘ₗ
        (↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)) : (α → R) →ₗ[R] α →₀ R)))
    (span R (Set.range v))
rw₁ :
  Eq (α := Submodule R M)
    (map (Finsupp.linearCombination R v)
      (LinearMap.range (↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)) : (α → R) →ₗ[R] α →₀ R)))
    (span R (Set.range v))
rw₂ : Eq (α := Submodule R M) (map (Finsupp.linearCombination R v) ⊤) (span R (Set.range v))
rw₃ : Eq (α := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v)) (span R (Set.range v))
rw₄ rw₅ : Eq (α := Submodule R M) (span R (Set.range v)) (span R (Set.range v))
⊢ Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))

Tactic:
rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]

Premises used: Submodule.map_top, LinearMap.range_comp, Finsupp.range_linearCombination, Finsupp.linearCombination_eq_fintype_linearCombination, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
rw :
  Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) ⊤
rw₁ rw₂ : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
⊢ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : α → R) → M)

Tactic:
rw [← LinearMap.range_eq_top, Fintype.range_linearCombination]

Premises used: LinearMap.range_eq_top, Fintype.range_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v_1 u v : α → M
h :
  ∀ (x : α → R),
    Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R (u + v) : (a : α → R) → M) x : M)
      ((HAdd.hAdd (α := (α → R) →ₗ[R] M) (Fintype.linearCombination R u) (Fintype.linearCombination R v) :
            (a : α → R) → M)
          x :
        M)
⊢ Fintype.linearCombination R (u + v) =
    HAdd.hAdd (α := (α → R) →ₗ[R] M) (Fintype.linearCombination R u) (Fintype.linearCombination R v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v_1 u v : α → M
x : α → R
⊢ Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R (u + v) : (a : α → R) → M) x : M)
    ((HAdd.hAdd (α := (α → R) →ₗ[R] M) (Fintype.linearCombination R u) (Fintype.linearCombination R v) :
          (a : α → R) → M)
        x :
      M)

Tactic:
simp [Fintype.linearCombination,
    Finset.sum_add_distrib, Pi.add_apply, smul_add]

Premises used: Finset.sum_add_distrib, Pi.add_apply, Fintype.linearCombination, smul_add
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v_1 : α → M
r : S
v : α → M
h :
  ∀ (x : α → R),
    Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R (r • v) : (a : α → R) → M) x : M)
      ((HSMul.hSMul (α := S) (β := (α → R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S)
              (Fintype.linearCombination R v) :
            (a : α → R) → M)
          x :
        M)
⊢ Fintype.linearCombination R (r • v) =
    HSMul.hSMul (α := S) (β := (α → R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (Fintype.linearCombination R v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v_1 : α → M
r : S
v : α → M
x : α → R
⊢ Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R (r • v) : (a : α → R) → M) x : M)
    ((HSMul.hSMul (α := S) (β := (α → R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (Fintype.linearCombination R v) :
          (a : α → R) → M)
        x :
      M)

Tactic:
simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]

Premises used: Fintype.linearCombination, Finset.smul_sum, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
⊢ Eq (α := (α → R) →ₗ[R] M) ((Fintype.bilinearCombination R S : (a : α → M) → (α → R) →ₗ[R] M) v : (α → R) →ₗ[R] M)
    (Fintype.linearCombination R v : (α → R) →ₗ[R] M)

Tactic:
rfl

Premises used: Fintype.linearCombination, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v : α → M
inst_7 : DecidableEq α
i : α
r : R
⊢ (((Fintype.bilinearCombination R S : (a : α → M) → (α → R) →ₗ[R] M) v : (α → R) →ₗ[R] M) : (a : α → R) → M)
      (Pi.single (M := fun (a : α) ↦ R) i r) =
    r • v i

Tactic:
simp [Fintype.bilinearCombination]

Premises used: Fintype.bilinearCombination