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
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_3 : (i : ι) → AddCommMonoid (β₁ i)
inst_4 : (i : ι) → AddCommMonoid (β₂ i)
inst_5 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_6 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
inst_7 : DecidableEq ι
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
h : (i : ι) → LinearMap.{u_3, u_3, u_9, u_6} (RingHom.id R) (β₂ i) N
l : Π₀ (i : ι), β₁ i
⊢ Eq.{u_6 + 1} (α := N)
    ((((lsum ℕ (M := β₂) : (a : (i : ι) → β₂ i →ₗ[R] N) → (Π₀ (i : ι), β₂ i) →ₗ[R] N) h : (Π₀ (i : ι), β₂ i) →ₗ[R] N) :
          (a : Π₀ (i : ι), β₂ i) → N)
        ((mapRange.linearMap (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) l :
          Π₀ (i : ι), β₂ i) :
      N)
    (((lsum ℕ (M := β₁) : (a : (i : ι) → β₁ i →ₗ[R] N) → (Π₀ (i : ι), β₁ i) →ₗ[R] N) fun (i : ι) ↦ h i ∘ₗ f i :
          (a : Π₀ (i : ι), β₁ i) → N)
        l :
      N)

Tactic:
simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp

Premises used: DFinsupp.sumAddHom_apply, DFinsupp.sum_mapRange_index
-- 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
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_3 : (i : ι) → AddCommMonoid (β₁ i)
inst_4 : (i : ι) → AddCommMonoid (β₂ i)
inst_5 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_6 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
inst_7 : DecidableEq ι
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
h : (i : ι) → LinearMap.{u_3, u_3, u_9, u_6} (RingHom.id R) (β₂ i) N
l : Π₀ (i : ι), β₁ i
⊢ Eq.{u_6 + 1} (α := N)
    ((((lsum ℕ (M := β₂) : (a : (i : ι) → β₂ i →ₗ[R] N) → (Π₀ (i : ι), β₂ i) →ₗ[R] N) h : (Π₀ (i : ι), β₂ i) →ₗ[R] N) :
          (a : Π₀ (i : ι), β₂ i) → N)
        ((mapRange.linearMap (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) l :
          Π₀ (i : ι), β₂ i) :
      N)
    (((lsum ℕ (M := β₁) : (a : (i : ι) → β₁ i →ₗ[R] N) → (Π₀ (i : ι), β₁ i) →ₗ[R] N) fun (i : ι) ↦ h i ∘ₗ f i :
          (a : Π₀ (i : ι), β₁ i) → N)
        l :
      N)

Tactic:
classical simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp

Premises used: DFinsupp.sumAddHom_apply, DFinsupp.sum_mapRange_index
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β₁ i)
inst_2 : (i : ι) → AddCommMonoid (β₂ i)
inst_3 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_4 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
⊢ (mapRange.linearMap (β₁ := β₁) (β₂ := β₂) f).ker =
    Submodule.comap (coeFnLinearMap R (β := β₁)) (Submodule.pi (φ := β₁) Set.univ fun (i : ι) ↦ (f i).ker)

Tactic:
Submodule.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)

Premises used: LinearMap.toAddMonoidHom, Submodule.toAddSubmonoid_injective, DFinsupp.mker_mapRangeAddMonoidHom
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β₁ i)
inst_2 : (i : ι) → AddCommMonoid (β₂ i)
inst_3 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_4 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
⊢ (mapRange.linearMap (β₁ := β₁) (β₂ := β₂) f).range =
    Submodule.comap (coeFnLinearMap R (β := β₂)) (Submodule.pi (φ := β₂) Set.univ fun (x : ι) ↦ (f x).range)

Tactic:
Submodule.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)

Premises used: LinearMap.toAddMonoidHom, Submodule.toAddSubmonoid_injective, DFinsupp.mrange_mapRangeAddMonoidHom
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₁ : ι → Type u_8
inst_1 : (i : ι) → AddCommMonoid (β₁ i)
inst_2 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
⊢ Eq (α := (Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₁ i)
    (linearEquiv (β₁ := β₁) (β₂ := β₁) fun (i : ι) ↦ LinearEquiv.refl R (β₁ i)) (LinearEquiv.refl R (Π₀ (i : ι), β₁ i))

Tactic:
LinearEquiv.ext mapRange_id

Premises used: LinearEquiv.ext, DFinsupp.mapRange_id, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β : ι → Type u_7
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → AddCommMonoid (β₁ i)
inst_3 : (i : ι) → AddCommMonoid (β₂ i)
inst_4 : (i : ι) → Module.{u_3, u_7} R (β i)
inst_5 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_6 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
f : (i : ι) → LinearEquiv.{u_3, u_3, u_7, u_8} (RingHom.id R) (β i) (β₁ i)
f₂ : (i : ι) → LinearEquiv.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
⊢ ∀ (i : ι),
    Eq.{u_9 + 1} (α := β₂ i)
      (Function.comp.{u_7 + 1, u_8 + 1, u_9 + 1} (α := β i) (β := β₁ i)
        ((fun (i : ι) (x : β₁ i) ↦ ((f₂ i : (a : β₁ i) → β₂ i) x : β₂ i)) i)
        ((fun (i : ι) (x : β i) ↦ ((f i : (a : β i) → β₁ i) x : β₁ i)) i) 0)
      0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β₁ i)
