[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
n : N
p : Submodule R M
q : Submodule R N
hm : m ∈ p
hn : n ∈ q
⊢ ↑(↑f ↑{ val := m, property := hm }) n = ↑(↑f m) n
[PROOFSTEP]
rfl
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) = span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) ≤ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
rw [map₂_le]
[GOAL]
case a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (m : M), m ∈ span R s → ∀ (n : N), n ∈ span R t → ↑(↑f m) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
apply @span_induction' R M _ _ _ s
[GOAL]
case a.Hs
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M), x ∈ s → ∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intro a ha
[GOAL]
case a.Hs
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f a) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
apply @span_induction' R N _ _ _ t
[GOAL]
case a.Hs.Hs
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x : N), x ∈ t → ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ↑(↑f a) 0 ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x : N),
    x ∈ span R t →
      ∀ (y : N),
        y ∈ span R t →
          ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
            ↑(↑f a) y ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
              ↑(↑f a) (x + y) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R) (x : N),
    x ∈ span R t →
      ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
        ↑(↑f a) (a_1 • x) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intro b hb
[GOAL]
case a.Hs.Hs
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
b : N
hb : b ∈ t
⊢ ↑(↑f a) b ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ↑(↑f a) 0 ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x : N),
    x ∈ span R t →
      ∀ (y : N),
        y ∈ span R t →
          ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
            ↑(↑f a) y ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
              ↑(↑f a) (x + y) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R) (x : N),
    x ∈ span R t →
      ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
        ↑(↑f a) (a_1 • x) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
exact subset_span ⟨_, _, ‹_›, ‹_›, rfl⟩
[GOAL]
case a.Hs.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ↑(↑f a) 0 ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x : N),
    x ∈ span R t →
      ∀ (y : N),
        y ∈ span R t →
          ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
            ↑(↑f a) y ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
              ↑(↑f a) (x + y) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.Hs.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R) (x : N),
    x ∈ span R t →
      ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
        ↑(↑f a) (a_1 • x) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
all_goals intros;
  simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
    LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.Hs.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ↑(↑f a) 0 ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.Hs.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ↑(↑f a) 0 ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.Hs.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x : N),
    x ∈ span R t →
      ∀ (y : N),
        y ∈ span R t →
          ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
            ↑(↑f a) y ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
              ↑(↑f a) (x + y) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.Hs.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
x✝ : N
hx✝ : x✝ ∈ span R t
y✝ : N
hy✝ : y✝ ∈ span R t
a✝¹ : ↑(↑f a) x✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
a✝ : ↑(↑f a) y✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
⊢ ↑(↑f a) (x✝ + y✝) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.Hs.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R) (x : N),
    x ∈ span R t →
      ↑(↑f a) x ∈ span R (image2 (fun m n => ↑(↑f m) n) s t) →
        ↑(↑f a) (a_1 • x) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.Hs.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
