-- Mathlib/Algebra/Algebra/Operations.lean
theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M) * (y • N)

Proof state:
case h.refine_1.intro.intro.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
x✝¹ x✝ : A
hn : (x * y) • x✝¹ ∈ x • M * y • N
hm : (x * y) • x✝ ∈ x • M * y • N
⊢ (x * y) • x✝¹ + (x * y) • x✝ ∈ x • M * y • N

Tactic:
exact Submodule.add_mem _ hn hm

Result:
no goals

Proof state:
case h.refine_2.intro.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
m : A
hm : m ∈ ↑M
n : A
hn : n ∈ ↑N
⊢ (DistribMulAction.toLinearMap R A x) m * (DistribMulAction.toLinearMap R A y) n ∈ (x * y) • (M * N)

Tactic:
simp_rw [DistribMulAction.toLinearMap_apply, smul_mul_smul_comm]

Result:
case h.refine_2.intro.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
m : A
hm : m ∈ ↑M
n : A
hn : n ∈ ↑N
⊢ (x * y) • (m * n) ∈ (x * y) • (M * N)

Proof state:
case h.refine_2.intro.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
m : A
hm : m ∈ ↑M
n : A
hn : n ∈ ↑N
⊢ (x * y) • (m * n) ∈ (x * y) • (M * N)

Tactic:
exact smul_mem_pointwise_smul _ _ _ (mul_mem_mul hm hn)

Result:
no goals

Proof state:
case h.refine_1.intro.intro.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ (x * y) • (m * n) ∈ x • M * y • N

Tactic:
rw [mul_smul_mul_comm]

Result:
case h.refine_1.intro.intro.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ x • m * y • n ∈ x • M * y • N

Proof state:
case h.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
⊢ ∀ m ∈ x • M, ∀ n ∈ y • N, m * n ∈ (x * y) • (M * N)

Tactic:
rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩

Result:
case h.refine_2.intro.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
m : A
hm : m ∈ ↑M
n : A
hn : n ∈ ↑N
⊢ (DistribMulAction.toLinearMap R A x) m * (DistribMulAction.toLinearMap R A y) n ∈ (x * y) • (M * N)

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
⊢ x✝ ∈ (x * y) • (M * N) ↔ x✝ ∈ x • M * y • N

Tactic:
refine ⟨?_, fun hx ↦ Submodule.mul_induction_on hx ?_ fun _ _ hx hy ↦ Submodule.add_mem _ hx hy⟩

Result:
case h.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
⊢ x✝ ∈ (x * y) • (M * N) → x✝ ∈ x • M * y • N

case h.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
hx : x✝ ∈ x • M * y • N
⊢ ∀ m ∈ x • M, ∀ n ∈ y • N, m * n ∈ (x * y) • (M * N)

Proof state:
case h.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
⊢ x✝ ∈ (x * y) • (M * N) → x✝ ∈ x • M * y • N

Tactic:
rintro ⟨_, hx, rfl⟩

Result:
case h.refine_1.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
⊢ (DistribMulAction.toLinearMap R A (x * y)) w✝ ∈ x • M * y • N

Proof state:
case h.refine_1.intro.intro.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ x • m * y • n ∈ x • M * y • N

Tactic:
exact mul_mem_mul (smul_mem_pointwise_smul m x M hm) (smul_mem_pointwise_smul n y N hn)

Result:
no goals

Proof state:
case h.refine_1.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
⊢ (x * y) • w✝ ∈ x • M * y • N

Tactic:
refine Submodule.mul_induction_on hx (fun m hm n hn ↦ ?_) (fun _ _ hn hm ↦ ?_)

Result:
case h.refine_1.intro.intro.refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ (x * y) • (m * n) ∈ x • M * y • N

case h.refine_1.intro.intro.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
x✝¹ x✝ : A
hn : (x * y) • x✝¹ ∈ x • M * y • N
hm : (x * y) • x✝ ∈ x • M * y • N
⊢ (x * y) • (x✝¹ + x✝) ∈ x • M * y • N

Proof state:
case h.refine_1.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
⊢ (DistribMulAction.toLinearMap R A (x * y)) w✝ ∈ x • M * y • N

Tactic:
rw [DistribMulAction.toLinearMap_apply]

Result:
case h.refine_1.intro.intro
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
⊢ (x * y) • w✝ ∈ x • M * y • N

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
⊢ (x * y) • (M * N) = x • M * y • N

Tactic:
ext

Result:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
x✝ : A
⊢ x✝ ∈ (x * y) • (M * N) ↔ x✝ ∈ x • M * y • N

Proof state:
case h.refine_1.intro.intro.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
x✝¹ x✝ : A
hn : (x * y) • x✝¹ ∈ x • M * y • N
hm : (x * y) • x✝ ∈ x • M * y • N
⊢ (x * y) • (x✝¹ + x✝) ∈ x • M * y • N

Tactic:
rw [smul_add]

Result:
case h.refine_1.intro.intro.refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
x y : R
w✝ : A
hx : w✝ ∈ ↑(M * N)
x✝¹ x✝ : A
hn : (x * y) • x✝¹ ∈ x • M * y • N
hm : (x * y) • x✝ ∈ x • M * y • N
⊢ (x * y) • x✝¹ + (x * y) • x✝ ∈ x • M * y • N