awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
h :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_6 + 1} (α := M)
      (((({ toFun := (⇑(mapRange.addMonoidHom (↑1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } :
                  (a : ι →₀ M) → ι →₀ M)
                x :
              ι →₀ M) :
            (a : ι) → M)
          a :
        M)
      ((((1 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
⊢ Eq (α := End (End R (ι →₀ M)) (ι →₀ M))
    { toFun := (⇑(mapRange.addMonoidHom (↑1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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 : ι →₀ M
a : ι
⊢ Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑1 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((1 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
h :
  ∀ (x_2 : ι →₀ M) (a : ι),
    Eq.{u_6 + 1} (α := M)
      (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x * x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (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' := ⋯,
                      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) } :
                  (a : ι →₀ M) → ι →₀ M)
                x_2 :
              ι →₀ M) :
            (a : ι) → M)
          a :
        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) }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
x_2 : ι →₀ M
a : ι
⊢ Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x * x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (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' := ⋯,
                    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) } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
h :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_6 + 1} (α := M)
      (((({ toFun := (⇑(mapRange.addMonoidHom (↑0 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } :
                  (a : ι →₀ M) → ι →₀ M)
                x :
              ι →₀ M) :
            (a : ι) → M)
          a :
        M)
      ((((0 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
⊢ Eq (α := End (End R (ι →₀ M)) (ι →₀ M))
    { toFun := (⇑(mapRange.addMonoidHom (↑0 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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 : ι →₀ M
a : ι
⊢ Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑0 : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯, map_smul' := ⋯ } :
                (a : ι →₀ M) → ι →₀ M)
              x :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)
    ((((0 : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
h :
  ∀ (x_2 : ι →₀ M) (a : ι),
    Eq.{u_6 + 1} (α := M)
      (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x + x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (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' := ⋯,
                      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) } :
                  (a : ι →₀ M) → ι →₀ M)
                x_2 :
              ι →₀ M) :
            (a : ι) → M)
          a :
        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) }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
x_2 : ι →₀ M
a : ι
⊢ Eq.{u_6 + 1} (α := M)
    (((({ toFun := (⇑(mapRange.addMonoidHom (↑(x + x_1) : M →+ M)) : (a : ι →₀ M) → ι →₀ M), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (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' := ⋯,
                    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) } :
                (a : ι →₀ M) → ι →₀ M)
              x_2 :
            ι →₀ M) :
          (a : ι) → M)
        a :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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 x_1 : M
⊢ (((f : (a : ι →₀ M) → ι →₀ M) (single i (x + x_1)) : ι →₀ M) : (a : ι) → M) i =
    HAdd.hAdd (α := M) (β := M) ((((f : (a : ι →₀ M) → ι →₀ M) (single i x) : ι →₀ M) : (a : ι) → M) i : M)
      ((((f : (a : ι →₀ M) → ι →₀ M) (single i x_1) : ι →₀ M) : (a : ι) → M) i : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
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)
⊢ 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)

Tactic:
rw [← End.smul_def g, ← map_smul]

Premises used: Module.End.smul_def, map_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
    ((((f : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) : ι →₀ M) : (a : ι) → M) i : M)

Tactic:
simp [g]
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
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' := ⋯, 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) :
            (a : M) → M)
          x_1 :
        M)
      ((x : (a : M) → M) x_1 : 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

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
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' := ⋯, 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) :
          (a : M) → M)
        x_1 :
      M)
    ((x : (a : M) → M) x_1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
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' := ⋯, 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)
⊢ 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

Tactic:
ext x j
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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 : ι
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)
⊢ 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)

Tactic:
change f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _

Premises used: LinearMap.comp, HSMul.hSMul, Finsupp.lapply, DFunLike.coe, Finsupp.lsingle
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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 : ι
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)
⊢ 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:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
    ((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:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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
inr :
  ∀ (i : ι),
    ∃ (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

Tactic:
obtain _ | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
h : IsEmpty ι
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f

Tactic:
⟨0, Subsingleton.elim ..⟩

Premises used: Exists.intro, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
h : IsEmpty ι
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f

Tactic:
exact ⟨0, Subsingleton.elim ..⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
i : ι
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f

Tactic:
⟨_, (ringEquivEndFinsupp i).right_inv f⟩

Premises used: RingEquiv.toEquiv, Equiv.right_inv, Module.End.ringEquivEndFinsupp, Exists.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
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)
i : ι
⊢ ∃ (a : End (End R M) M), (ringHomEndFinsupp ι : (a : End (End R M) M) → End (End R (ι →₀ M)) (ι →₀ M)) a = f

Tactic:
exact ⟨_, (ringEquivEndFinsupp i).right_inv f⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_5
inst : Zero β
inst_1 : AddCommMonoid M
inst_2 : DistribSMul R M
v : α →₀ β
c : R
h : α → β → M
⊢ c • v.sum h = v.sum fun (a : α) (b : β) ↦ c • h a b

Tactic:
Finset.smul_sum

Premises used: Finsupp.sum, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
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₂))
rw₁ : ∀ (i : α), Eq.{u_6 + 1} (α := M₂) ((h i : (a : M) → M₂) 0 : M₂) (0 : 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₂))

Tactic:
rw [Finsupp.sum_smul_index', Finsupp.smul_sum]

Premises used: Finsupp.sum_smul_index', Finsupp.smul_sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
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₂
⊢ 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:
simp only [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
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₂
i : α
⊢ Eq.{u_6 + 1} (α := M₂) ((h i : (a : M) → M₂) 0 : M₂) (0 : M₂)

Tactic:
(h i).map_zero

Premises used: LinearMap.map_zero
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
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₂
i : α
⊢ Eq.{u_6 + 1} (α := M₂) ((h i : (a : M) → M₂) 0 : M₂) (0 : M₂)

Tactic:
exact (h i).map_zero

Premises used: LinearMap.map_zero