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 : 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 : Π₀ (i : ι), ↥(p i)) : (a : ι) → ↥(p a)) i
have h₁ : -(m : (a : ι) → ↥(p a)) i = 0
Tactic: rw [DFinsupp.zero_apply, ← neg_eq_zero]
-- 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)
i : ι
⊢ -(m : (a : ι) → ↥(p a)) i = 0
have h₁ : ((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 m) =
  (↑(-(m : (a : ι) → ↥(p a)) i) : N)
Tactic: refine h i (-m i) m ?_
-- 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)
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 m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
have h₁ : ∀
  (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)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i m + single (β := fun (i : ι) ↦ ↥(p i)) i ((m : (a : ι) → ↥(p a)) i)) :
        N)
      (0 : 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 m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
Tactic: rwa [← erase_add_single i m, map_add, lsum_single, Submodule.subtype_apply,
    add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm
Cleared hypotheses: hm
-- 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)
i : ι
h₁ :
  ∀
    (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)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i m + single (β := fun (i : ι) ↦ ↥(p i)) i ((m : (a : ι) → ↥(p a)) i)) :
          N)
        (0 : 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 m) =
      (↑(-(m : (a : ι) → ↥(p a)) 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)
      (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
have h₂ : ∀
  (hm :
    HAdd.hAdd (α := N) (β := 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 m) :
          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 ((m : (a : ι) → ↥(p a)) i)) :
          N) =
      0),
  ((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 m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
Tactic: rwa [← erase_add_single i m, map_add, lsum_single, Submodule.subtype_apply,
    add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)
have h₁ : iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)
Tactic: rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] 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 : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have simp_rw : (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: simp_rw [iSupIndep_def, Submodule.disjoint_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have mp : (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) →
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
mp :
  (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
⊢ (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have mpr : (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) →
  ∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0
i : ι
hi : i ∈ s
⊢ v i = 0
have mp : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (v i)
Tactic: apply h _ _ (hv i hi)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0
i : ι
hi : i ∈ s
⊢ Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (v i)
have hv0₁ : -v i = ∑ x ∈ s.erase i, v x
Tactic: rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
Cleared hypotheses: hv0, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (v i)
have mp : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (∑ x ∈ s.erase i, v x)
Tactic: rw [← Submodule.neg_mem_iff, hv0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
i : ι
x : N
hx : x ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x
⊢ x = 0
have mpr : ∀ (f : ι →₀ N)
  (hf :
    ∀ (i_1 : ι),
      Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N))
  (hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i)
  (hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)),
  Eq (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
Tactic: obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
Cleared hypotheses: x, hx, hsup
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
⊢ Eq (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
have mpr : ∀ (h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0),
  ∃ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) ∧ Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 ∧ ∃ i ∈ s, v i ≠ 0
Tactic: contrapose! 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 : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
⊢ ∃ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) ∧ Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 ∧ ∃ i ∈ s, v i ≠ 0
have h₁ : (∀ i_1 ∈ insert i f.support,
    (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1 ∈ p i_1) ∧
  Eq.{u_6 + 1} (α := N)
      (∑ i_1 ∈ insert i f.support,
        (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
      0 ∧
    ∃ i_1 ∈ insert i f.support,
      Ne.{u_6 + 1} (α := N)
        ((fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1) 0
Tactic: use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
⊢ (∀ i_1 ∈ insert i f.support,
      (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1 ∈ p i_1) ∧
    Eq.{u_6 + 1} (α := N)
        (∑ i_1 ∈ insert i f.support,
          (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
        0 ∧
      ∃ i_1 ∈ insert i f.support,
        Ne.{u_6 + 1} (α := N)
          ((fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1) 0
have h₁ : ∀ (j : ι) (hj : j ∈ insert i f.support),
  (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) j ∈ p j
Tactic: refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
h₁ :
  ∀ (j : ι) (hj : j ∈ insert i f.support),
    (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) j ∈ p j
⊢ (∀ i_1 ∈ insert i f.support,
      (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1 ∈ p i_1) ∧
    Eq.{u_6 + 1} (α := N)
        (∑ i_1 ∈ insert i f.support,
          (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
        0 ∧
      ∃ i_1 ∈ insert i f.support,
        Ne.{u_6 + 1} (α := N)
          ((fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1) 0
have h₂ : Eq.{u_6 + 1} (α := N)
  (∑ i_1 ∈ insert i f.support,
    (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
  0
Tactic: refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
j : ι
hj : j ∈ insert i f.support
⊢ Membership.mem (α := N) (p j) (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)
have pos : ∀ (h : j = i), (-f.sum fun (x : ι) (x_1 : N) ↦ x_1) ∈ p j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
j : ι
hj : j ∈ insert i f.support
pos : ∀ (h : j = i), (-f.sum fun (x : ι) (x_1 : N) ↦ x_1) ∈ p j
⊢ Membership.mem (α := N) (p j) (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)
have neg : ∀ (h : ¬j = i), Membership.mem (α := N) (p j) ((f : (a : ι) → N) j : N)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf :
  ∀ (i_1 : ι),
    Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i_1 ≠ i), p i_1) ((f : (a : ι) → N) i_1 : N)
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
⊢ Eq.{u_6 + 1} (α := N)
    (∑ i_1 ∈ insert i f.support,
      (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
    0
have hf₁ : Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i ≠ i), p i) ((f : (a : ι) → N) i : N)
Tactic: specialize hf i
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hx : (f.sum fun (_i : ι) (xi : N) ↦ xi) ∈ p i
hsup : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (f.sum fun (_i : ι) (xi : N) ↦ xi)
h : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
hf : Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i ≠ i), p i) ((f : (a : ι) → N) i : N)
⊢ Eq.{u_6 + 1} (α := N)
    (∑ i_1 ∈ insert i f.support,
      (fun (j : ι) ↦ (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)) i_1)
    0
have hf₁ : Eq.{u_6 + 1} (α := N) ((f : (a : ι) → N) i : N) (0 : N)
Tactic: simp at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have simp_rw : (∀ (i : ι), Disjoint (p i) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j)) ↔
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: classical
  simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
simp_rw :
  (∀ (i : ι), Disjoint (p i) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j)) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have simp_rw₁ : (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: classical
  simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]