-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_range_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    range (map f g) = Submodule.span R { t | ∃ m n, f m ⊗ₜ g n = t }

Proof state:
case e_s.h.mpr
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t} → t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
rintro ⟨m, n, rfl⟩

Result:
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ f m ⊗ₜ[R] g n ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}

Proof state:
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n

Tactic:
simp only [map_tmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.span R (⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
congr

Result:
case e_s
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} = {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Proof state:
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (map f g) (m ⊗ₜ[R] n) ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
use m, n

Result:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ f m ⊗ₜ[R] g n = (map f g) (m ⊗ₜ[R] n)

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ range (map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span, Set.mem_image,
  Set.mem_setOf_eq]

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.span R (⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Proof state:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ f m ⊗ₜ[R] g n = (map f g) (m ⊗ₜ[R] n)

Tactic:
simp only [map_tmul]

Result:
no goals

Proof state:
case e_s
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} = {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
ext t

Result:
case e_s.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Proof state:
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ f m ⊗ₜ[R] g n ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
refine ⟨_, ⟨⟨m, n, rfl⟩, ?_⟩⟩

Result:
case e_s.h.mpr.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n

Proof state:
case e_s.h.mp
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} → t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

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

Result:
case e_s.h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
m : M
n : N
⊢ (map f g) (m ⊗ₜ[R] n) ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}