inst_2 : (i : ι) → AddCommMonoid (β₂ i)
inst_3 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_4 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
e : (i : ι) → LinearEquiv.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
⊢ (linearEquiv (β₁ := β₁) (β₂ := β₂) e).symm = linearEquiv (β₁ := β₂) (β₂ := β₁) fun (i : ι) ↦ (e i).symm

Tactic:
rfl

Premises used: LinearEquiv.symm, DFinsupp.mapRange, DFinsupp.mapRange.linearEquiv, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommGroup (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
⊢ (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f).ker =
    AddSubgroup.comap (N := (i : ι) → β₁ i) (coeFnAddMonoidHom (β := β₁))
      (AddSubgroup.pi (f := β₁) Set.univ fun (x : ι) ↦ (f x).ker)

Tactic:
AddSubgroup.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom f

Premises used: DFinsupp.mker_mapRangeAddMonoidHom, AddSubgroup.toAddSubmonoid_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommGroup (β₁ i)
inst_1 : (i : ι) → AddCommGroup (β₂ i)
f : (i : ι) → AddMonoidHom.{u_9, u_8} (β₂ i) (β₁ i)
⊢ (mapRange.addMonoidHom (β₁ := β₂) (β₂ := β₁) f).range =
    AddSubgroup.comap (N := (i : ι) → β₁ i) (coeFnAddMonoidHom (β := β₁))
      (AddSubgroup.pi (f := β₁) Set.univ fun (x : ι) ↦ (f x).range)

Tactic:
AddSubgroup.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom f

Premises used: DFinsupp.mrange_mapRangeAddMonoidHom, AddSubgroup.toAddSubmonoid_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : (x : N) → Decidable (x ≠ 0)
f : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
x : Π₀ (i : ι), M i
⊢ Eq.{u_6 + 1} (α := N) ((coprodMap (M := M) f : (a : Π₀ (i : ι), M i) → N) x : N)
    (sum (β := fun (i : ι) ↦ N)
        (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ N) (fun (i : ι) ↦ (⇑(f i) : (a : M i) → N)) ⋯ x) fun (x : ι) ↦ id :
      N)

Tactic:
DFinsupp.sumAddHom_apply _ _

Premises used: DFinsupp.mapRange, DFinsupp.sumAddHom_apply, Trunc.lift
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
f : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
i : ι
x : M i
⊢ Eq.{u_6 + 1} (α := N) ((coprodMap (M := M) f : (a : Π₀ (i : ι), M i) → N) (single (β := M) i x) : N)
    ((f i : (a : M i) → N) x : N)

Tactic:
simp [coprodMap]

Premises used: DFinsupp.coprodMap
-- 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 ι
β : ι → Type u_7
inst_4 : (i : ι) → Zero (β i)
inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
S : Submodule R N
f : Π₀ (i : ι), β i
g : (i : ι) → β i → N
h : ∀ (c : ι), (f : (a : ι) → β a) c ≠ 0 → g c ((f : (a : ι) → β a) c) ∈ S
⊢ f.sum (β := β) g ∈ S

Tactic:
_root_.dfinsuppSum_mem S f g h

Premises used: dfinsuppSum_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
inst_3 : DecidableEq ι
β : ι → Type u_7
inst_4 : (i : ι) → AddZeroClass (β i)
S : Submodule R N
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{u_7, u_6} (β i) N
h : ∀ (c : ι), (f : (a : ι) → β a) c ≠ 0 → Membership.mem (α := N) S ((g c : (a : β c) → N) ((f : (a : ι) → β a) c) : N)
⊢ Membership.mem (α := N) S ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → N) f : N)

Tactic:
_root_.dfinsuppSumAddHom_mem S f g h

Premises used: Set.Mem, dfinsuppSumAddHom_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
inst_3 : DecidableEq ι
p : ι → Submodule R N
a :
  iSup p ≤
    LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype)
a₁ :
  LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype) ≤
    iSup p
⊢ iSup p =
    LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
apply :
  ∀ (i : ι),
    p i ≤
      LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
        ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype)
⊢ iSup p ≤
    LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype)

Tactic:
apply iSup_le _

Premises used: iSup_le
-- 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
i : ι
y : N
hy : y ∈ p i
simp :
  ∃ (y_1 : Π₀ (i : ι), ↥(p i)),
    (sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype.toAddMonoidHom : (a : Π₀ (i : ι), ↥(p i)) → N)
        y_1 =
      y
⊢ Membership.mem (γ := Submodule R N)
    (LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype))
    y

Tactic:
simp only [LinearMap.mem_range, lsum_apply_apply]

