awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g_1 : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h_1 : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g (⇑f : (a : M) → M₂)
x : ↥f.range
x' : M
hx' : (f : (a : M) → M₂) x' = (↑x : M₂)
rw : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) (g ((f : (a : M) → M₂) x')) : M₂) ((f : (a : M) → M₂) x' : M₂)
⊢ (f : (a : M) → M₂) (g (↑x : M₂)) = (↑x : M₂)
have rw₁ : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x' : M₂) ((f : (a : M) → M₂) x' : M₂)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : ↥f.range
⊢ (f : (a : M) → M₂) ((symm (ofInjective f h) : (a : ↥f.range) → M) x : M) = (↑x : M₂)
have obtain : ∀ (y : M),
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((symm (ofInjective f h) : (a : ↥f.range) → M)
            (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) sorry : ↥f.range) :
          M) :
      M₂)
    ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) sorry) : M₂) : M₂)
Tactic: obtain ⟨-, ⟨y, rfl⟩⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : M
⊢ Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((symm (ofInjective f h) : (a : ↥f.range) → M)
            (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯ : ↥f.range) :
          M) :
      M₂)
    ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯) : M₂) : M₂)
have this : Eq.{u_7 + 1} (α := ↥f.range) (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) sorry : ↥f.range)
  (((ofInjective f h : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ M ↥f.range) : (a : M) → ↥f.range) y : ↥f.range)
Tactic: have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Bijective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M₂
⊢ (f : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x
have rw : (ofBijective f h : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x
Tactic: rw [← ofBijective_apply f (hf := h) ((ofBijective f h).symm x), apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Bijective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M₂
rw : (ofBijective f h : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x
⊢ (f : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x
have rw₁ : x = x
Tactic: rw [← ofBijective_apply f (hf := h) ((ofBijective f h).symm x), apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ↥q
have refine_1 : x ∈ p
Tactic: refine ⟨⟨x, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
refine_1 : x ∈ p
⊢ ↥q
have refine_2 : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x sorry ∈ q
Tactic: refine ⟨⟨x, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ x ∈ p
have refine_1 : ∀ (val : M) (h : val ∈ p),
  Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p) →
    Membership.mem (α := M) p ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h) : M)
Tactic: rcases hx with ⟨⟨_, h⟩, _, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x ⋯ ∈ q
have refine_2 : ∀ (val : M) (h : val ∈ p) (left : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p)),
  Membership.mem (α := ↥p) q
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h))
        sorry :
      ↥p)
Tactic: rcases hx with ⟨⟨_, h⟩, _, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective.{u_5 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : p ≤ f.range
x_1 : ↥p
x : N
hx : x ∈ p
⊢ ∃ (a : ↥(comap f p)),
    (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) a =
      Subtype.mk (p := fun (x : N) ↦ x ∈ p) x hx
have obtain : ∀ (y : M) (hx : Membership.mem (α := N) p ((f : (a : M) → N) y : N)),
  ∃ (a : ↥(comap f p)),
    Eq.{u_9 + 1} (α := ↥p) ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) sorry : (a : ↥(comap f p)) → ↥p) a : ↥p)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f : (a : M) → N) y) hx : ↥p)
Tactic: obtain ⟨y, rfl⟩ := h hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective.{u_8 + 1, u_7 + 1} (α := M₃) (β := M₂) (⇑i : (a : M₃) → M₂)
hf : ∀ (x : M₁), Membership.mem (α := M₂) i.range ((f : (a : M₁) → M₂) x : M₂)
⊢ i ∘ₗ f.codRestrictOfInjective i hi hf = f
have h : ∀ (x : M₁),
  Eq.{u_7 + 1} (α := M₂) ((i ∘ₗ f.codRestrictOfInjective i hi hf : (a : M₁) → M₂) x : M₂) ((f : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
e : LinearEquiv.{u_1, u_1, u_5, u_8} (RingHom.id R) (↥i.range) M₃ := LinearEquiv.symm (LinearEquiv.ofInjective i hi)
x₁ x₂ : M₁
⊢ (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (x₁ + x₂)) ⋯ =
    (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₁) ⋯ +
      (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₂) ⋯
have h : ∀ (y : M₂),
  Eq.{u_8 + 1} (α := M₃)
    (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (x₁ + x₂)) sorry : (a : M₂) → M₃) y : M₃)
    (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₁) sorry +
            (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₂) sorry :
          (a : M₂) → M₃)
        y :
      M₃)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
e : LinearEquiv.{u_1, u_1, u_5, u_8} (RingHom.id R) (↥i.range) M₃ := LinearEquiv.symm (LinearEquiv.ofInjective i hi)
t : R
x : M₁
⊢ (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (t • x)) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
      ((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x) ⋯)
have h : ∀ (y : M₂),
  Eq.{u_8 + 1} (α := M₃)
    (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (t • x)) sorry : (a : M₂) → M₃) y : M₃)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
            ((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x) sorry) :
          (a : M₂) → M₃)
        y :
      M₃)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ 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)
have 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)
Tactic: apply set_smul_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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)
⊢ 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)
have 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
Tactic: apply set_smul_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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)
⊢ x ∈ sR • N
have 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)
Tactic: obtain ⟨c, hc, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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))
⊢ 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)
have le : (↑(∑ x ∈ c.support, (DistribSMul.toLinearMap R (↥N) x : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) x)) : M) ∈ sR • N
Tactic: simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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 ∈ c.support, (DistribSMul.toLinearMap R (↥N) x : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) x)) : M) ∈ sR • N
have le : ∑ i ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) i : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) i)) : M) ∈ sR • N
Tactic: rw [AddSubmonoid.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
have le : ∀ c_1 ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) c_1 : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) c_1)) : M) ∈ sR • N
Tactic: refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ ∑ i ∈ c.support, (↑((DistribSMul.toLinearMap R (↥N) i : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) i)) : M) ∈ sR • N
have 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)
Tactic: refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ (↑((DistribSMul.toLinearMap R (↥N) r : (a : ↥N) → ↥N) ((c : (a : R) → ↥N) r)) : M) ∈ sR • N
have 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
Tactic: rw [mem_set_smul_def, Submodule.mem_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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))
⊢ (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)
have 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)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ 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)
have 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
Tactic: simp only [Set.mem_iInter, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
have 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
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ (∀
      (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
have 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
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
have 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
Tactic: refine fun h ↦ h fun r n hr hn ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ r • n ∈ sR • N
have 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
Tactic: rw [mem_set_smul_def, mem_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ 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)
have 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)
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