awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
mpr :
  Eq.{u_6 + 1} (α := N)
    (∑ x ∈ s,
      (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
                Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                  (↑(μ (↑i : ι)) : N) ⋯ :
              (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
            x) :
        N))
    (∑ i ∈ s, (↑(μ i) : N))
⊢ ∑
      x ∈
        support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
          (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
            Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
              (↑(μ (↑i : ι)) : N) ⋯),
      (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
                Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                  (↑(μ (↑i : ι)) : N) ⋯ :
              (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
            x) :
        N) =
    a
have mpr₁ : ∀ x ∈ s,
  x ∉
      support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
        (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
            (↑(μ (↑i : ι)) : N) sorry) →
    (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
                Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                  (↑(μ (↑i : ι)) : N) sorry :
              (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
            x) :
        N) =
      0
Tactic: rw [Finset.sum_subset support_mk_subset, ← hμ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
x : ι
hx : x ∈ s
⊢ (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                (↑(μ (↑i : ι)) : N) ⋯ :
            (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
          x) :
      N) =
    (↑(μ x) : N)
have rw : (↑(Subtype.mk (p := fun (x_1 : N) ↦
        Membership.mem (γ := Submodule R N)
          (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) x hx) : ι) ∈ s),
            p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) x hx) : ι))
          x_1)
        (↑(μ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) x hx) : ι)) : N) sorry) :
    N) =
  (↑(μ x) : N)
Tactic: rw [mk_of_mem hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
x : ι
h : x ∈ s
hx :
  x ∉
    support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
        Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
          (↑(μ (↑i : ι)) : N) ⋯)
⊢ (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                (↑(μ (↑i : ι)) : N) ⋯ :
            (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
          x) :
      N) =
    0
have hx₁ : (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
        Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
          (↑(μ (↑i : ι)) : N) sorry :
      (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
    x =
  0
Tactic: rw [mem_support_iff, not_ne_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
x : ι
h : x ∈ s
hx :
  (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
            (↑(μ (↑i : ι)) : N) ⋯ :
        (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
      x =
    0
⊢ (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                (↑(μ (↑i : ι)) : N) ⋯ :
            (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
          x) :
      N) =
    0
have mpr : Eq.{u_6 + 1} (α := N) (↑0 : N) 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ Membership.mem (γ := Submodule R N) (⨆ i ∈ s, p i) a ↔ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have rw : (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
  ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
Tactic: classical
    rw [Submodule.mem_iSup_iff_exists_dfinsupp']
    constructor <;> rintro ⟨μ, hμ⟩
    · use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
    · refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
⊢ Membership.mem (γ := Submodule R N) (⨆ i ∈ s, p i) a ↔ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have mp : ∀ (μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i))
  (hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a),
  ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
Tactic: classical
    rw [Submodule.mem_iSup_iff_exists_dfinsupp']
    constructor <;> rintro ⟨μ, hμ⟩
    · use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
    · refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
mp :
  ∀ (μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i))
    (hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a),
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
⊢ Membership.mem (γ := Submodule R N) (⨆ i ∈ s, p i) a ↔ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have mpr : ∀ (μ : (i : ι) → ↥(p i)) (hμ : ∑ i ∈ s, (↑(μ i) : N) = a),
  ∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
Tactic: classical
    rw [Submodule.mem_iSup_iff_exists_dfinsupp']
    constructor <;> rintro ⟨μ, hμ⟩
    · use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
    · refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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
have simp_rw : (∀ (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: simp_rw [iSupIndep_def, Submodule.disjoint_def,
    Submodule.mem_biSup_iff_exists_dfinsupp, exists_imp, filter_ne_eq_erase]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 →
            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
have 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
Tactic: refine forall_congr' fun i => Subtype.forall'.trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
⊢ iSupIndep p
have 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
Tactic: rw [iSupIndep_iff_forall_dfinsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
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)
⊢ x = 0
have 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)
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
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
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)
⊢ x = 0
have this : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 p
have rw : iSupIndep (α := Submodule ℕ N) ((⇑AddSubmonoid.toNatSubmodule : (a : AddSubmonoid N) → Submodule ℕ N) ∘ p)
Tactic: rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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)
have 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) sorry)) ∘ₗ
                (↑(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: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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 p
have rw : iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)
Tactic: rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
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
⊢ 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)
have 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
Tactic: rw [iSupIndep_iff_forall_dfinsupp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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)
have 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))
  ⊥
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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))
    ⊥
have 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
Tactic: rw [LinearMap.ker_eq_bot']
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
⊢ m = 0
have h₁ : ∀ (i : ι), (m : (a : ι) → ↥(p a)) i = ((0 : Π₀ (i : ι), ↥(p i)) : (a : ι) → ↥(p a)) i
Tactic: ext i : 1