awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
closed_under_smul :
  ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N →
        r • n ∈
          map (M := Finsupp.{u_2, u_3} R ↥N)
            (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
            (Finsupp.supported (↥N) R sR)
le :
  map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR) ≤
    sR • N
⊢ sR • N =
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)

Tactic:
apply set_smul_eq_of_le

Premises used: Submodule.set_smul_eq_of_le
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
        (a : R →₀ ↥N) → M)
      (Finsupp.single r (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn)) =
    r • n

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)

Tactic:
exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
x : M
hx :
  x ∈
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)
le :
  ∀ (c : Finsupp.{u_2, u_3} R ↥N) (hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))),
    Membership.mem (α := M) (sR • N)
      ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
            (a : R →₀ ↥N) → M)
          c :
        M)
⊢ x ∈ sR • N

Tactic:
obtain ⟨c, hc, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
le : (↑(∑ x ∈ c.support, (DistribSMul.toLinearMap R (↥N) x : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) x)) : M) ∈ sR • N
⊢ Membership.mem (α := M) (sR • N)
    ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
          (a : R →₀ ↥N) → M)
        c :
      M)

Tactic:
simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]

Premises used: Finsupp.sum, Finsupp.coe_lsum, LinearMap.coe_comp, Submodule.coe_subtype, Function.comp_apply
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
le : ∑ i ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) i : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) i)) : M) ∈ sR • N
⊢ (↑(∑ x ∈ c.support, (DistribSMul.toLinearMap R (↥N) x : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) x)) : M) ∈ sR • N

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Premises used: AddSubmonoid.coe_finsetSum
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
⊢ ∑ i ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) i : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) i)) : M) ∈ sR • N

Tactic:
Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩

Premises used: Submodule.sum_mem, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
le : ∀ c_1 ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) c_1 : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) c_1)) : M) ∈ sR • N
le₁ :
  (fun (s : Submodule R M) ↦
        (⋂ (_ :
            Membership.mem (γ := Set (Submodule R M))
              {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} s),
            (↑s : Set M) :
          Set M))
      (sR • N) =
    (↑(sR • N) : Set M)
⊢ ∑ i ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) i : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) i)) : M) ∈ sR • N

Tactic:
refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩

Premises used: Submodule.sum_mem, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
r : R
hr : r ∈ c.support
le :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
      (↑((DistribSMul.toLinearMap R (↥N) r : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) r)) : M) ∈ p
⊢ (↑((DistribSMul.toLinearMap R (↥N) r : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) r)) : M) ∈ sR • N

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
r : R
hr : r ∈ c.support
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
⊢ (↑((DistribSMul.toLinearMap R (↥N) r : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) r)) : M) ∈ p

Tactic:
hp (hc hr) (c r).2

Premises used: Set.Mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
r : R
hr : r ∈ c.support
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
⊢ (↑((DistribSMul.toLinearMap R (↥N) r : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) r)) : M) ∈ p

Tactic:
exact hp (hc hr) (c r).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
le :
  ∀ (x : M),
    Membership.mem (γ := Set M)
        ((fun (s : Submodule R M) ↦
            (⋂ (_ :
                Membership.mem (γ := Set (Submodule R M))
                  {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} s),
                (↑s : Set M) :
              Set M))
          (sR • N))
        x ↔
      x ∈ (↑(sR • N) : Set M)
⊢ (fun (s : Submodule R M) ↦
        (⋂ (_ :
            Membership.mem (γ := Set (Submodule R M))
              {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} s),
            (↑s : Set M) :
          Set M))
      (sR • N) =
    (↑(sR • N) : Set M)

Tactic:
ext x : 1
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
le :
  (∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N) ↔
    x ∈ sR • N
⊢ Membership.mem (γ := Set M)
      ((fun (s : Submodule R M) ↦
          (⋂ (_ :
              Membership.mem (γ := Set (Submodule R M))
                {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} s),
              (↑s : Set M) :
            Set M))
        (sR • N))
      x ↔
    x ∈ (↑(sR • N) : Set M)

Tactic:
simp only [Set.mem_iInter, SetLike.mem_coe]

Premises used: Set.mem_iInter, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
le :
  (∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N) →
    x ∈ sR • N
le₁ :
  x ∈ sR • N →
    ∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N
⊢ (∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N) ↔
    x ∈ sR • N

Tactic:
fconstructor
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
⊢ (∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N) →
    x ∈ sR • N

Tactic:
fun h ↦ h fun r n hr hn ↦ ?_
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
le :
  ∀
    (h :
      ∀
        (i :
          Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
            (sR • N)),
        x ∈ sR • N)
    (r : R) (n : M) (hr : r ∈ sR) (hn : n ∈ N), r • n ∈ sR • N
⊢ (∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N) →
    x ∈ sR • N

