awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
⊢ (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
r : A
n : M
hr : r ∈ I
hn : n ∈ N
⊢ r • n ∈ I • N

Tactic:
AddSubmonoid.smul_mem_smul hr hn

Premises used: AddSubmonoid.smul_mem_smul, Set.Mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N P : Submodule R M
⊢ I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P

Tactic:
AddSubmonoid.smul_le

Premises used: Set.Mem, AddSubmonoid.smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
⊢ (↑I : Set A) • N = I • N

Tactic:
set_smul_eq_of_le _ _ _
    (fun _ _ hr hx ↦ smul_mem_smul hr hx)
    (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx)

Premises used: Iff.mpr, Submodule.set_smul_eq_of_le, Submodule.mem_set_smul_of_mem_mem, Submodule.smul_le, Submodule.smul_mem_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)
add : ∀ (x y : M), p x → p y → p (x + y)
⊢ p x

Tactic:
AddSubmonoid.smul_induction_on H smul add

Premises used: AddSubmonoid.smul_induction_on
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx

Tactic:
Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
refine : ∃ (x_1 : x ∈ I • N), p x x_1
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ ∃ (x_1 : x ∈ I • N), p x x_1

Tactic:
smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ ∃ (x_1 : x ∈ I • N), p x x_1

Tactic:
exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N P : Submodule R M
hij : I ≤ J
hnp : N ≤ P
⊢ I • N ≤ J • P

Tactic:
AddSubmonoid.smul_le_smul hij hnp

Premises used: Set.Mem, AddSubmonoid.smul_le_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
h : I ≤ J
⊢ I • N ≤ J • N

Tactic:
smul_mono h le_rfl

Premises used: le_rfl, Submodule.smul_mono
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N P : Submodule R M
⊢ CovariantClass.{v, u_1} (Submodule R A) (Submodule R M) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => smul_mono le_rfl⟩

Premises used: CovariantClass.mk, le_rfl, Submodule.smul_mono
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
⊢ HSMul.hSMul (β := Submodule R M) I ⊥ = ⊥

Tactic:
toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _

Premises used: Submodule.toAddSubmonoid_injective, AddSubmonoid.addSubmonoid_smul_bot
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
n : M
h : n ∈ N
rw : Membership.mem (γ := Submodule R M) ⊥ 0
⊢ Membership.mem (γ := Submodule R M) ⊥ (HSMul.hSMul.{v, u_1, u_1} (α := A) 0 n)

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
n : M
h : n ∈ N
⊢ Membership.mem (γ := Submodule R M) ⊥ 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
n : M
h : n ∈ N
⊢ Membership.mem (γ := Submodule R M) ⊥ 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N P : Submodule R M
⊢ (I • (N ⊔ P)).toAddSubmonoid = (I • N ⊔ I • P).toAddSubmonoid

Tactic:
simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]

Premises used: Submodule.smul_toAddSubmonoid, Submodule.sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
mn : A
hmn : mn ∈ I ⊔ J
p : M
hp : p ∈ N
obtain : ∀ (m : A) (hm : m ∈ I) (n : A) (hn : n ∈ J) (hmn : m + n ∈ I ⊔ J), (m + n) • p ∈ I • N ⊔ J • N
⊢ mn • p ∈ I • N ⊔ J • N

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
rw : m • p + n • p ∈ I • N ⊔ J • N
⊢ (m + n) • p ∈ I • N ⊔ J • N

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N

Tactic:
add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp

Premises used: Submodule.add_mem_sup, Submodule.smul_mem_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N

Tactic:
exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp

Premises used: Submodule.add_mem_sup, Submodule.smul_mem_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
B : Type u_2
inst_7 : Semiring B
inst_8 : Module R B
inst_9 : Module A B
inst_10 : Module B M
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R B M
inst_13 : IsScalarTower A B M
I : Submodule R A
J : Submodule R B
N : Submodule R M
⊢ (I • J) • N = I • J • N

Tactic:
le_antisymm
    (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij
      (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
      fun x y ↦ (add_smul x y t).symm ▸ add_mem)
    (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn
      (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
      fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)

Premises used: Iff.mpr, Submodule.smul_induction_on, le_antisymm, Submodule.smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
I : Submodule R A
t : ι → Submodule R M
⊢ (HSMul.hSMul (β := Submodule R M) I (⨆ (i : ι), t i)).toAddSubmonoid =
    toAddSubmonoid.{u, u_1} (R := R) (⨆ (i : ι), I • t i)

Tactic:
simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]

Premises used: AddSubmonoid.smul_iSup, Submodule.smul_toAddSubmonoid, Submodule.iSup_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
simp_rw : Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) 0
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (HSMul.hSMul.{v, u_1, u_1} (α := A) 0 s)

Tactic:
simp_rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) 0

Tactic:
apply zero_mem

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
x y : A
simp_rw :
  Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s) →
    Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (y • s) →
      Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s + y • s)
⊢ (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) x →
    (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) y →
      (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) (x + y)

