awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ Eq.{u_6 + 1} (α := M)
    ((((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) :
            ι →₀ M) :
          (a : ι) → M)
        j :
      M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)
have h : Eq (α := M) ((f : (a : M) → M) (lapply j ∘ₗ g ∘ₗ lsingle i • m) : M)
  ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
          ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
          ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
        (a : ι) → M)
      j :
    M)
Tactic: change f (Finsupp.lapply j ∘ₗ g ∘ₗ Finsupp.lsingle i • m) = _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ Eq (α := M) ((f : (a : M) → M) (lapply j ∘ₗ g ∘ₗ lsingle i • m) : M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)
have h : HSMul.hSMul (β := M) (lapply j ∘ₗ g ∘ₗ lsingle i) ((f : (a : M) → M) m : M) =
  (HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
        ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
        ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
      (a : ι) → M)
    j
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
⊢ Eq (α := End (End R (ι →₀ M)) (ι →₀ M))
    { toFun := (⇑(mapRange.addMonoidHom (↑1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } 1
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry, map_smul' := sorry } :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((1 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
x x_1 : End (End R M) M
⊢ { toFun := (⇑(mapRange.addMonoidHom (↑(x * x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := End (End R (ι →₀ M)) (ι →₀ M))
      { toFun := (⇑(mapRange.addMonoidHom (↑x : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
      { toFun := (⇑(mapRange.addMonoidHom (↑x_1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
have h : ∀ (x_2 : ι →₀ M) (a : ι),
  Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x * x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                  map_smul' := sorry } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((HMul.hMul (α := End (End R (ι →₀ M)) (ι →₀ M))
                  { toFun := (⇑(mapRange.addMonoidHom (↑x : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                    map_smul' := sorry : LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
                  { toFun := (⇑(mapRange.addMonoidHom (↑x_1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                    map_smul' := sorry : LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
⊢ Eq (α := End (End R (ι →₀ M)) (ι →₀ M))
    { toFun := (⇑(mapRange.addMonoidHom (↑0 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } 0
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑0 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry, map_smul' := sorry } :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((0 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
x x_1 : End (End R M) M
⊢ { toFun := (⇑(mapRange.addMonoidHom (↑(x + x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := End (End R (ι →₀ M)) (ι →₀ M))
      { toFun := (⇑(mapRange.addMonoidHom (↑x : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
      { toFun := (⇑(mapRange.addMonoidHom (↑x_1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
have h : ∀ (x_2 : ι →₀ M) (a : ι),
  Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x + x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                  map_smul' := sorry } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((HAdd.hAdd (α := End (End R (ι →₀ M)) (ι →₀ M))
                  { toFun := (⇑(mapRange.addMonoidHom (↑x : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                    map_smul' := sorry : LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) }
                  { toFun := (⇑(mapRange.addMonoidHom (↑x_1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := sorry,
                    map_smul' := sorry : LinearMap (R := End R (ι →₀ M)) (RingHom.id (End R (ι →₀ M))) (ι →₀ M) (ι →₀ M) } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g_1 : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g_1
⊢ Eq.{u_6 + 1} (α := M) ((((f : (a : ι →₀ M) → ι →₀ M) (single i (g_1 • m)) : ι →₀ M) : (a : ι) → M) i : M)
    ((((g : (a : ι →₀ M) → ι →₀ M) ((f : (a : ι →₀ M) → ι →₀ M) (single i m)) : ι →₀ M) : (a : ι) → M) i : M)
have rw : Eq.{u_6 + 1} (α := M) ((((f : (a : ι →₀ M) → ι →₀ M) (single i (g_1 • m)) : ι →₀ M) : (a : ι) → M) i : M)
  ((((f : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) : ι →₀ M) : (a : ι) → M) i : M)
Tactic: rw [← End.smul_def g, ← map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
i : ι
x : End (End R M) M
⊢ (fun (f : End (End R (ι →₀ M)) (ι →₀ M)) ↦
        ({ toFun := fun (m : M) ↦ (((f : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) : (a : ι) → M) i, map_add' := ⋯,
            map_smul' := ⋯ } :
          LinearMap (R := End R M) (RingHom.id (End R M)) M M))
      (OneHom.toFun
        (↑(↑(ringHomEndFinsupp ι) : End (End R M) M →* End (End R (ι →₀ M)) (ι →₀ M)) :
          OneHom (End (End R M) M) (End (End R (ι →₀ M)) (ι →₀ M)))
        x) =
    x
have h : ∀ (x_1 : M),
  Eq (α := M)
    (((fun (f : End (End R (ι →₀ M)) (ι →₀ M)) ↦
              ({ toFun := fun (m : M) ↦ (((f : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) : (a : ι) → M) i,
                  map_add' := sorry, map_smul' := sorry } :
                LinearMap (R := End R M) (RingHom.id (End R M)) M M))
            (OneHom.toFun
              (↑(↑(ringHomEndFinsupp ι) : End (End R M) M →* End (End R (ι →₀ M)) (ι →₀ M)) :
                OneHom (End (End R M) M) (End (End R (ι →₀ M)) (ι →₀ M)))
              x) :
          (a : M) → M)
        x_1 :
      M)
    ((x : (a : M) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ OneHom.toFun
      (↑(↑(ringHomEndFinsupp ι) : End (End R M) M →* End (End R (ι →₀ M)) (ι →₀ M)) :
        OneHom (End (End R M) M) (End (End R (ι →₀ M)) (ι →₀ M)))
      ((fun (f : End (End R (ι →₀ M)) (ι →₀ M)) ↦
          ({ toFun := fun (m : M) ↦ (((f : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) : (a : ι) → M) i,
              map_add' := ⋯, map_smul' := ⋯ } :
            LinearMap (R := End R M) (RingHom.id (End R M)) M M))
        f) =
    f
have h : ∀ (x : ι →₀ M) (j : ι),
  Eq.{u_6 + 1} (α := M)
    ((((OneHom.toFun
                  (↑(↑(ringHomEndFinsupp ι) : End (End R M) M →* End (End R (ι →₀ M)) (ι →₀ M)) :
                    OneHom (End (End R M) M) (End (End R (ι →₀ M)) (ι →₀ M)))
                  ((fun (f : End (End R (ι →₀ M)) (ι →₀ M)) ↦
                      ({ toFun := fun (m : M) ↦ (((f : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) : (a : ι) → M) i,
                          map_add' := sorry, map_smul' := sorry } :
                        LinearMap (R := End R M) (RingHom.id (End R M)) M M))
                    f) :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        j :
      M)
    ((((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) j : M)
Tactic: ext x j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ Eq.{u_6 + 1} (α := M)
    ((((OneHom.toFun
                  (↑(↑(ringHomEndFinsupp ι) : End (End R M) M →* End (End R (ι →₀ M)) (ι →₀ M)) :
                    OneHom (End (End R M) M) (End (End R (ι →₀ M)) (ι →₀ M)))
                  ((fun (f : End (End R (ι →₀ M)) (ι →₀ M)) ↦
                      ({ toFun := fun (m : M) ↦ (((f : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) : (a : ι) → M) i,
                          map_add' := ⋯, map_smul' := ⋯ } :
                        LinearMap (R := End R M) (RingHom.id (End R M)) M M))
                    f) :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        j :
      M)
    ((((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) j : M)
have h : Eq.{u_6 + 1} (α := M)
  ((((f : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (α := (ι →₀ M) →ₗ[R] ι →₀ M) (lsingle i ∘ₗ lapply j) x) : ι →₀ M) :
        (a : ι) → M)
      i :
    M)
  ((((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) j : M)
Tactic: change f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ Eq.{u_6 + 1} (α := M)
    ((((f : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (α := (ι →₀ M) →ₗ[R] ι →₀ M) (lsingle i ∘ₗ lapply j) x) : ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) j : M)
have h : Eq.{u_6 + 1} (α := M)
  ((HSMul.hSMul (α := (ι →₀ M) →ₗ[R] ι →₀ M) (β := ι →₀ M) (lsingle i ∘ₗ lapply j)
          ((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) :
        (a : ι) → M)
      i :
    M)
  ((((f : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) j : M)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f
have inl : IsEmpty ι → ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f
Tactic: obtain _ | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End (End R (ι →₀ M)) (ι →₀ M)
inl :
  IsEmpty ι →
    ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f
have inr : ∀ (i : ι), ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f
Tactic: obtain _ | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ((c • v).sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂)) =
    HSMul.hSMul.{u_4, u_6, u_6} (α := R₂) (β := M₂) ((σ : (a : R) → R₂) c : R₂)
      (v.sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂))
have rw : Eq.{u_6 + 1} (α := M₂) (v.sum fun (i : α) (c_1 : M) ↦ (h i : (a : M) → M₂) (c • c_1))
  (v.sum fun (a : α) (b : M) ↦
    HSMul.hSMul.{u_4, u_6, u_6} (α := R₂) (β := M₂) ((σ : (a : R) → R₂) c : R₂) ((h a : (a : M) → M₂) b : M₂))
Tactic: rw [Finsupp.sum_smul_index', Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
rw :
  Eq.{u_6 + 1} (α := M₂) (v.sum fun (i : α) (c_1 : M) ↦ (h i : (a : M) → M₂) (c • c_1))
    (v.sum fun (a : α) (b : M) ↦
      HSMul.hSMul.{u_4, u_6, u_6} (α := R₂) (β := M₂) ((σ : (a : R) → R₂) c : R₂) ((h a : (a : M) → M₂) b : M₂))
⊢ ((c • v).sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂)) =
    HSMul.hSMul.{u_4, u_6, u_6} (α := R₂) (β := M₂) ((σ : (a : R) → R₂) c : R₂)
      (v.sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂))
have rw₁ : ∀ (i : α), Eq.{u_6 + 1} (α := M₂) ((h i : (a : M) → M₂) 0 : M₂) (0 : M₂)
Tactic: rw [Finsupp.sum_smul_index', Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
| HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) m : N)
have rw : m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)
Tactic: rw [← sum_single m, map_finsuppSum, smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ (f : (a : ι →₀ M) → N) (r • m) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) m : N)
have conv_rhs : Eq.{u_12 + 1} (α := N) ((f : (a : ι →₀ M) → N) (r • m) : N)
  (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N) : N)
Tactic: conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ Eq.{u_12 + 1} (α := N) ((f : (a : ι →₀ M) → N) (r • m) : N)
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N) : N)
have erw : Eq.{u_12 + 1} (α := N) (m.sum fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b)))
  (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N))
Tactic: erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ Eq.{u_12 + 1} (α := N) (m.sum fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b)))
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N))
have e_g : Eq (α := ι → M → N) (fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b))) fun (a : ι) (b : M) ↦
  HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ Eq (α := ι → M → N) (fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b))) fun (a : ι) (b : M) ↦
    HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)
have e_g : ∀ (i : ι) (m : M),
  (f : (a : ι →₀ M) → N) (single i (r • m)) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single i m) : N)
Tactic: ext i m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMul R M
inst_16 : SMulZeroClass R N
inst_17 : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
⊢ (f : (a : M) → ι →₀ N) (r • m) = HSMul.hSMul (β := ι →₀ N) r ((f : (a : M) → ι →₀ N) m : ι →₀ N)
have h : ∀ (i : ι),
  Eq.{u_12 + 1} (α := N) ((((f : (a : M) → ι →₀ N) (r • m) : ι →₀ N) : (a : ι) → N) i : N)
    ((HSMul.hSMul (β := ι →₀ N) r ((f : (a : M) → ι →₀ N) m : ι →₀ N) : (a : ι) → N) i : N)
Tactic: ext i