awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
refine :
  ∀ (i : ι),
    (∀ (x : ↥(p i)) (x_1 : Π₀ (i : ι), ↥(p i)),
        ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype :
                (a : Π₀ (i : ι), ↥(p i)) → N)
              (erase (β := fun (i : ι) ↦ ↥(p i)) i x_1) =
            (↑x : N) →
          (↑x : N) = 0) ↔
      ∀ (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
        ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype :
                (a : Π₀ (i : ι), ↥(p i)) → N)
              (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
            (↑x : N) →
          x = 0
⊢ (∀ (i : ι),
      ∀ x ∈ p i,
        ∀ (x_1 : Π₀ (i : ι), ↥(p i)),
          ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                    fun (i : ι) ↦ (p i).subtype :
                  (a : Π₀ (i : ι), ↥(p i)) → N)
                (erase (β := fun (i : ι) ↦ ↥(p i)) i x_1) =
              x →
            x = 0) ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
          (↑x : N) →
        x = 0

Tactic:
refine forall_congr' fun i => Subtype.forall'.trans ?_

Premises used: forall_congr', Iff.trans, Subtype.forall'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
i : ι
⊢ (∀ (x : ↥(p i)) (x_1 : Π₀ (i : ι), ↥(p i)),
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i x_1) =
          (↑x : N) →
        (↑x : N) = 0) ↔
    ∀ (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
          (↑x : N) →
        x = 0

Tactic:
simp_rw [Submodule.coe_eq_zero]

Premises used: Submodule.coe_eq_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
rw :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
⊢ iSupIndep p

Tactic:
rw [iSupIndep_iff_forall_dfinsupp]

Premises used: iSupIndep_iff_forall_dfinsupp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv :
  ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
    (↑x : N)
⊢ Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i v) :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (single (β := fun (i : ι) ↦ ↥(p i)) i x) :
      N)

Tactic:
simpa only [lsum_single] using hv

Premises used: DFinsupp.lsum_single
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv :
  ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
    (↑x : N)
⊢ Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i v) :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (single (β := fun (i : ι) ↦ ↥(p i)) i x) :
      N)

Tactic:
replace hv : lsum ℕ (fun i => (p i).subtype) (erase i v) =
      lsum ℕ (fun i => (p i).subtype) (single i x) := by
    simpa only [lsum_single] using hv
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i v) :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (single (β := fun (i : ι) ↦ ↥(p i)) i x) :
      N)
⊢ (erase (β := fun (i : ι) ↦ ↥(p i)) i v : (a : ι) → ↥(p a)) i =
    (single (β := fun (i : ι) ↦ ↥(p i)) i x : (a : ι) → ↥(p a)) i

Tactic:
have := DFunLike.ext_iff.mp (h hv) i
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i v) :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (single (β := fun (i : ι) ↦ ↥(p i)) i x) :
      N)
this :
  (erase (β := fun (i : ι) ↦ ↥(p i)) i v : (a : ι) → ↥(p a)) i =
    (single (β := fun (i : ι) ↦ ↥(p i)) i x : (a : ι) → ↥(p a)) i
⊢ x = 0

Tactic:
simpa [eq_comm] using this

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommMonoid N
p : ι → AddSubmonoid N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
rw : iSupIndep (α := Submodule ℕ N) ((⇑AddSubmonoid.toNatSubmodule : (a : AddSubmonoid N) → Submodule ℕ N) ∘ p)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]

Premises used: AddSubmonoid.toNatSubmodule, iSupIndep_map_orderIso_iff
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommMonoid N
p : ι → AddSubmonoid N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ iSupIndep (α := Submodule ℕ N) ((⇑AddSubmonoid.toNatSubmodule : (a : AddSubmonoid N) → Submodule ℕ N) ∘ p)

Tactic:
iSupIndep_of_dfinsupp_lsum_injective _ h

