case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ map₂ f (span R {m}) x✝ = map (↑f m) x✝
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
⊢ map₂ f (span R {m}) = map (↑f m)
funext
case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝) = map (↑f m) x✝
case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ map₂ f (span R {m}) x✝ = map (↑f m) x✝
rw [map₂_eq_span_image2]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝) ≤ map (↑f m) x✝

case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ map (↑f m) x✝ ≤ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝)
case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝) = map (↑f m) x✝
apply le_antisymm
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ ∀ (x : M), x ∈ ↑(span R {m}) → ∀ (y : N), y ∈ ↑x✝ → ↑(↑f x) y ∈ ↑(map (↑f m) x✝)
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝) ≤ map (↑f m) x✝
rw [span_le, Set.image2_subset_iff]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
x : M
hx : x ∈ ↑(span R {m})
y : N
hy : y ∈ ↑x✝
⊢ ↑(↑f x) y ∈ ↑(map (↑f m) x✝)
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ ∀ (x : M), x ∈ ↑(span R {m}) → ∀ (y : N), y ∈ ↑x✝ → ↑(↑f x) y ∈ ↑(map (↑f m) x✝)
intro x hx y hy
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
y : N
hy : y ∈ ↑x✝
a : R
hx : a • m ∈ ↑(span R {m})
⊢ ↑(↑f (a • m)) y ∈ ↑(map (↑f m) x✝)
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
x : M
hx : x ∈ ↑(span R {m})
y : N
hy : y ∈ ↑x✝
⊢ ↑(↑f x) y ∈ ↑(map (↑f m) x✝)
obtain ⟨a, rfl⟩ := mem_span_singleton.1 hx
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
y : N
hy : y ∈ ↑x✝
a : R
hx : a • m ∈ ↑(span R {m})
⊢ ↑(a • ↑f m) y ∈ ↑(map (↑f m) x✝)
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
y : N
hy : y ∈ ↑x✝
a : R
hx : a • m ∈ ↑(span R {m})
⊢ ↑(↑f (a • m)) y ∈ ↑(map (↑f m) x✝)
rw [f.map_smul]
no goals
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
y : N
hy : y ∈ ↑x✝
a : R
hx : a • m ∈ ↑(span R {m})
⊢ ↑(a • ↑f m) y ∈ ↑(map (↑f m) x✝)
exact smul_mem _ a (mem_map_of_mem hy)
case h.a.intro.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
n : N
hn : n ∈ ↑x✝
⊢ ↑(↑f m) n ∈ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝)
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
⊢ map (↑f m) x✝ ≤ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝)
rintro _ ⟨n, hn, rfl⟩
no goals
case h.a.intro.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
x✝ : Submodule R N
n : N
hn : n ∈ ↑x✝
⊢ ↑(↑f m) n ∈ span R (image2 (fun m n => ↑(↑f m) n) ↑(span R {m}) ↑x✝)
exact subset_span ⟨m, n, mem_span_singleton_self m, hn, rfl⟩