Tactic:
simp_rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
x y : A
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s) →
    Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (y • s) →
      Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s + y • s)

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
⊢ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N = N

Tactic:
le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_

Premises used: Iff.mpr, le_antisymm, Submodule.smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
refine_1 : ∀ (r : A) (hr : Membership.mem (γ := Submodule R A) 1 r) (m : M) (hm : m ∈ N), r • m ∈ N
refine_2 : ∀ (m : M) (hm : m ∈ N), m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N
⊢ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N = N

Tactic:
refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_

Premises used: Iff.mpr, le_antisymm, Submodule.smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
r : A
hr : Membership.mem (γ := Submodule R A) 1 r
m : M
hm : m ∈ N
refine_1 : ∀ (r : R), HSMul.hSMul.{v, u_1, u_1} (α := A) ((LinearMap.toSpanSingleton R A 1 : (a : R) → A) r : A) m ∈ N
⊢ r • m ∈ N

Tactic:
obtain ⟨r, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
refine_1 : r • m ∈ N
⊢ HSMul.hSMul.{v, u_1, u_1} (α := A) ((LinearMap.toSpanSingleton R A 1 : (a : R) → A) r : A) m ∈ N

Tactic:
rw [LinearMap.toSpanSingleton_apply, smul_one_smul]

Premises used: LinearMap.toSpanSingleton_apply, smul_one_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N

Tactic:
N.smul_mem r hm

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N

Tactic:
exact N.smul_mem r hm

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
refine_2 : HSMul.hSMul.{v, u_1, u_1} (α := A) 1 m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N
⊢ m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N

Tactic:
rw [← one_smul A m]

Premises used: one_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ HSMul.hSMul.{v, u_1, u_1} (α := A) 1 m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N

Tactic:
smul_mem_smul (one_le.mp le_rfl) hm

Premises used: le_rfl, Set.Mem, Iff.mp, Submodule.smul_mem_smul, Submodule.one_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ HSMul.hSMul.{v, u_1, u_1} (α := A) 1 m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N

Tactic:
exact smul_mem_smul (one_le.mp le_rfl) hm

Premises used: le_rfl, Iff.mp, Submodule.smul_mem_smul, Submodule.one_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
⊢ (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M)

Tactic:
AddSubmonoid.smul_subset_smul

Premises used: AddSubmonoid.smul_subset_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
m n : A
hm : m ∈ M
hn : n ∈ N
⊢ m * n ∈ M * N

Tactic:
smul_mem_smul hm hn

Premises used: Set.Mem, Submodule.smul_mem_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N P : Submodule R A
⊢ M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

Tactic:
smul_le

Premises used: Set.Mem, Submodule.smul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
⊢ (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid

Tactic:
rfl

Premises used: Set.Mem, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
C : A → Prop
r : A
hr : r ∈ M * N
hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r

Tactic:
smul_induction_on hr hm ha

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
C : (r : A) → r ∈ M * N → Prop
mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯
add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯
r : A
hr : r ∈ M * N
⊢ C r hr

Tactic:
smul_induction_on' hr mem_mul_mem add

Premises used: Submodule.smul_induction_on'
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ M * ⊥ = ⊥

Tactic:
smul_bot _

Premises used: Submodule.smul_bot
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ ⊥ * M = ⊥

Tactic:
bot_smul _

Premises used: Submodule.bot_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
M N : Submodule R A
h : M = ⊥ ∨ N = ⊥
inl : ⊥ * N = ⊥
inr : M * ⊥ = ⊥
⊢ M * N = ⊥

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
N : Submodule R A
⊢ ⊥ * N = ⊥

Tactic:
bot_mul _

Premises used: Submodule.bot_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
M : Submodule R A
⊢ M * ⊥ = ⊥

Tactic:
mul_bot _

Premises used: Submodule.mul_bot
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
N : Submodule R A
⊢ ⊥ * N = ⊥

Tactic:
exacts [bot_mul _, mul_bot _]

Premises used: Submodule.bot_mul, Submodule.mul_bot
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ 1 * M = M

Tactic:
Submodule.one_smul _

Premises used: Submodule.one_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
h : ∀ m ∈ M, ∀ n ∈ N, Commute m n
⊢ M * N = N * M

Tactic:
toAddSubmonoid_injective <| AddSubmonoid.mul_comm_of_commute h

Premises used: Submodule.toAddSubmonoid_injective, AddSubmonoid.mul_comm_of_commute
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N P : Submodule R A
⊢ M * (N ⊔ P) = M * N ⊔ M * P

Tactic:
smul_sup _ _ _

Premises used: Set.Mem, setOf, Submodule.smul_sup
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N P : Submodule R A
⊢ (M ⊔ N) * P = M * P ⊔ N * P

Tactic:
sup_smul _ _ _

Premises used: Set.Mem, setOf, Submodule.sup_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M N : Submodule R A
⊢ (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A)

Tactic:
smul_subset_smul _ _

Premises used: Submodule.smul_subset_smul