ha : a ∈ s
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R t
a✝ : ↑(↑f a) x✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
⊢ ↑(↑f a) (a✝¹ • x✝) ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (n : N), n ∈ span R t → ↑(↑f 0) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.H0
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
n✝ : N
a✝ : n✝ ∈ span R t
⊢ ↑(↑f 0) n✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (x : M),
    x ∈ span R s →
      ∀ (y : M),
        y ∈ span R s →
          (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
            (∀ (n : N), n ∈ span R t → ↑(↑f y) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
              ∀ (n : N), n ∈ span R t → ↑(↑f (x + y)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.H1
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
x✝ : M
hx✝ : x✝ ∈ span R s
y✝ : M
hy✝ : y✝ ∈ span R s
a✝² : ∀ (n : N), n ∈ span R t → ↑(↑f x✝) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
a✝¹ : ∀ (n : N), n ∈ span R t → ↑(↑f y✝) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
n✝ : N
a✝ : n✝ ∈ span R t
⊢ ↑(↑f (x✝ + y✝)) n✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ ∀ (a : R) (x : M),
    x ∈ span R s →
      (∀ (n : N), n ∈ span R t → ↑(↑f x) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)) →
        ∀ (n : N), n ∈ span R t → ↑(↑f (a • x)) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
intros
[GOAL]
case a.H2
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a✝² : R
x✝ : M
hx✝ : x✝ ∈ span R s
a✝¹ : ∀ (n : N), n ∈ span R t → ↑(↑f x✝) n ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
n✝ : N
a✝ : n✝ ∈ span R t
⊢ ↑(↑f (a✝² • x✝)) n✝ ∈ span R (image2 (fun m n => ↑(↑f m) n) s t)
[PROOFSTEP]
simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add, LinearMap.zero_apply, LinearMap.add_apply,
  LinearMap.smul_apply, SMulHomClass.map_smul]
[GOAL]
case a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ span R (image2 (fun m n => ↑(↑f m) n) s t) ≤ map₂ f (span R s) (span R t)
[PROOFSTEP]
rw [span_le]
[GOAL]
case a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
⊢ image2 (fun m n => ↑(↑f m) n) s t ⊆ ↑(map₂ f (span R s) (span R t))
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Set M
t : Set N
a : M
b : N
ha : a ∈ s
hb : b ∈ t
⊢ (fun m n => ↑(↑f m) n) a b ∈ ↑(map₂ f (span R s) (span R t))
[PROOFSTEP]
exact apply_mem_map₂ _ (subset_span ha) (subset_span hb)
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n ∈ ⊥
⊢ ↑(↑f m) n ∈ ⊥
[PROOFSTEP]
rw [Submodule.mem_bot] at hn 
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ ↑(↑f m) n ∈ ⊥
[PROOFSTEP]
rw [hn, LinearMap.map_zero]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥
[PROOFSTEP]
simp only [mem_bot]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
q : Submodule R N
m : M
hm : m ∈ ⊥
n : N
hn : n ∈ q
⊢ ↑(↑f m) n ∈ ⊥
[PROOFSTEP]
rw [Submodule.mem_bot] at hm ⊢
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
q : Submodule R N
m : M
hm : m = 0
n : N
hn : n ∈ q
⊢ ↑(↑f m) n = 0
[PROOFSTEP]
rw [hm, LinearMap.map_zero₂]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
q : Submodule R N
⊢ image2 (fun m n => ↑(↑f m) n) ↑p ↑q ⊆ ↑(map₂ f p q)
[PROOFSTEP]
rintro _ ⟨i, j, hi, hj, rfl⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
q : Submodule R N
i : M
j : N
hi : i ∈ ↑p
hj : j ∈ ↑q
⊢ (fun m n => ↑(↑f m) n) i j ∈ ↑(map₂ f p q)
[PROOFSTEP]
exact apply_mem_map₂ _ hi hj
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = span R (image2 (fun m n => ↑(↑f m) n) ↑p ↑q)
[PROOFSTEP]
rw [← map₂_span_span, span_eq, span_eq]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
q : Submodule R N
⊢ map₂ (LinearMap.flip f) q p = map₂ f p q
[PROOFSTEP]
rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b => ↑(↑(LinearMap.flip f) b) a) ↑p ↑q) = span R (image2 (fun m n => ↑(↑f m) n) ↑p ↑q)
[PROOFSTEP]
rfl
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t
[PROOFSTEP]
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
  simpa only [span_eq] using this
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : ι → Submodule R M
t : Submodule R N
this : map₂ f (⨆ (i : ι), span R ↑(s i)) (span R ↑t) = ⨆ (i : ι), map₂ f (span R ↑(s i)) (span R ↑t)
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t
[PROOFSTEP]
simpa only [span_eq] using this
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ (i : ι), span R ↑(s i)) (span R ↑t) = ⨆ (i : ι), map₂ f (span R ↑(s i)) (span R ↑t)
[PROOFSTEP]
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), map₂ f s (t i)
[PROOFSTEP]
suffices map₂ f (span R s) (⨆ i, span R (t i : Set N)) = ⨆ i, map₂ f (span R s) (span R (t i)) by
  simpa only [span_eq] using this
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Submodule R M
t : ι → Submodule R N
this : map₂ f (span R ↑s) (⨆ (i : ι), span R ↑(t i)) = ⨆ (i : ι), map₂ f (span R ↑s) (span R ↑(t i))
⊢ map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), map₂ f s (t i)
[PROOFSTEP]
simpa only [span_eq] using this
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ (i : ι), span R ↑(t i)) = ⨆ (i : ι), map₂ f (span R ↑s) (span R ↑(t i))
[PROOFSTEP]
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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)
[PROOFSTEP]
funext
[GOAL]
case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝
[PROOFSTEP]
rw [map₂_eq_span_image2]
[GOAL]
case h
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝
[PROOFSTEP]
apply le_antisymm
[GOAL]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝
[PROOFSTEP]
rw [span_le, Set.image2_subset_iff]
[GOAL]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
intro x hx y hy
[GOAL]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
obtain ⟨a, rfl⟩ := mem_span_singleton.1 hx
[GOAL]
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
rw [f.map_smul]
[GOAL]
case h.a.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
exact smul_mem _ a (mem_map_of_mem hy)
[GOAL]
case h.a
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
rintro _ ⟨n, hn, rfl⟩
[GOAL]
case h.a.intro.intro
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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✝)
[PROOFSTEP]
exact subset_span ⟨m, n, mem_span_singleton_self m, hn, rfl⟩
[GOAL]
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
s : Submodule R M
n : N
⊢ map₂ f s (span R {n}) = map (↑(LinearMap.flip f) n) s
[PROOFSTEP]
rw [← map₂_span_singleton_eq_map, map₂_flip]