Tactic:
refine fun h ↦ h fun r n hr hn ↦ ?_
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
h :
  ∀
    (i :
      Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
        (sR • N)),
    x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
le :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
      r • n ∈ p
⊢ r • n ∈ sR • N

Tactic:
rw [mem_set_smul_def, mem_sInf]

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
h :
  ∀
    (i :
      Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
        (sR • N)),
    x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
      r • n ∈ p

Tactic:
fun p hp ↦ hp hr hn
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
h :
  ∀
    (i :
      Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
        (sR • N)),
    x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
      r • n ∈ p

Tactic:
exact fun p hp ↦ hp hr hn
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
x : M
⊢ x ∈ sR • N →
    ∀
      (i :
        Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}
          (sR • N)),
      x ∈ sR • N

Tactic:
simp_all
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
closed_under_smul :
  ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N →
        r • n ∈
          map (M := Finsupp.{u_2, u_3} R ↥N)
            (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
            (Finsupp.supported (↥N) R sR)
le le₁ :
  map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR) ≤
    sR • N
⊢ sR • N =
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)

Tactic:
classical
  apply set_smul_eq_of_le
  · intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
  · intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finsetSum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · simp_all

Premises used: Submodule.set_smul_eq_of_le, Finsupp.sum, Submodule.mem_set_smul_def, Set.mem_iInter, Finsupp.coe_lsum, LinearMap.coe_comp, SetLike.mem_coe, Submodule.coe_subtype, Submodule.mem_sInf, Function.comp_apply, rfl, AddSubmonoid.coe_finsetSum
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
mp :
  x ∈ sR • N →
    ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
mpr :
  (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
    x ∈ sR • N
⊢ x ∈ sR • N ↔
    ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)

Tactic:
fconstructor
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
h : x ∈ sR • N
⊢ x ∈
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)

Tactic:
rw [set_smul_eq_map] at h

Premises used: Submodule.set_smul_eq_map
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
h :
  x ∈
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)
mp :
  ∀ (c : Finsupp.{u_2, u_3} R ↥N) (hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))),
    ∃ (c_1 : Finsupp.{u_2, u_3} R ↥N),
      (↑c_1.support : Set R) ⊆ sR ∧
        Eq (α := M)
          ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
                (a : R →₀ ↥N) → M)
              c :
            M)
          ((↑(c_1.sum fun (r : R) (m : ↥N) ↦ r • m) : M) : M)
⊢ ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)

Tactic:
obtain ⟨c, hc, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
⊢ ∃ (c_1 : Finsupp.{u_2, u_3} R ↥N),
    (↑c_1.support : Set R) ⊆ sR ∧
      Eq (α := M)
        ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
              (a : R →₀ ↥N) → M)
            c :
          M)
        ((↑(c_1.sum fun (r : R) (m : ↥N) ↦ r • m) : M) : M)

Tactic:
⟨c, hc, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))
⊢ ∃ (c_1 : Finsupp.{u_2, u_3} R ↥N),
    (↑c_1.support : Set R) ⊆ sR ∧
      Eq (α := M)
        ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
              (a : R →₀ ↥N) → M)
            c :
          M)
        ((↑(c_1.sum fun (r : R) (m : ↥N) ↦ r • m) : M) : M)

Tactic:
exact ⟨c, hc, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
mpr :
  (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
    ∀ (p : Submodule R M),
      Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
        x ∈ p
⊢ (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
    x ∈ sR • N

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc1 : (↑c.support : Set R) ⊆ sR
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
mpr : ∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥N) i ((c : (a : R) → ↥N) i : ↥N)) : M) ∈ p
⊢ (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M) ∈ p

Tactic:
rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]

Premises used: Finsupp.sum, AddSubmonoid.coe_finsetSum
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc1 : (↑c.support : Set R) ⊆ sR
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
⊢ ∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥N) i ((c : (a : R) → ↥N) i : ↥N)) : M) ∈ p

Tactic:
Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2

Premises used: Submodule.sum_mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc1 : (↑c.support : Set R) ⊆ sR
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
⊢ ∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥N) i ((c : (a : R) → ↥N) i : ↥N)) : M) ∈ p

Tactic:
exact Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2

Premises used: Submodule.sum_mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
n : M
w : R
left : w ∈ s
w_1 : R
left_1 : w_1 ∈ t
h : n ∈ x
rw : w • w_1 • n ∈ s • t • x
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((fun (x1 x2 : R) ↦ x1 * x2) w w_1) n ∈ s • t • x

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
n : M
w : R
left : w ∈ s
w_1 : R
left_1 : w_1 ∈ t
h : n ∈ x
⊢ w • w_1 • n ∈ s • t • x

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
⊢ SMulCommClass.{u_2, u_2, u_3} R R ↥x

Tactic:
have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