Premises used: iSupIndep_of_dfinsupp_lsum_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommMonoid N
p : ι → AddSubmonoid N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ iSupIndep (α := Submodule ℕ N) ((⇑AddSubmonoid.toNatSubmodule : (a : AddSubmonoid N) → Submodule ℕ N) ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
h :
  ∀ (a : ι),
    Eq.{u_6 + 1} (α := N)
      (((((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype) ∘ₗ
                (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
                    LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯)) ∘ₗ
                  (↑(finsuppLequivDFinsupp R) : (ι →₀ R) →ₗ[R] Π₀ (x : ι), R)) ∘ₗ
              Finsupp.lsingle a :
            (a : R) → N)
          1 :
        N)
      ((Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a : (a : R) → N) 1 : N)
⊢ Eq (α := (ι →₀ R) →ₗ[R] N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
        (p i).subtype) ∘ₗ
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯)) ∘ₗ
        (↑(finsuppLequivDFinsupp R) : (ι →₀ R) →ₗ[R] Π₀ (x : ι), R))
    (Finsupp.linearCombination R v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a : ι
⊢ Eq.{u_6 + 1} (α := N)
    (((((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype) ∘ₗ
              (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
                  LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯)) ∘ₗ
                (↑(finsuppLequivDFinsupp R) : (ι →₀ R) →ₗ[R] Π₀ (x : ι), R)) ∘ₗ
            Finsupp.lsingle a :
          (a : R) → N)
        1 :
      N)
    ((Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a : (a : R) → N) 1 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
rw : iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]

Premises used: iSupIndep_map_orderIso_iff, AddSubgroup.toIntSubmodule
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)

Tactic:
iSupIndep_of_dfinsupp_lsum_injective _ h

Premises used: iSupIndep_of_dfinsupp_lsum_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
h :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h : iSupIndep p
⊢ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0

Tactic:
rw [iSupIndep_iff_forall_dfinsupp] at h

Premises used: iSupIndep_iff_forall_dfinsupp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
this :
  Eq (α := Submodule R (Π₀ (i : ι), ↥(p i)))
    (LinearMap.ker (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype))
    ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
rw [LinearMap.ker_eq_bot] at this

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
this
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this :
  Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
suffices :
  Eq (α := Submodule R (Π₀ (i : ι), ↥(p i)))
    (LinearMap.ker (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype))
    ⊥
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
suffices LinearMap.ker (lsum ℕ fun i => (p i).subtype) = ⊥ by
    -- Lean can't find this without our help
    letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance
    rw [LinearMap.ker_eq_bot] at this
    exact this
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
rw :
  ∀ (m : Π₀ (i : ι), ↥(p i)),
    Eq.{u_6 + 1} (α := N)
        (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            m :
          N)
        (0 : N) →
      m = 0
⊢ Eq (α := Submodule R (Π₀ (i : ι), ↥(p i)))
    (LinearMap.ker (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype))
    ⊥

Tactic:
rw [LinearMap.ker_eq_bot']

Premises used: LinearMap.ker_eq_bot'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
m : Π₀ (i : ι), ↥(p i)
hm :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        m :
      N)
    (0 : N)
h₁ : ∀ (i : ι), (m : (a : ι) → ↥(p a)) i = ((0 : Π₀ (i : ι), ↥(p i)) : (a : ι) → ↥(p a)) i
⊢ m = 0

Tactic:
ext i : 1
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
m : Π₀ (i : ι), ↥(p i)
hm :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        m :
      N)
    (0 : N)
i : ι
h₁ : -(m : (a : ι) → ↥(p a)) i = 0
⊢ (m : (a : ι) → ↥(p a)) i = ((0 : Π₀ (i : ι), ↥(p i)) : (a : ι) → ↥(p a)) i

Tactic:
rw [DFinsupp.zero_apply, ← neg_eq_zero]

Premises used: DFinsupp.zero_apply, neg_eq_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
m : Π₀ (i : ι), ↥(p i)
hm :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        m :
      N)
    (0 : N)
i : ι
⊢ -(m : (a : ι) → ↥(p a)) i = 0

Tactic:
h i (-m i) m ?_

Premises used: DFunLike.coe, Neg.neg