awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
α' : Type u_7
v : α → M
inst_4 : Module R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
w : α' → S
⊢ Eq (α := (α × α' →₀ R) →ₗ[R] M) (linearCombination R fun (i : α × α') ↦ w i.2 • v i.1)
    ((↑R :
          {S : Type u_6} →
            {M : Type (max u_1 u_6)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module R M] →
                          [inst_11 : Module R M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (linearCombination S v) ∘ₗ
      mapRange.linearMap (linearCombination R w) ∘ₗ (↑(curryLinearEquiv R) : (α × α' →₀ R) →ₗ[R] α →₀ α' →₀ R))
have h : ∀ (a : α × α'),
  Eq.{u_2 + 1} (α := M) (((linearCombination R fun (i : α × α') ↦ w i.2 • v i.1) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((((↑R :
                  {S : Type u_6} →
                    {M : Type (max u_1 u_6)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_7 : Semiring S] →
                            [inst_8 : AddCommMonoid M] →
                              [inst_9 : AddCommMonoid M₂] →
                                [inst_10 : Module R M] →
                                  [inst_11 : Module R M₂] →
                                    [inst_12 : Module S M] →
                                      [inst_13 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (linearCombination S v) ∘ₗ
              mapRange.linearMap (linearCombination R w) ∘ₗ
                (↑(curryLinearEquiv R) : (α × α' →₀ R) →ₗ[R] α →₀ α' →₀ R)) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Fin 0 → M
⊢ Eq (α := (Fin 0 →₀ R) →ₗ[R] M) (linearCombination R f) 0
have h : ∀ (i : Fin 0),
  Eq.{u_2 + 1} (α := M) ((linearCombination R f ∘ₗ lsingle i : (a : R) → M) 1 : M)
    ((0 ∘ₗ lsingle i : (a : R) → M) 1 : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
⊢ Eq (α := Submodule R ↥(span R (v '' s))) (LinearMap.range (linearCombinationOn α M R v s)) ⊤
have rw : LE.le (α := Submodule R M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))
Tactic: rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
    range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
⊢ Eq (α := Finsupp.{u_1, u_5} (↑s : Type u_1) R →ₗ[R] M) (linearCombination R (s.restrict (π := fun (a : α) ↦ M) v))
    (Submodule.subtype (span R (v '' s)) ∘ₗ
      linearCombinationOn α M R v s ∘ₗ
        (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s)))
have h : ∀ (a : (↑s : Type u_1)),
  Eq.{u_2 + 1} (α := M) ((linearCombination R (s.restrict (π := fun (a : α) ↦ M) v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    (((Submodule.subtype (span R (v '' s)) ∘ₗ
              linearCombinationOn α M R v s ∘ₗ
                (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s))) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
⊢ Eq (α := Finsupp.{u_1, u_5} (↑s : Type u_1) R →ₗ[R] M) (linearCombination R (s.restrict (π := fun (a : α) ↦ M) v))
    (Submodule.subtype (span R (v '' s)) ∘ₗ
      linearCombinationOn α M R v s ∘ₗ
        (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s)))
have h : ∀ (a : (↑s : Type u_1)),
  Eq.{u_2 + 1} (α := M) ((linearCombination R (s.restrict (π := fun (a : α) ↦ M) v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    (((Submodule.subtype (span R (v '' s)) ∘ₗ
              linearCombinationOn α M R v s ∘ₗ
                (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s))) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)
Tactic: classical ext; simp [linearCombinationOn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 : α' → α
⊢ Eq (α := (α' →₀ R) →ₗ[R] M) (linearCombination R (v ∘ f)) (linearCombination R v ∘ₗ lmapDomain R R f)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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) ((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)
have 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))
Tactic: rw [linearCombination_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R g : (a : α →₀ R) → M) (onFinset s f hf) : M) (∑ x ∈ s, f x • g x : M)
have simp : Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)
Tactic: simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)
have rw : ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
Tactic: rw [Finset.sum_filter_of_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ f x ≠ 0
have contrapose : ∀ (h : f x = 0), f x • g x = 0
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R g : (a : α →₀ R) → M) (onFinset s f hf) : M) (∑ x ∈ s, f x • g x : M)
have simp : Eq.{u_2 + 1} (α := M) (∑ x ∈ s with f x ≠ 0, f x • g x) (∑ x ∈ s, f x • g x)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)
have simp₁ : ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R g : (a : α →₀ R) → M) (onFinset s f hf) : M) (∑ x ∈ s, f x • g x : M)
have simp₃ : ∀ x ∈ s, ∀ (h : f x = 0), f x • g x = 0
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ linearCombination R (u + v) = HAdd.hAdd (α := (α →₀ R) →ₗ[R] M) (linearCombination R u) (linearCombination R v)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ linearCombination R (r • v) =
    HSMul.hSMul (α := S) (β := (α →₀ R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (linearCombination R v)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∑ i : α, (f + g) i • v i = HAdd.hAdd (α := M) (∑ i : α, f i • v i) (∑ i : α, g i • v i)
have simp_rw : Eq.{u_2 + 1} (α := M) (∑ i : α, (f + g) i • v i) (∑ x : α, (f x + g x) • v x)
Tactic: simp_rw [← Finset.sum_add_distrib, ← add_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∑ i : α, (r • f) i • v i = HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R) (∑ i : α, f i • v i)
have 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)
Tactic: simp_rw [Finset.smul_sum, smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ (Fintype.linearCombination R v : (a : α → R) → M) (Pi.single (M := fun (a : α) ↦ R) i r) = r • v i
have simp_rw : (∑ x : α, if x = i then r • v x else 0) = r • v i
Tactic: simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i
have rw : (if Membership.mem (γ := Finset α) Finset.univ i then r • v i else 0) = r • v i
Tactic: rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i
have rw₁ : r • v i = r • v i
Tactic: rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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)
have h : Subset.{u_1} (α := Finset α)
  (support.{u_1, u_3} (M := R) ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x)) Finset.univ
Tactic: apply Finset.sum_subset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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)
have 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
Tactic: apply Finset.sum_subset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
      ((((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : α → R) → α →₀ R) x_1 : α →₀ R) : (a : α) → R) x))
    0
have 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
Tactic: rw [Finsupp.notMem_support_iff.mp hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))
have 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))
Tactic: rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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))
⊢ Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))
have 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))
Tactic: rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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))
⊢ Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))
have rw₂ : Eq (α := Submodule R M) (map (Finsupp.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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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))
⊢ Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))
have rw₃ : Eq (α := Submodule R M) (LinearMap.range (Finsupp.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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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))
⊢ Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) (span R (Set.range v))
have rw₄ : Eq (α := Submodule R M) (span R (Set.range v)) (span R (Set.range v))
Tactic: rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : α → R) → M)
have rw : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
  Eq (α := Submodule R M) (LinearMap.range (Fintype.linearCombination R v)) ⊤
Tactic: rw [← LinearMap.range_eq_top, Fintype.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)) ⊤
⊢ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : α → R) → M)
have rw₁ : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
Tactic: rw [← LinearMap.range_eq_top, Fintype.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Fintype.linearCombination R (u + v) =
    HAdd.hAdd (α := (α → R) →ₗ[R] M) (Fintype.linearCombination R u) (Fintype.linearCombination R v)
have 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)
Tactic: ext