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
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Membership.mem (α := M) (γ := Submodule R M) (span R (Set.range v)) ((linearCombination R v : (a : α →₀ R) → M) l : M)
have h : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (l.sum fun (i : α) (a : R) ↦ a • 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
v : α → M
x : M
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x →
    Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x
have h : Set.range v ⊆ (↑(LinearMap.range (linearCombination R v)) : Set M)
Tactic: apply span_le.2
-- 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
x_1 x : M
hx : x ∈ Set.range v
⊢ x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)
have h : ∀ (i : α) (hi : v i = x), x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)
Tactic: rcases hx with ⟨i, hi⟩
Cleared hypotheses: hx
-- 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
x_1 x : M
i : α
hi : v i = x
⊢ x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)
have h : ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
Tactic: rw [SetLike.mem_coe, LinearMap.mem_range]
-- 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
x_1 x : M
i : α
hi : v i = x
⊢ ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
have h : (linearCombination R v : (a : α →₀ R) → M) (single i 1) = x
Tactic: use single i 1
-- 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
⊢ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α →₀ R) (β := M) (⇑(linearCombination R v) : (a : α →₀ R) → M)
have rw : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_linearCombination]
-- 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
rw :
  Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) ⊤
⊢ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α →₀ R) (β := M) (⇑(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, range_linearCombination]
-- 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
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), (g : (a : M) → M') (v i) = v' (f i)
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v
have h₁ : ∀ (l : α),
  Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l : (a : R) → M') 1 : M')
    (((g ∘ₗ linearCombination R v) ∘ₗ lsingle l : (a : R) → M') 1 : M')
Tactic: ext l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α → α'
⊢ Eq (α := (α →₀ R) →ₗ[R] M') (linearCombination R v' ∘ₗ lmapDomain R R f) (linearCombination R (v' ∘ f))
have h : ∀ (a : α),
  Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a : (a : R) → M') 1 : M')
    ((linearCombination R (v' ∘ f) ∘ₗ lsingle a : (a : R) → M') 1 : M')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (equivMapDomain f l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
have rw : Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (mapDomain (⇑f : (a : α) → α') l) : M')
  ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
Tactic: rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
rw :
  Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (mapDomain (⇑f : (a : α) → α') l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
⊢ Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (equivMapDomain f l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
have rw₁ : Eq.{u_8 + 1} (α := M') ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
  ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
Tactic: rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]
-- 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
s : Set M
⊢ Eq (α := Submodule R M) (span R s)
    (LinearMap.range (M := Finsupp.{u_2, u_5} { x : M // x ∈ s } R)
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have rw : Eq (α := Submodule R M) (span R s)
  (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- 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
s : Set M
rw :
  Eq (α := Submodule R M) (span R s)
    (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ Eq (α := Submodule R M) (span R s)
    (LinearMap.range (M := Finsupp.{u_2, u_5} { x : M // x ∈ s } R)
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have rw₁ : Eq (α := Submodule R M) (span R s) (span R {x : M | x ∈ s})
Tactic: rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- 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
s : Set M
rw :
  Eq (α := Submodule R M) (span R s)
    (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
rw₁ : Eq (α := Submodule R M) (span R s) (span R {x : M | x ∈ s})
⊢ Eq (α := Submodule R M) (span R s)
    (LinearMap.range (M := Finsupp.{u_2, u_5} { x : M // x ∈ s } R)
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have rw₂ : Eq (α := Submodule R M) (span R s) (span R s)
Tactic: rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- 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 M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))
have h₁ : v '' s ⊆ (↑(map (linearCombination R v) (supported R R s)) : Set M)
Tactic: apply span_eq_of_le
-- 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 α
h₁ : v '' s ⊆ (↑(map (linearCombination R v) (supported R R s)) : Set M)
⊢ Eq (α := Submodule R M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))
have h₂ : LE.le (α := Submodule R M) (map (linearCombination R v) (supported R R s)) (span R (v '' s))
Tactic: apply span_eq_of_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (hypothesis)
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 α
x : M
hx : x ∈ v '' s
⊢ x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)
have hx₁ : ∃ x_1 ∈ s, v x_1 = x
Tactic: rw [Set.mem_image] at hx
Cleared hypotheses: hx
-- 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 α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)
have h₁ : ∀ (a : α), a ∈ s ∧ v a = x → x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)
Tactic: apply Exists.elim hx
-- 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 α
⊢ LE.le (α := Submodule R M) (map (linearCombination R v) (supported R R s)) (span R (v '' s))
have h₂ : ∀ (z : α →₀ R) (hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z),
  Membership.mem (γ := Submodule R (α →₀ R)) (comap (linearCombination R v) (span R (v '' s))) z
Tactic: refine map_le_iff_le_comap.2 fun z hz => ?_
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
have haveI : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s),
  Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
Tactic: haveI := Classical.decPred fun x => x ∈ s
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
have pos : ∀ (h : c ∈ s),
  Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
Tactic: by_cases h : c ∈ s
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
pos :
  ∀ (h : c ∈ s),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
have neg : ∀ (h : c ∉ s),
  Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
Tactic: by_cases h : c ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (hypothesis)
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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (comap (linearCombination R v) (span R (v '' s))) z
have this : ∀ (i : α),
  Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
Tactic: have : ∀ i, z i • v i ∈ span R (v '' s) := by
      intro c
      haveI := Classical.decPred fun x => x ∈ s
      by_cases h : c ∈ s
      · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
      · simp [(Finsupp.mem_supported' R _).1 hz _ 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
v : α → M
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (comap (linearCombination R v) (span R (v '' s))) z
have h₂ : Membership.mem (γ := Submodule R M) (span R (v '' s)) (z.sum fun (i : α) (a : R) ↦ a • v i)
Tactic: rw [mem_comap, 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
v : α → M
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) (z.sum fun (i : α) (a : R) ↦ a • v i)
have h₂ : ∀ c ∈ z.support,
  Membership.mem (γ := Submodule R M) (span R (v '' s)) ((fun (i : α) (a : R) ↦ a • v i) c ((z : (a : α) → R) c))
Tactic: refine sum_mem ?_
-- 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 α
x : M
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    ∃ (l : α →₀ R),
      Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l ∧ (linearCombination R v : (a : α →₀ R) → M) l = x
have rw : Membership.mem (γ := Submodule R M) (map (linearCombination R v) (supported R R s)) x ↔
  ∃ (l : α →₀ R),
    Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l ∧ (linearCombination R v : (a : α →₀ R) → M) l = x
Tactic: rw [span_image_eq_map_linearCombination]
-- 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 : Option α → M
f : Finsupp.{u_1, u_5} (Option α) R
⊢ (linearCombination R v : (a : Option α →₀ R) → M) f =
    HAdd.hAdd (β := M) (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none))
      ((linearCombination R (v ∘ Option.some) : (a : α →₀ R) → M) f.some : M)
have rw : (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
    f.some.sum fun (a : α) (r : R) ↦ r • v (Option.some a)) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
    f.some.sum fun (i : α) (a : R) ↦ a • (v ∘ Option.some) i
Tactic: rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ Eq.{u_2 + 1} (α := M)
    ((linearCombination R A : (a : α →₀ R) → M) ((linearCombination R B : (a : β →₀ R) → α →₀ R) f : α →₀ R) : M)
    ((linearCombination R fun (b : β) ↦ (linearCombination R A : (a : α →₀ R) → M) (B b) : (a : β →₀ R) → M) f : M)
have simp : Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
  (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
Tactic: simp only [linearCombination_apply]
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
have zero : Eq.{u_2 + 1} (α := M) (sum (sum 0 fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
  (sum 0 fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
Tactic: induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]
Cleared hypotheses: f
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
zero :
  Eq.{u_2 + 1} (α := M) (sum (sum 0 fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum 0 fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
have add : ∀ (f₁ f₂ : β →₀ R)
  (h₁ :
    Eq.{u_2 + 1} (α := M) (sum (f₁.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
      (f₁.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i)))
  (h₂ :
    Eq.{u_2 + 1} (α := M) (sum (f₂.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
      (f₂.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))),
  Eq.{u_2 + 1} (α := M) (sum ((f₁ + f₂).sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    ((f₁ + f₂).sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
Tactic: induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]
Cleared hypotheses: f
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
zero :
  Eq.{u_2 + 1} (α := M) (sum (sum 0 fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum 0 fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
add :
  ∀ (f₁ f₂ : β →₀ R)
    (h₁ :
      Eq.{u_2 + 1} (α := M) (sum (f₁.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
        (f₁.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i)))
    (h₂ :
      Eq.{u_2 + 1} (α := M) (sum (f₂.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
        (f₂.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))),
    Eq.{u_2 + 1} (α := M) (sum ((f₁ + f₂).sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
      ((f₁ + f₂).sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
have single : ∀ (a : β) (b : R),
  Eq.{u_2 + 1} (α := M) (sum (sum (single a b) fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum (single a b) fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
Tactic: induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]
Cleared hypotheses: f
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ Eq.{u_2 + 1} (α := M)
    ((linearCombination R A : (a : α →₀ R) → M) ((linearCombination R B : (a : β →₀ R) → α →₀ R) f : α →₀ R) : M)
    ((linearCombination R fun (b : β) ↦ (linearCombination R A : (a : α →₀ R) → M) (B b) : (a : β →₀ R) → M) f : M)
have simp : Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
  (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
Tactic: classical
  simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]