awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
h0 :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
h0₁ : 0 = HSMul.hSMul (β := N) c 0
h0₂ h0₃ : Eq.{u_6 + 1} (α := N) 0 0
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)

Tactic:
rw [smul_zero, map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f_1 : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
ha :
  (f : (a : ι) → M a) a = 0 →
    b ≠ 0 →
      (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) →
        (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
            (c • (single (β := M) a b + f)) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
                (single (β := M) a b + f) :
              N)
⊢ (f : (a : ι) → M a) a = 0 →
    b ≠ 0 →
      (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) →
        (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
            (c • (single (β := M) a b + f)) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
                (single (β := M) a b + f) :
              N)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f_1 : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
h : (f : (a : ι) → M a) a = 0
ha :
  b ≠ 0 →
    (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
        HSMul.hSMul (β := N) c
          ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) →
      (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (c • (single (β := M) a b + f)) =
        HSMul.hSMul (β := N) c
          ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
              (single (β := M) a b + f) :
            N)
⊢ b ≠ 0 →
    (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
        HSMul.hSMul (β := N) c
          ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) →
      (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (c • (single (β := M) a b + f)) =
        HSMul.hSMul (β := N) c
          ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
              (single (β := M) a b + f) :
            N)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F G : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }

Tactic:
DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F G : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
refine :
  ∀ (i : ι),
    { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
        lsingle (M := M) i =
      HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
          { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
            map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
          { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
            map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
        lsingle (M := M) i
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F G : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
h :
  ∀ (x : M i),
    Eq.{u_6 + 1} (α := N)
      (({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
              lsingle (M := M) i :
            (a : M i) → N)
          x :
        N)
      ((HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
                { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                  map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
                { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                  map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
              lsingle (M := M) i :
            (a : M i) → N)
          x :
        N)
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      lsingle (M := M) i =
    HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
        { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
        { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
      lsingle (M := M) i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F G : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
x : M i
⊢ Eq.{u_6 + 1} (α := N)
    (({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)
    ((HAdd.hAdd (α := (Π₀ (i : ι), M i) →ₗ[R] N)
              { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }
              { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
c : S
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }

Tactic:
DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
c : S
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
refine :
  ∀ (i : ι),
    { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
        lsingle (M := M) i =
      HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
          { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
            map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
        lsingle (M := M) i
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
      { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N), map_add' := ⋯,
        map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N }

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
c : S
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
h :
  ∀ (x : M i),
    Eq.{u_6 + 1} (α := N)
      (({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
              lsingle (M := M) i :
            (a : M i) → N)
          x :
        N)
      ((HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
                { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                  map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
              lsingle (M := M) i :
            (a : M i) → N)
          x :
        N)
⊢ { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      lsingle (M := M) i =
    HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
        { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
      lsingle (M := M) i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
c : S
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
x : M i
⊢ Eq.{u_6 + 1} (α := N)
    (({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)
    ((HSMul.hSMul (α := S) (β := (Π₀ (i : ι), M i) →ₗ[R] N) ((RingHom.id S : (a : S) → S) c : S)
              { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
h :
  ∀ (x : ι) (x_1 : M x),
    Eq.{u_6 + 1} (α := N)
      (((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i)
              ((fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
                  ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                      map_add' := ⋯, map_smul' := ⋯ } :
                    (Π₀ (i : ι), M i) →ₗ[R] N))
                F)
              x :
            (a : M x) → N)
          x_1 :
        N)
      ((F x : (a : M x) → N) x_1 : N)
⊢ (fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i)
      ((fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
          ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
              map_add' := ⋯, map_smul' := ⋯ } :
            (Π₀ (i : ι), M i) →ₗ[R] N))
        F) =
    F

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
x : ι
x_1 : M x
⊢ Eq.{u_6 + 1} (α := N)
    (((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i)
            ((fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
                ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (Π₀ (i : ι), M i) →ₗ[R] N))
              F)
            x :
          (a : M x) → N)
        x_1 :
      N)
    ((F x : (a : M x) → N) x_1 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
⊢ (fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
        ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (Π₀ (i : ι), M i) →ₗ[R] N))
      ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) =
    F

Tactic:
DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
refine :
  ∀ (i : ι),
    (fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
            ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := ⋯, map_smul' := ⋯ } :
              (Π₀ (i : ι), M i) →ₗ[R] N))
          ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) ∘ₗ
        lsingle (M := M) i =
      F ∘ₗ lsingle (M := M) i
⊢ (fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
        ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (Π₀ (i : ι), M i) →ₗ[R] N))
      ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) =
    F

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Premises used: DFinsupp.lhom_ext'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
i : ι
h :
  ∀ (x : M i),
    Eq.{u_6 + 1} (α := N)
      (((fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
                  ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                      map_add' := ⋯, map_smul' := ⋯ } :
                    (Π₀ (i : ι), M i) →ₗ[R] N))
                ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) ∘ₗ
              lsingle (M := M) i :
            (a : M i) → N)
          x :
        N)
      ((F ∘ₗ lsingle (M := M) i : (a : M i) → N) x : N)
⊢ (fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
          ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
              map_add' := ⋯, map_smul' := ⋯ } :
            (Π₀ (i : ι), M i) →ₗ[R] N))
        ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) ∘ₗ
      lsingle (M := M) i =
    F ∘ₗ lsingle (M := M) i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
i : ι
x : M i
⊢ Eq.{u_6 + 1} (α := N)
    (((fun (F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N) ↦
                ({ toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (Π₀ (i : ι), M i) →ₗ[R] N))
              ((fun (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) ↦ F ∘ₗ lsingle (M := M) i) F) ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)
    ((F ∘ₗ lsingle (M := M) i : (a : M i) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
x : M i
⊢ Eq.{u_6 + 1} (α := N)
    ((((lsum S (M := M) : (a : (i : ι) → M i →ₗ[R] N) → (Π₀ (i : ι), M i) →ₗ[R] N) F : (Π₀ (i : ι), M i) →ₗ[R] N) :
          (a : Π₀ (i : ι), M i) → N)
        (single (β := M) i x) :
      N)
    ((F i : (a : M i) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
S : Type u_4
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
inst_4 : Semiring S
inst_5 : (i : ι) → Module.{u_4, u_5} S (M i)
inst_6 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_5} R S (M i)
⊢ Eq (α := (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
    ((lsum S (M := M) : (a : (i : ι) → M i →ₗ[R] Π₀ (i : ι), M i) → (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
        (lsingle (M := M)) :
      (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
    (LinearMap.id : (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)

Tactic:
lhom_ext (lsum_single _ _)

Premises used: DFinsupp.lsum_single, DFinsupp.lhom_ext