awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
x : M
hx : x ∈ p
hy : Membership.mem (α := M₂) (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
                (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x) hy) :
            M₂) :
          M₂) :
      M)

Tactic:
simp only [symm_apply_apply, coe_coe, hx]

Premises used: LinearEquiv.symm_apply_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ (fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
        (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) ⋯ : ↥p))
      ((LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) ⋯).toFun x) =
    x

Tactic:
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
        LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta]

Premises used: LinearMap.toFun_eq_coe, LinearEquiv.symm_apply_apply, SetLike.eta, LinearMap.codRestrict_apply, LinearMap.domRestrict_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
a :
  (↑((LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) ⋯).toFun
          ((fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
              (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) ⋯ : ↥p))
            y)) :
      M₂) =
    (↑y : M₂)
⊢ (LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) ⋯).toFun
      ((fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
          (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) ⋯ : ↥p))
        y) =
    y

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
⊢ (↑((LinearMap.codRestrict (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) ((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p) ⋯).toFun
          ((fun (y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) ↦
              (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂)) ⋯ : ↥p))
            y)) :
      M₂) =
    (↑y : M₂)

Tactic:
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
        LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply]

Premises used: LinearMap.toFun_eq_coe, LinearEquiv.apply_symm_apply, LinearMap.codRestrict_apply, LinearMap.domRestrict_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂) ((↑((e.submoduleMap p : (a : ↥p) → ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) x) : M₂) : M₂)
    ((e : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
⊢ Eq.{u_5 + 1} (α := M) ((↑(((e.submoduleMap p).symm : (a : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)) → ↥p) x) : M) : M)
    ((e.symm : (a : M₂) → M) (↑x : M₂) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Order
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : Module R M
S : Submodule R M
⊢ IsOrderedAddMonoid.{u_2} ↥S

Tactic:
Function.Injective.isOrderedAddMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Subtype.val, rfl, Function.Injective.isOrderedAddMonoid
-- Module: Mathlib.Algebra.Module.Submodule.Order
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : Module R M
S : Submodule R M
⊢ IsOrderedCancelAddMonoid.{u_2} ↥S

Tactic:
Function.Injective.isOrderedCancelAddMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedCancelAddMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ (↑(-S) : Set M) = -(↑S : Set M)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ (-S).toAddSubmonoid = -S.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : M
S : Submodule R M
⊢ g ∈ -S ↔ -g ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
⊢ -S ≤ -T ↔ S ≤ T

Tactic:
SetLike.coe_subset_coe.symm.trans Set.neg_subset_neg

Premises used: SetLike.coe_subset_coe, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
⊢ -S ≤ T ↔ S ≤ -T

Tactic:
SetLike.coe_subset_coe.symm.trans Set.neg_subset

Premises used: SetLike.coe_subset_coe, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ -S = S ↔ -S ≤ S

Tactic:
⟨le_of_eq, fun h => antisymm h <| neg_le.mp h⟩

Premises used: Iff.intro, antisymm, Iff.mp, le_of_eq, Submodule.neg_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
⊢ -(S ⊓ T) = -S ⊓ -T

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
⊢ -(S ⊔ T) = -S ⊔ -T

Tactic:
(negOrderIso : Submodule R M ≃o Submodule R M).map_sup S T

Premises used: Set.Mem, setOf, Submodule.negOrderIso, OrderIso.map_sup
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (-⊥) ⊥

Tactic:
SetLike.coe_injective <| (Set.neg_singleton 0).trans <| congr_arg _ neg_zero

Premises used: SetLike.coe_injective, congr_arg, Set.neg_singleton, OfNat.ofNat, neg_zero, Eq.trans
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (-⊤) ⊤

Tactic:
SetLike.coe_injective <| Set.neg_univ

Premises used: SetLike.coe_injective, Set.neg_univ
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Sort u_4
S : ι → Submodule R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (-⨅ (i : ι), S i) (⨅ (i : ι), -S i)

Tactic:
(negOrderIso : Submodule R M ≃o Submodule R M).map_iInf _

Premises used: OrderIso.map_iInf, Submodule.negOrderIso
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Sort u_4
S : ι → Submodule R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (-⨆ (i : ι), S i) (⨆ (i : ι), -S i)

Tactic:
(negOrderIso : Submodule R M ≃o Submodule R M).map_iSup _

Premises used: OrderIso.map_iSup, Submodule.negOrderIso
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
p : Submodule R M
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule S M) (-restrictScalars S p) x ↔
      Membership.mem (γ := Submodule S M) (restrictScalars S (-p)) x
⊢ Eq (α := Submodule S M) (-restrictScalars S p) (restrictScalars S (-p))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
p : Submodule R M
x : M
⊢ Membership.mem (γ := Submodule S M) (-restrictScalars S p) x ↔
    Membership.mem (γ := Submodule S M) (restrictScalars S (-p)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ -p = p

Tactic:
ext fun _ => p.neg_mem_iff

Premises used: Submodule.neg_mem_iff, Submodule.ext
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
⊢ p + q = p ⊔ q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) 0 ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
S : Submodule R M
⊢ a • S = map (DistribSMul.toLinearMap R M a) S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
S : Submodule R M
⊢ (↑(a • S) : Set M) = a • (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
S : Submodule R M
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, AddSubmonoid.map, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
inst : Monoid α
R : Type u_4
M : Type u_5
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : DistribMulAction α M
inst_4 : Module R M
inst_5 : SMulCommClass α R M
a : α
S : Submodule R M
⊢ (a • S).toAddSubgroup = a • S.toAddSubgroup

Tactic:
rfl

Premises used: rfl, AddSubgroup.map
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
m : M
a : α
S : Submodule R M
⊢ m ∈ a • S ↔ ∃ b ∈ S, a • b = m

Tactic:
Set.mem_smul_set

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
m : M
a : α
S : Submodule R M
⊢ m ∈ S → a • m ∈ a • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
⊢ CovariantClass α (Submodule R M) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => map_mono⟩

Premises used: CovariantClass.mk, Submodule.map_mono
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
⊢ HSMul.hSMul (β := Submodule R M) a ⊥ = ⊥

Tactic:
map_bot _

Premises used: Submodule.map_bot
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
S T : Submodule R M
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Set.Mem, setOf, Submodule.map_sup
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
a : α
ι : Sort u_4
f : ι → Submodule R M
⊢ HSMul.hSMul (β := Submodule R M) a (⨆ (i : ι), f i) = ⨆ (i : ι), a • f i

Tactic:
map_iSup _ _

Premises used: Submodule.map_iSup
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
inst_6 : DistribMulAction.{u_1, u_3} αᵐᵒᵖ M
inst_7 : SMulCommClass.{u_1, u_2, u_3} αᵐᵒᵖ R M
inst_8 : IsCentralScalar α M
⊢ IsCentralScalar.{u_1, u_3} α (Submodule R M)

Tactic:
⟨fun _a S => (congr_arg fun f : Module.End R M => S.map f) <| LinearMap.ext <| op_smul_eq_smul _⟩

Premises used: LinearMap.ext, congr_arg, IsCentralScalar.mk, Submodule.map, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
inst_3 : Monoid α
inst_4 : SMul α R
inst_5 : DistribMulAction α M
inst_6 : SMulCommClass α R M
inst_7 : IsScalarTower α R M
a : α
S : Submodule R M
x : M
hx : x ∈ (↑S : Set M)
⊢ Membership.mem (α := M) S ((DistribSMul.toLinearMap R M a : (a : M) → M) x : M)

Tactic:
smul_of_tower_mem _ a hx

Premises used: Set.Mem, Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
inst_3 : Monoid α
inst_4 : SMul α R
inst_5 : DistribMulAction α M
inst_6 : SMulCommClass α R M
inst_7 : IsScalarTower α R M
a : α
S : Submodule R M
x : M
hx : x ∈ (↑S : Set M)
⊢ Membership.mem (α := M) S ((DistribSMul.toLinearMap R M a : (a : M) → M) x : M)

Tactic:
exact smul_of_tower_mem _ a hx

Premises used: Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N : Submodule R M
x : M
⊢ x ∈ s • N ↔
    Membership.mem (γ := Submodule R M) (sInf {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}) x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
rw :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p} p →
      r • m ∈ p
⊢ r • m ∈ s • N

Tactic:
rw [mem_set_smul_def, mem_sInf]

Premises used: Submodule.mem_set_smul_def, Submodule.mem_sInf
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p} p →
      r • m ∈ p