Premises used: LinearMap.mem_range, 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 : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ (y_1 : Π₀ (i : ι), ↥(p i)),
    (sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype.toAddMonoidHom : (a : Π₀ (i : ι), ↥(p i)) → N)
        y_1 =
      y

Tactic:
⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Premises used: DFinsupp.sumAddHom_single, DFinsupp.single, Subtype.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
inst_3 : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ (y_1 : Π₀ (i : ι), ↥(p i)),
    (sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype.toAddMonoidHom : (a : Π₀ (i : ι), ↥(p i)) → N)
        y_1 =
      y

Tactic:
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
-- 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
v : Π₀ (i : ι), ↥(p i)
⊢ Membership.mem (α := N) (iSup p)
    (((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)
        v :
      N)

Tactic:
dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2

Premises used: Set.Mem, le_iSup, Submodule.dfinsuppSumAddHom_mem, DFunLike.coe, Subtype.property, 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
inst_3 : DecidableEq ι
p : ι → Submodule R N
v : Π₀ (i : ι), ↥(p i)
⊢ Membership.mem (α := N) (iSup p)
    (((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)
        v :
      N)

Tactic:
exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2

Premises used: le_iSup, Submodule.dfinsuppSumAddHom_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
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
a :
  LE.le.{u_6} (α := Submodule R N) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (LinearMap.range (M := Π₀ (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) ∘ₗ
        filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p))
a₁ :
  LE.le.{u_6} (α := Submodule R N)
    (LinearMap.range (M := Π₀ (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) ∘ₗ
        filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p))
    (⨆ (i : ι), ⨆ (_ : p i), S i)
⊢ Eq.{u_6 + 1} (α := Submodule R N) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (LinearMap.range (M := Π₀ (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) ∘ₗ
        filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
⊢ LE.le.{u_6} (α := Submodule R N) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (LinearMap.range (M := Π₀ (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) ∘ₗ
        filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p))

Tactic:
iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Premises used: iSup₂_le, Set.Mem, DFinsupp.single, setOf, Subtype.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
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
a :
  ∀ (i : ι) (hi : p i) (y : N) (hy : y ∈ S i),
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(S i)) : (a : (i : ι) → ↥(S i) →ₗ[R] N) → (Π₀ (i : ι), ↥(S i)) →ₗ[R] N) fun (i : ι) ↦
              (S i).subtype) ∘ₗ
            filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p :
          (a : Π₀ (i : ι), ↥(S i)) → N)
        (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : N) ↦ x ∈ S i) y hy)) =
      y
⊢ LE.le.{u_6} (α := Submodule R N) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (LinearMap.range (M := Π₀ (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) ∘ₗ
        filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p))

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Premises used: iSup₂_le
-- 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
i : ι
hi : p i
y : N
hy : y ∈ S i
a :
  ((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)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : N) ↦ x ∈ S i) y hy)) =
    y
⊢ (((lsum ℕ (M := fun (i : ι) ↦ ↥(S i)) : (a : (i : ι) → ↥(S i) →ₗ[R] N) → (Π₀ (i : ι), ↥(S i)) →ₗ[R] N) fun (i : ι) ↦
            (S i).subtype) ∘ₗ
          filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p :
        (a : Π₀ (i : ι), ↥(S i)) → N)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : N) ↦ x ∈ S i) y hy)) =
    y

Tactic:
rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]

Premises used: LinearMap.comp_apply, DFinsupp.filterLinearMap_apply, DFinsupp.filter_single_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
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ 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)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : N) ↦ x ∈ S i) y hy)) =
    y

Tactic:
simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]

Premises used: LinearMap.toAddMonoidHom_coe, DFinsupp.sumAddHom_single, 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
v : Π₀ (i : ι), ↥(S i)
⊢ Membership.mem.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (i : ι), ⨆ (_ : p 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) ∘ₗ
            filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p :
          (a : Π₀ (i : ι), ↥(S i)) → N)
        v :
      N)

Tactic:
dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Premises used: Set.Mem, Submodule.dfinsuppSumAddHom_mem, 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
inst_3 : DecidableEq ι
p : ι → Prop
inst_4 : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
a :
  ∀ (i : ι),
    (((filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i ≠
        0 →
      Membership.mem (α := N) (γ := Submodule R N) (⨆ (i : ι), ⨆ (_ : 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.{u_6, u_6} (α := N) (γ := Submodule R N) (⨆ (i : ι), ⨆ (_ : p 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) ∘ₗ
            filterLinearMap R (fun (i : ι) ↦ ↥(S i)) p :
          (a : Π₀ (i : ι), ↥(S i)) → N)
        v :
      N)

Tactic:
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Premises used: Submodule.dfinsuppSumAddHom_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
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
⊢ Membership.mem (α := N) (γ := Submodule R N) (⨆ (i : ι), ⨆ (_ : 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:
mem_iSup_of_mem i ?_

Premises used: Submodule.mem_iSup_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
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
a :
  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) (⨆ (i : ι), ⨆ (_ : 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:
refine mem_iSup_of_mem i ?_

Premises used: Submodule.mem_iSup_of_mem