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 : 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₁ :
  ((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)
⊢ -(m : (a : ι) → ↥(p a)) i = 0

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

Premises used: DFunLike.coe, Neg.neg
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)

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

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 : iSupIndep (α := Submodule ℤ N) ((⇑AddSubgroup.toIntSubmodule : (a : AddSubgroup N) → Submodule ℤ N) ∘ p)
⊢ Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
h.dfinsupp_lsum_injective

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

Tactic:
exact h.dfinsupp_lsum_injective

Premises used: iSupIndep.dfinsupp_lsum_injective
-- 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
⊢ 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)

Tactic:
⟨iSupIndep.dfinsupp_lsum_injective, iSupIndep_of_dfinsupp_lsum_injective p⟩

Premises used: iSupIndep.dfinsupp_lsum_injective, Iff.intro, iSupIndep_of_dfinsupp_lsum_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ∀ 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
⊢ 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

Tactic:
simp_rw [iSupIndep_def, Submodule.disjoint_def]

Premises used: iSupIndep_def, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ (∀ (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
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
mp : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (v i)
⊢ v i = 0

Tactic:
apply h _ _ (hv i hi)
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 = ∑ x ∈ s.erase i, v x

Tactic:
rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0

Premises used: Finset.add_sum_erase, add_eq_zero_iff_neg_eq
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
hv0₁ : -v i = ∑ x ∈ s.erase i, v x
⊢ i ∈ s

Tactic:
rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0

Premises used: Finset.add_sum_erase, add_eq_zero_iff_neg_eq
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
mp : Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (∑ x ∈ s.erase i, v x)
⊢ Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) (v i)

Tactic:
rw [← Submodule.neg_mem_iff, hv0]

Premises used: Submodule.neg_mem_iff
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
⊢ ∀ i_1 ∈ s.erase i, i_1 ≠ i

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
⊢ ∀ i_1 ∈ s.erase i, v i_1 ∈ p i_1

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.DFinsupp
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) (∑ x ∈ s.erase i, v x)

Tactic:
exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)

Premises used: biSup_mono, SetLike.le_def, Submodule.sum_mem_biSup, Iff.mp
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ x = 0

Tactic:
obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup

Premises used: Submodule.mem_iSup_iff_exists_finsupp, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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
⊢ Eq (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.DFinsupp
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₁ :
  (∀ 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
⊢ ∃ (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:
use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j

Premises used: Finsupp.sum, Finsupp.support, Insert.insert, Eq, DFunLike.coe, Neg.neg, ite
-- Module: Mathlib.LinearAlgebra.DFinsupp
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,
    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:
grind
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ (∀ 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:
refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
h₁ : Membership.mem (α := N) (p j) (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)
⊢ (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:
beta_reduce
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
neg : ∀ (h : ¬j = i), Membership.mem (α := N) (p j) ((f : (a : ι) → N) j : N)
⊢ Membership.mem (α := N) (p j) (if j = i then -f.sum fun (x : ι) (x_1 : N) ↦ x_1 else (f : (a : ι) → N) j : N)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.DFinsupp
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_1 : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
j : ι
hj : j ∈ insert i f.support
h : j = i
⊢ (-f.sum fun (x : ι) (x_1 : N) ↦ x_1) ∈ p j

Tactic:
(p j).neg_mem (h ▸ hx)

Premises used: Eq.rec, Submodule.neg_mem, Eq.symm
-- Module: Mathlib.LinearAlgebra.DFinsupp
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_1 : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
j : ι
hj : j ∈ insert i f.support
h : j = i
⊢ (-f.sum fun (x : ι) (x_1 : N) ↦ x_1) ∈ p j

Tactic:
exact (p j).neg_mem (h ▸ hx)

Premises used: Submodule.neg_mem
-- Module: Mathlib.LinearAlgebra.DFinsupp
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_1 : Ne (α := N) (f.sum fun (_i : ι) (xi : N) ↦ xi) 0
j : ι
hj : j ∈ insert i f.support
h : ¬j = i
⊢ Membership.mem (α := N) (p j) ((f : (a : ι) → N) j : N)

Tactic:
simpa [h] using hf j
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
⊢ Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (_ : i ≠ i), p i) ((f : (a : ι) → N) i : N)

Tactic:
specialize hf i
-- Module: Mathlib.LinearAlgebra.DFinsupp
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) ((f : (a : ι) → N) i : N) (0 : N)

Tactic:
simp at hf
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : Eq.{u_6 + 1} (α := N) ((f : (a : ι) → N) i : N) (0 : 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

Tactic:
grind [Finsupp.sum, Finset.sum_congr]

Premises used: Finsupp.sum, Finset.sum_congr
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
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
mpr 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
⊢ 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

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]

Premises used: biSup_mono, Finsupp.sum, SetLike.le_def, Submodule.neg_mem_iff, Submodule.sum_mem_biSup, iSupIndep_def, add_eq_zero_iff_neg_eq, Iff.mp, Submodule.disjoint_def, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
rw :
  (∀ (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) ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i

Tactic:
rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]

Premises used: iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 :
  (∀ (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) →
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
mpr :
  (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i) →
    ∀ (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
⊢ (∀ (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) ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
s : Finset ι
v w : ι → N
hvw : ∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i
⊢ Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i

Tactic:
simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2

Premises used: sub_eq_zero, HSub.hSub, And.right, And.left, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 w : ι → N),
    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0
⊢ (∀ i ∈ s, v i ∈ p i ∧ 0 i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, 0 i) → ∀ i ∈ s, v i = 0 i

Tactic:
specialize h s v 0

Premises used: OfNat.ofNat