awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : DecidableEq ι
p : ι → Submodule R N
⊢ 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)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
⊢ 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)
have 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
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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)
have 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)
Tactic: apply iSup_le _
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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
have 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
Tactic: simp only [LinearMap.mem_range, lsum_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ 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))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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))
⊢ 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))
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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))
have 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
Tactic: refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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) ∘ₗ
          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
have 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
Tactic: rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
have 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)
Tactic: refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
have 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)
Tactic: refine mem_iSup_of_mem i ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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) (⨆ (_ : 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)
have 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)
Tactic: by_cases hp : p i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hp : p i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ x ∈ iSup p ↔ ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
have 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
Tactic: rw [mem_iSup_iff_exists_dfinsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ (∃ (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
have 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
Tactic: simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ (∃ (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
have 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
Tactic: simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ (∃ (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
have 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
Tactic: simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have 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
Tactic: rw [mem_iSup_iff_exists_dfinsupp']
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ (∃ (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
have 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
Tactic: refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
have 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 : ι)) sorry) =
  f.support
Tactic: refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ ∃ (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)
have 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 : ι)) sorry :
          (a : ι) → ↥(p a))
        i))
    ((fun (_i : ι) (xi : N) ↦ xi) i ((f : (a : ι) → N) i))
Tactic: refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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)
⊢ 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
have 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 : ι)) sorry) ↔
    a ∈ f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
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
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have 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
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]