Tactic:
fun _ h => h mem1 mem2
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p} p →
      r • m ∈ p

Tactic:
exact fun _ h => h mem1 mem2
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
⊢ s • N ≤ p

Tactic:
sInf_le closed_under_smul

Premises used: Set.Mem, sInf_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
mp : s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
mpr : (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
fconstructor
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ p

Tactic:
h <| mem_set_smul_of_mem_mem hr hn

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ p

Tactic:
exact h <| mem_set_smul_of_mem_mem hr hn

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
⊢ (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p

Tactic:
apply set_smul_le

Premises used: Submodule.set_smul_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s : Set S
N p : Submodule R M
closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
le : p ≤ s • N
⊢ s • N = p

Tactic:
le_antisymm (set_smul_le s N p closed_under_smul) le

Premises used: le_antisymm, Submodule.set_smul_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
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 : Set S
N : Submodule R M
⊢ CovariantClass.{u_4, u_3} (Set S) (Submodule R M) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ _ le => set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr)
    (mem2 := le hm)⟩

Premises used: CovariantClass.mk, Submodule.mem_set_smul_of_mem_mem, HSMul.hSMul, Submodule.set_smul_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
N : Submodule R M
s t : Set S
le : s ≤ t
⊢ s • N ≤ t • N

Tactic:
set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := le hr)
    (mem2 := hm)

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.set_smul_le
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
s t : Set S
p q : Submodule R M
le_set : s ≤ t
le_submodule : p ≤ q
⊢ s • p ≤ t • q

Tactic:
le_trans (set_smul_mono_left _ le_set) <| smul_mono_right _ le_submodule

Premises used: Submodule.set_smul_mono_left, smul_mono_right, le_trans
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ s • N = ⨆ a ∈ s, a • N

Tactic:
Eq.trans (congrArg sInf ?_) csInf_Ici

Premises used: congrArg, csInf_Ici, InfSet.sInf, Eq.trans
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
refine :
  Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p}
    (Set.Ici (⨆ a ∈ s, a • N))
⊢ s • N = ⨆ a ∈ s, a • N

Tactic:
refine Eq.trans (congrArg sInf ?_) csInf_Ici

Premises used: congrArg, csInf_Ici, InfSet.sInf, Eq.trans
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
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
inst_5 : SMulCommClass S R M
s : Set S
N : Submodule R M
simp_rw :
  Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ (b : r ∈ s), ∀ a ∈ N, r • a ∈ p}
    {x : Submodule R M | ∀ (i : S) (i_1 : i ∈ s), i • N ≤ x}
⊢ Eq.{u_3 + 1} (α := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p}
    (Set.Ici (⨆ a ∈ s, a • N))

Tactic:
simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]

Premises used: forall_comm, Set.Ici_def, iSup_le_iff