awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
pos :
  ∀ (hp : p i),
    Membership.mem (α := N) (γ := Submodule R N) (⨆ (_ : p i), S i)
      ((LinearMap.toAddMonoidHom.{u_3, u_3, u_6, u_6} (R := R) (S := R) (modM₁ := (fun (i : ι) ↦ (S i).module) i)
              (modM₂ := inst_2) (σ := RingHom.id R) ((fun (i : ι) ↦ (S i).subtype) i) :
            (a : ↥(S i)) → N)
          ((((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        N)
neg :
  ∀ (hp : ¬p i),
    Membership.mem (α := N) (γ := Submodule R N) (⨆ (_ : p i), S i)
      ((LinearMap.toAddMonoidHom.{u_3, u_3, u_6, u_6} (R := R) (S := R) (modM₁ := (fun (i : ι) ↦ (S i).module) i)
              (modM₂ := inst_2) (σ := RingHom.id R) ((fun (i : ι) ↦ (S i).subtype) i) :
            (a : ↥(S i)) → N)
          ((((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        N)
⊢ Membership.mem (α := N) (γ := Submodule R N) (⨆ (_ : p i), S i)
    ((LinearMap.toAddMonoidHom.{u_3, u_3, u_6, u_6} (R := R) (S := R) (modM₁ := (fun (i : ι) ↦ (S i).module) i)
            (modM₂ := inst_2) (σ := RingHom.id R) ((fun (i : ι) ↦ (S i).subtype) i) :
          (a : ↥(S i)) → N)
        ((((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      N)

Tactic:
by_cases hp : p i
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
hp : p i
⊢ Membership.mem (α := N) (γ := Submodule R N) (⨆ (_ : p i), S i)
    ((LinearMap.toAddMonoidHom.{u_3, u_3, u_6, u_6} (R := R) (S := R) (modM₁ := (fun (i : ι) ↦ (S i).module) i)
            (modM₂ := inst_2) (σ := RingHom.id R) ((fun (i : ι) ↦ (S i).subtype) i) :
          (a : ↥(S i)) → N)
        ((((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      N)

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
hp : ¬p i
⊢ Membership.mem (α := N) (γ := Submodule R N) (⨆ (_ : p i), S i)
    ((LinearMap.toAddMonoidHom.{u_3, u_3, u_6, u_6} (R := R) (S := R) (modM₁ := (fun (i : ι) ↦ (S i).module) i)
            (modM₂ := inst_2) (σ := RingHom.id R) ((fun (i : ι) ↦ (S i).subtype) i) :
          (a : ↥(S i)) → N)
        ((((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      N)

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Submodule R N
x : N
⊢ x ∈ iSup p ↔
    ∃ (f : Π₀ (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)
          f =
        x

Tactic:
SetLike.ext_iff.mp (iSup_eq_range_dfinsupp_lsum p) x

Premises used: Set.Mem, setOf, Submodule.iSup_eq_range_dfinsupp_lsum, SetLike.ext_iff, Iff.mp, Set.range
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Submodule R N
inst_4 : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
rw :
  (∃ (f : Π₀ (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)
          f =
        x) ↔
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ x ∈ iSup p ↔ ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp]

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Submodule R N
inst_4 : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
simp_rw :
  (∃ (f : Π₀ (i : ι), ↥(p i)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype.toAddMonoidHom : (a : Π₀ (i : ι), ↥(p i)) → N)
          f =
        x) ↔
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
simp_rw₁ :
  (∃ (f : Π₀ (i : ι), ↥(p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) ↦ (⇑(p x).subtype.toAddMonoidHom : (a : ↥(p x)) → N)) = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
simp_rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) ↦ (⇑(p x).subtype : (a : ↥(p x)) → N)) = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ (∃ (f : Π₀ (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)
          f =
        x) ↔
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x

Tactic:
simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]

Premises used: LinearMap.toAddMonoidHom_coe, DFinsupp.sumAddHom_apply, Submodule.coe_subtype, DFinsupp.lsum_apply_apply
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
x : N
⊢ Membership.mem (γ := Submodule R N) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)),
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(S i)) : (a : (i : ι) → ↥(S i) →ₗ[R] N) → (Π₀ (i : ι), ↥(S i)) →ₗ[R] N)
              fun (i : ι) ↦ (S i).subtype :
            (a : Π₀ (i : ι), ↥(S i)) → N)
          (filter (β := fun (i : ι) ↦ ↥(S i)) p f) =
        x

Tactic:
SetLike.ext_iff.mp (biSup_eq_range_dfinsupp_lsum p S) x

Premises used: Submodule.biSup_eq_range_dfinsupp_lsum, Set.Mem, setOf, SetLike.ext_iff, Iff.mp, Set.range, Trunc.lift
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp']

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp'
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
h : ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ ∀ (a : ι),
    a ∈ f.support (β := fun (i : ι) ↦ ↥(p i)) ↔
      Ne.{u_6 + 1} (α := N) ((fun (i : ι) ↦ (↑((f : (a : ι) → ↥(p a)) i) : N)) a) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
h : ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ ∀ (i : ι),
    Membership.mem (α := N) (p i)
      (({ support := f.support (β := fun (i : ι) ↦ ↥(p i)), toFun := fun (i : ι) ↦ (↑((f : (a : ι) → ↥(p a)) i) : N),
              mem_support_toFun := ⋯ } :
            (a : ι) → N)
          i :
        N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
refine :
  (∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x

Tactic:
refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)
⊢ ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
    Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
      (f.sum fun (_i : ι) (xi : N) ↦ xi)

Tactic:
⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩

Premises used: DFinsupp.mk, Finsupp.support, Subtype.mk, Exists.intro, Subtype.val, DFunLike.coe, Finset.sum_congr
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)
refine_1 :
  support (β := fun (i : ι) ↦ ↥(p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
        Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) =
    f.support
refine_2 :
  ∀ (i : ι) (hi : i ∈ f.support),
    Eq.{u_6 + 1} (α := N)
      ((fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) i
        ((DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯ :
            (a : ι) → ↥(p a))
          i))
      ((fun (_i : ι) (xi : N) ↦ xi) i ((f : (a : ι) → N) i))
⊢ ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
    Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
      (f.sum fun (_i : ι) (xi : N) ↦ xi)

Tactic:
refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)
refine_1 :
  ∀ (a : ι),
    a ∈
        support (β := fun (i : ι) ↦ ↥(p i))
          (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
            Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) ↔
      a ∈ f.support
⊢ support (β := fun (i : ι) ↦ ↥(p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
        Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) =
    f.support

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)
a : ι
⊢ a ∈
      support (β := fun (i : ι) ↦ ↥(p i))
        (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) ↔
    a ∈ f.support

Tactic:
simp [mk_eq_zero]

Premises used: Submodule.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)
i : ι
hi : i ∈ f.support
⊢ Eq.{u_6 + 1} (α := N)
    ((fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) i
      ((DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
            Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯ :
          (a : ι) → ↥(p a))
        i))
    ((fun (_i : ι) (xi : N) ↦ xi) i ((f : (a : ι) → N) i))

Tactic:
simp [Finsupp.mem_support_iff.mp hi]

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
rw₃ :
  (∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
rw₄ :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
    ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
      Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
        (f.sum fun (_i : ι) (xi : N) ↦ xi)
refine_1 :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
    support (β := fun (i : ι) ↦ ↥(p i))
        (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) =
      f.support
refine_2 refine_2₁ :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) (i : ι) (hi : i ∈ f.support),
    Eq.{u_6 + 1} (α := N)
      ((fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) i
        ((DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯ :
            (a : ι) → ↥(p a))
          i))
      ((fun (_i : ι) (xi : N) ↦ xi) i ((f : (a : ι) → N) i))
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x

Tactic:
classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp', Submodule.mk_eq_zero, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 :
  (∃ (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

Tactic:
rw [Submodule.mem_iSup_iff_exists_dfinsupp']

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp'
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
mp :
  (∃ (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
mpr :
  (∃ (μ : (i : ι) → ↥(p i)), ∑ 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
⊢ (∃ (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:
constructor
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
h :
  ∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N) =
    a
⊢ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a

Tactic:
use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
h :
  Eq (α := N)
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
    (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
⊢ ∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N) =
    a

Tactic:
rw [← hμ]
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
h :
  Eq (α := N) (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
⊢ Eq (α := N)
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
    (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))

Tactic:
symm
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
h : μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) ⊆ s
h₁ :
  ∀ x ∈ s,
    x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) →
      Eq.{u_6 + 1} (α := N)
        ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x ((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x)) 0
⊢ Eq (α := N) (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))

Tactic:
apply Finset.sum_subset

Premises used: Finset.sum_subset
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
h : x ∉ s → x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
⊢ x ∈ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) → x ∈ s

Tactic:
contrapose
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
h : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
⊢ x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))

Tactic:
rw [mem_support_iff, not_ne_iff]

Premises used: not_ne_iff, DFinsupp.mem_support_iff
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
h : (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N) = (↑0 : N)
⊢ (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
h : Membership.mem (γ := Submodule R N) ⊥ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N)
⊢ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N) = (↑0 : N)

Tactic:
rw [coe_zero, ← mem_bot R]

Premises used: Submodule.mem_bot, Submodule.coe_zero