awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
h_1 : b ≠ 0
hf :
  (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)
have ha : (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
    (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b) + c • f) =
  HSMul.hSMul (β := N) c
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) : N)
Tactic: rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
h_1 : b ≠ 0
hf :
  (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)
ha :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b) + c • f) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + 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)
have ha₁ : HAdd.hAdd (α := N) (β := N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
        (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
      N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
  HSMul.hSMul (β := N) c
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) : N)
Tactic: rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
h_1 : b ≠ 0
hf :
  (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)
ha :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b) + c • f) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
ha₁ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + 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)
have ha₂ : HAdd.hAdd (α := N) (β := N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
        (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
      N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
  c •
    HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) : N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
Tactic: rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
h_1 : b ≠ 0
hf :
  (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)
ha :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b) + c • f) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
ha₁ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
ha₂ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    c •
      HAdd.hAdd (α := N) (β := N)
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) : N)
        ((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)
have ha₃ : HAdd.hAdd (α := N) (β := N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
        (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
      N)
    ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
  HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) : N) +
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
Tactic: rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 }
have refine : ∀ (i : ι),
  { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((F + G) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
        map_add' := sorry, map_smul' := sorry } ∘ₗ
      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' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N }
        { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
          map_add' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
      lsingle (M := M) i
Tactic: refine DFinsupp.lhom_ext' (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 : ι
⊢ { 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
have 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' := sorry, map_smul' := sorry } ∘ₗ
            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' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N }
              { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ (G i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
                map_add' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 }
have refine : ∀ (i : ι),
  { toFun := (⇑(sumAddHom (β := M) fun (i : ι) ↦ ((c • F) i).toAddMonoidHom) : (a : Π₀ (i : ι), M i) → N),
        map_add' := sorry, map_smul' := sorry } ∘ₗ
      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' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
      lsingle (M := M) i
Tactic: refine DFinsupp.lhom_ext' (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 : ι
⊢ { 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
have 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' := sorry, map_smul' := sorry } ∘ₗ
            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' := sorry, map_smul' := sorry : (Π₀ (i : ι), M i) →ₗ[R] N } ∘ₗ
            lsingle (M := M) i :
          (a : M i) → N)
        x :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ (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
have 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' := sorry, map_smul' := sorry } :
                  (Π₀ (i : ι), M i) →ₗ[R] N))
              F)
            x :
          (a : M x) → N)
        x_1 :
      N)
    ((F x : (a : M x) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
have 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' := sorry, map_smul' := sorry } :
            (Π₀ (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: refine DFinsupp.lhom_ext' (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 : ι
⊢ (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
have 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' := sorry, map_smul' := sorry } :
                  (Π₀ (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: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
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 ι
m : Π₀ (i : ι), M i
h : Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) ⊤ m
⊢ Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) (⨆ (i : ι), LinearMap.range (lsingle (M := M) i)) m
have rw : Membership.mem (α := Π₀ (i : ι), M i) (γ := Submodule R (Π₀ (i : ι), M i))
  (⨆ (i : ι), LinearMap.range (lsingle (M := M) i))
  ((((lsum ℕ (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) :
        (a : Π₀ (i : ι), M i) → Π₀ (i : ι), M i)
      m :
    Π₀ (i : ι), M i)
Tactic: rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₁ i)) (AddMonoidHom.mker (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₁ i) →+ (i : ι) → β₁ i) (coeFnAddMonoidHom (β := β₁))
      (AddSubmonoid.pi (M := β₁) Set.univ fun (i : ι) ↦ AddMonoidHom.mker (f i)))
have h : ∀ (x : Π₀ (i : ι), β₁ i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₁ i))
      (AddMonoidHom.mker (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₁ i))
      (AddSubmonoid.comap (F := (Π₀ (i : ι), β₁ i) →+ (i : ι) → β₁ i) (coeFnAddMonoidHom (β := β₁))
        (AddSubmonoid.pi (M := β₁) Set.univ fun (i : ι) ↦ AddMonoidHom.mker (f i)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₂ i)) (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
have h : ∀ (x : Π₀ (i : ι), β₂ i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
        (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
        (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
      x
have h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
Tactic: simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]