-- Mathlib/LinearAlgebra/Span/Basic.lean
/-- If a bilinear map takes values in a submodule along two sets, then the same is true along
the span of these sets. -/
lemma _root_.LinearMap.BilinMap.apply_apply_mem_of_mem_span {R M N P : Type*} [CommSemiring R]
    [AddCommGroup M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P]
    (P' : Submodule R P) (s : Set M) (t : Set N)
    (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ x ∈ s, ∀ y ∈ t, B x y ∈ P')
    (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t) :
    B x y ∈ P'

Proof state:
case add_left
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u₁ u₂ : M
v : N
hu₁ : u₁ ∈ span R s
hu₂ : u₂ ∈ span R s
hv : v ∈ span R t
huv₁ : (B u₁) v ∈ P'
huv₂ : (B u₂) v ∈ P'
⊢ (B (u₁ + u₂)) v ∈ P'

Tactic:
simpa using add_mem huv₁ huv₂

Result:
no goals

Proof state:
case smul_right
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B u) (t • v) ∈ P'

Tactic:
simpa using Submodule.smul_mem _ _ huv

Result:
no goals

Proof state:
case smul_left
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B (t • u)) v ∈ P'

Tactic:
simpa using Submodule.smul_mem _ _ huv

Result:
no goals

Proof state:
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
hx : x ∈ span R s
hy : y ∈ span R t
⊢ (B x) y ∈ P'

Tactic:
induction hx, hy using span_induction₂ with
| mem_mem u v hu hv => exact hB u hu v hv
| zero_left v hv => simp
| zero_right u hu => simp
| add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
| add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
| smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
| smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv

Result:
no goals

Proof state:
case mem_mem
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v : N
hu : u ∈ s
hv : v ∈ t
⊢ (B u) v ∈ P'

Tactic:
exact hB u hu v hv

Result:
no goals

Proof state:
case zero_right
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
hu : u ∈ span R s
⊢ (B u) 0 ∈ P'

Tactic:
simp

Result:
no goals

Proof state:
case zero_left
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y v : N
hv : v ∈ span R t
⊢ (B 0) v ∈ P'

Tactic:
simp

Result:
no goals

Proof state:
case add_right
R : Type u_10
M : Type u_11
N : Type u_12
P : Type u_13
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v₁ v₂ : N
hu : u ∈ span R s
hv₁ : v₁ ∈ span R t
hv₂ : v₂ ∈ span R t
huv₁ : (B u) v₁ ∈ P'
huv₂ : (B u) v₂ ∈ P'
⊢ (B u) (v₁ + v₂) ∈ P'

Tactic:
simpa using add_mem huv₁ huv₂

Result:
no goals