awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N

Tactic:
have : Submodule.map N.subtype (I • ⊤) = I • N := by
    rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N
⊢ x ∈ HSMul.hSMul (β := Submodule R ↥N) I ⊤ ↔ (↑x : M) ∈ I • N

Tactic:
simp [← this, -map_smul'']

Premises used: Submodule.map_smul''
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
⊢ I • comap f S ≤ comap f (I • S)

Tactic:
Submodule.smul_le.mpr fun r hr x hx => ?_

Premises used: Iff.mpr, Set.Mem, Submodule.smul_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
refine : ∀ (r : R) (hr : r ∈ I) (x : M) (hx : x ∈ comap f S), r • x ∈ comap f (I • S)
⊢ I • comap f S ≤ comap f (I • S)

Tactic:
refine Submodule.smul_le.mpr fun r hr x hx => ?_

Premises used: Iff.mpr, Submodule.smul_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ Membership.mem (α := M') S ((f : (a : M) → M') x : M')

Tactic:
rw [Submodule.mem_comap] at hx ⊢

Premises used: Submodule.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : Membership.mem (α := M') S ((f : (a : M) → M') x : M')
rw : HSMul.hSMul (β := M') r ((f : (a : M) → M') x : M') ∈ I • S
⊢ Membership.mem (α := M') (I • S) ((f : (a : M) → M') (r • x) : M')

Tactic:
rw [f.map_smul]

Premises used: LinearMap.map_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : Membership.mem (α := M') S ((f : (a : M) → M') x : M')
⊢ HSMul.hSMul (β := M') r ((f : (a : M) → M') x : M') ∈ I • S

Tactic:
Submodule.smul_mem_smul hr hx

Premises used: Set.Mem, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : Membership.mem (α := M') S ((f : (a : M) → M') x : M')
⊢ HSMul.hSMul (β := M') r ((f : (a : M) → M') x : M') ∈ I • S

Tactic:
exact Submodule.smul_mem_smul hr hx

Premises used: Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ I • comap f p ≤ comap f (I • p)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
refine : comap f (I • p) ≤ I • comap f p
⊢ comap f (I • p) = I • comap f p

Tactic:
refine le_antisymm ?_ (by simp)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
rw : comap f (map f (I • comap f p))
| comap f (I • p)

Tactic:
rw [← Submodule.map_comap_eq_self hp, ← Submodule.map_smul'']

Premises used: Submodule.map_comap_eq_self, Submodule.map_smul''
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
conv_lhs : comap f (map f (I • comap f p)) ≤ I • comap f p
⊢ comap f (I • p) ≤ I • comap f p

Tactic:
conv_lhs => rw [← Submodule.map_comap_eq_self hp, ← Submodule.map_smul'']

Premises used: Submodule.map_comap_eq_self, Submodule.map_smul''
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
rw rw₁ : I • comap f p ≤ I • comap f p
⊢ comap f (map f (I • comap f p)) ≤ I • comap f p

Tactic:
rw [Submodule.comap_map_eq_of_injective hf]

Premises used: Submodule.comap_map_eq_of_injective
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
m x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ m)
m1 m2 : M
h : ∃ y ∈ I, y • m = m1
h_1 : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
rw : y1 • m + y2 • m = m1 + m2
rw₁ : m1 + y2 • m = m1 + m2
rw₂ rw₃ : m1 + m2 = m1 + m2
⊢ (y1 + y2) • m = m1 + m2

Tactic:
rw [add_smul, hy1, hy2]

Premises used: add_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
revert :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)

Tactic:
revert r
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) 0
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (HSMul.hSMul.{u, v, v} (α := R) 0 m)

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h : Membership.mem (γ := Submodule R R) (span R S) x
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h₁ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m)
h₂ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m + x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((x + x_1) • m)

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h : Membership.mem (γ := Submodule R R) (span R S) x
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h₁ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m)
h₂ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m + x_1 • m)

Tactic:
add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h : Membership.mem (γ := Submodule R R) (span R S) x
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h₁ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m)
h₂ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m + x_1 • m)

Tactic:
exact add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((x • x_1) • m)

