R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.span R ((fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) =
    Submodule.span R {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ range (map f g) = Submodule.span R {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span, Set.mem_image,
  Set.mem_setOf_eq]
case e_s
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} = {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.span R ((fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) =
    Submodule.span R {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
congr
case e_s.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
case e_s
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} = {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
ext t
case e_s.h.mp
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} → t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}

case e_s.h.mpr
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t} → t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}
case e_s.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
constructor
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (fun a => ↑(map f g) a) (m ⊗ₜ[R] n) ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
case e_s.h.mp
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t} → t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
rintro ⟨_, ⟨⟨m, n, rfl⟩, rfl⟩⟩
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ ↑f m ⊗ₜ[R] ↑g n = (fun a => ↑(map f g) a) (m ⊗ₜ[R] n)
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (fun a => ↑(map f g) a) (m ⊗ₜ[R] n) ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}
use m, n
no goals
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ ↑f m ⊗ₜ[R] ↑g n = (fun a => ↑(map f g) a) (m ⊗ₜ[R] n)
simp only [map_tmul]
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ ↑f m ⊗ₜ[R] ↑g n ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}
case e_s.h.mpr
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t} → t ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}
rintro ⟨m, n, rfl⟩
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (fun a => ↑(map f g) a) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ ↑f m ⊗ₜ[R] ↑g n ∈ (fun a => ↑(map f g) a) '' {t | ∃ m n, m ⊗ₜ[R] n = t}
refine ⟨_, ⟨⟨m, n, rfl⟩, ?_⟩⟩
no goals
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.921730
inst✝¹³ : Monoid R'
R'' : Type ?u.921736
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.921754
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (fun a => ↑(map f g) a) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n
simp only [map_tmul]