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
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 : Eq.{u_6 + 1} (α := Submodule R N) ⊥ (⨆ (_ : x ∈ s), p x)
⊢ Membership.mem (γ := Submodule R N) ⊥ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N)

Tactic:
suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
-- 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
⊢ Eq.{u_6 + 1} (α := Submodule R N) ⊥ (⨆ (_ : x ∈ s), p x)

Tactic:
(iSup_neg hx).symm

Premises used: iSup_neg, Eq.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
x : ι
hx : x ∉ s
⊢ Eq.{u_6 + 1} (α := Submodule R N) ⊥ (⨆ (_ : x ∈ s), p x)

Tactic:
exact (iSup_neg hx).symm

Premises used: iSup_neg, Eq.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
x : ι
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
⊢ 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

Tactic:
_
-- 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
hx : x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
⊢ (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0

Tactic:
rw [mem_support_iff, not_ne_iff] at hx

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 : ι
h_1 : x ∈ s
hx : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
h : Eq.{u_6 + 1} (α := N) ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x 0) 0
⊢ Eq.{u_6 + 1} (α := N)
    ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x ((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x)) 0

Tactic:
rw [hx]
-- 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
hx : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
⊢ Eq.{u_6 + 1} (α := N) ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x 0) 0

Tactic:
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
μ : (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:
⟨DFinsupp.mk s ?_, ?_⟩

Premises used: DFinsupp.mk, Exists.intro
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
mpr : (i : (↑(↑s : Set ι) : Type u_1)) → ↥(⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι))
mpr₁ :
  (sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
        Subtype.casesOn (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (motive := fun (x : (↑(↑s : Set ι) : Type u_1)) ↦
          ↥(⨆ (_ : (↑x : ι) ∈ s), p (↑x : ι))) i fun (i : ι) (hi : i ∈ (↑s : Set ι)) ↦
          Subtype.mk (p := fun (x : N) ↦
            Membership.mem (γ := Submodule R N)
              (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
                p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
              x)
            (↑(μ i) : N) ⋯)
      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

Tactic:
refine ⟨DFinsupp.mk s ?_, ?_⟩
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
mpr :
  Membership.mem (γ := Submodule R N)
    (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
    (↑(μ i) : N)
⊢ ↥(⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))

Tactic:
refine ⟨μ 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
mpr : (↑(μ i) : N) ∈ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)
mpr₁ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s
⊢ Membership.mem (γ := Submodule R N)
    (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
    (↑(μ i) : N)

Tactic:
rw [iSup_pos]

Premises used: iSup_pos
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ (↑(μ i) : N) ∈ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)

Tactic:
coe_mem _

Premises used: Set.Mem, Submodule.coe_mem
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ (↑(μ i) : N) ∈ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)

Tactic:
exact coe_mem _

Premises used: Submodule.coe_mem
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s

Tactic:
hi

Premises used: Set.Mem, setOf
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s

Tactic:
exact 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
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
mpr :
  ∑
      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
⊢ (sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
        Subtype.casesOn (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (motive := fun (x : (↑(↑s : Set ι) : Type u_1)) ↦
          ↥(⨆ (_ : (↑x : ι) ∈ s), p (↑x : ι))) i fun (i : ι) (hi : i ∈ (↑s : Set ι)) ↦
          Subtype.mk (p := fun (x : N) ↦
            Membership.mem (γ := Submodule R N)
              (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
                p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
              x)
            (↑(μ i) : N) ⋯)
      fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) =
    a

Tactic:
simp only [DFinsupp.sum]

Premises used: DFinsupp.sum
-- 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 : ι) → ↥(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))
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) ⋯) →
      (↑((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
⊢ ∑
      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

Tactic:
rw [Finset.sum_subset support_mk_subset, ← hμ]

Premises used: DFinsupp.support_mk_subset, 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
x : ι
hx : x ∈ s
rw 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) ⋯) :
      N) =
    (↑(μ x) : 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) =
    (↑(μ x) : N)

Tactic:
rw [mk_of_mem hx]

Premises used: DFinsupp.mk_of_mem
-- 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 : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
⊢ 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))

Tactic:
exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]

Premises used: Finset.sum_congr, 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
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
x : ι
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) ⋯) →
      (↑((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
⊢ 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) ⋯) →
      (↑((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

Tactic:
_
-- 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 : ι) → ↥(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 =
    0

Tactic:
rw [mem_support_iff, not_ne_iff] at hx

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 : ι) → ↥(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
mpr : Eq.{u_6 + 1} (α := N) (↑0 : N) 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

Tactic:
rw [hx]
-- 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 : ι) → ↥(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
⊢ Eq.{u_6 + 1} (α := N) (↑0 : N) 0

Tactic:
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 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
mpr 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
⊢ Membership.mem (γ := Submodule R N) (⨆ i ∈ s, p i) 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

Premises used: Submodule.mem_bot, DFinsupp.support_mk_subset, iSup_pos, not_ne_iff, Submodule.coe_mem, DFinsupp.sum, Submodule.coe_zero, DFinsupp.mem_support_iff, Finset.sum_subset, Submodule.mem_iSup_iff_exists_dfinsupp', Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
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
⊢ iSupIndep p ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
          (↑x : N) →
        x = 0

Tactic:
simp_rw [iSupIndep_def, Submodule.disjoint_def,
    Submodule.mem_biSup_iff_exists_dfinsupp, exists_imp, filter_ne_eq_erase]

Premises used: iSupIndep_def, DFinsupp.filter_ne_eq_erase, Submodule.disjoint_def, exists_imp, Submodule.mem_biSup_iff_exists_dfinsupp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : ι → Submodule R N
⊢ (∀ (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:
forall_congr' fun i => Subtype.forall'.trans ?_

Premises used: forall_congr', Iff.trans, Subtype.forall'