Tactic:
rw [smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (x • x_1 • m)

Tactic:
smul_mem _ _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (x • x_1 • m)

Tactic:
exact smul_mem _ _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x : R
h : Membership.mem (γ := Submodule R R) (Ideal.span S) x
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) 0
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (HSMul.hSMul (β := M) x 0)

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x : R
h : Membership.mem (γ := Submodule R R) (Ideal.span S) x
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x : R
h : Membership.mem (γ := Submodule R R) (Ideal.span S) x
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x x_1 : M
h : Membership.mem (γ := Submodule R M) (span R T) x
h_1 : Membership.mem (γ := Submodule R M) (span R T) x_1
h₁ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x)
h₂ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x_1)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x + r • x_1)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • (x + x_1))

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x x_1 : M
h : Membership.mem (γ := Submodule R M) (span R T) x
h_1 : Membership.mem (γ := Submodule R M) (span R T) x_1
h₁ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x)
h₂ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x_1)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x + r • x_1)

Tactic:
add_mem (h₁ r hr) (h₂ r hr)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x x_1 : M
h : Membership.mem (γ := Submodule R M) (span R T) x
h_1 : Membership.mem (γ := Submodule R M) (span R T) x_1
h₁ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x)
h₂ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x_1)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x + r • x_1)

Tactic:
exact add_mem (h₁ r hr) (h₂ r hr)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
r' : R
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
mem :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
rw : Membership.mem (γ := Submodule R M) (span R (S • T)) ((r * r') • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • r' • m)

Tactic:
rw [← mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
r' : R
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
mem :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((r * r') • m)

Tactic:
mem _ (Ideal.mul_mem_right _ _ hr)

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
r' : R
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
mem :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((r * r') • m)

Tactic:
exact mem _ (Ideal.mul_mem_right _ _ hr)

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
⊢ ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)

Tactic:
refine span_induction (fun m hm r hr ↦ span_induction
      (fun r hr ↦ subset_span ⟨r, hr, m, hm, rfl⟩)
      (by rw [zero_smul]; exact zero_mem _)
      (fun _ _ _ _ h₁ h₂ ↦ by rw [add_smul]; exact add_mem h₁ h₂)
      (fun _ _ _ h ↦ by rw [smul_assoc]; exact smul_mem _ _ h) hr)
      (fun _ _ ↦ by rw [smul_zero]; exact zero_mem _)
      (fun _ _ _ _ h₁ h₂ r hr ↦ by rw [smul_add]; exact add_mem (h₁ r hr) (h₂ r hr))
      (fun r' m hm mem r hr ↦ by rw [← mul_smul]; exact mem _ (Ideal.mul_mem_right _ _ hr)) hm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
s : R
hs : s ∈ S
t : M
ht : t ∈ T
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) s t ∈
    (↑(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span S) (span R T)) : Set M)

Tactic:
smul_mem_smul (subset_span hs) (subset_span ht)

Premises used: Set.Mem, Submodule.subset_span, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
s : R
hs : s ∈ S
t : M
ht : t ∈ T
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) s t ∈
    (↑(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span S) (span R T)) : Set M)

Tactic:
exact smul_mem_smul (subset_span hs) (subset_span ht)

Premises used: Submodule.subset_span, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
s : Set M
x : M
rw :
  Ideal.IsTwoSided (Ideal.span (↑I : Set R)) →
    ∀ {s : Set M} {x : M},
      x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span (↑I : Set R)) (span R s) ↔
        Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R s) ↔ Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x

Tactic:
rw [← I.span_eq] at *

Premises used: Ideal.span_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : Ideal.IsTwoSided (Ideal.span (↑I : Set R))
s : Set M
x : M
rw :
  Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x ↔
    Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
rw₁ rw₂ :
  Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x ↔
    Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x
⊢ x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span (↑I : Set R)) (span R s) ↔
    Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x

Tactic:
rw [Submodule.span_smul_span, I.span_eq]

Premises used: Ideal.span_eq, Submodule.span_smul_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
mp :
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f)) →
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x
mpr :
  (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x) →
    x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f)) ↔
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ (a.sum fun (i : ι) (c : R) ↦ c • f i) ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))

Tactic:
Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, Submodule.sum_mem, Finsupp.sum, Submodule.subset_span, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ (a.sum fun (i : ι) (c : R) ↦ c • f i) ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))

Tactic:
exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _

Premises used: Set.mem_range_self, Submodule.sum_mem, Submodule.subset_span, Submodule.smul_mem_smul