-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem LinearMap.lTensor_surjective (hg : Function.Surjective g) :
    Function.Surjective (lTensor Q g)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(lTensor Q g)

Tactic:
intro z

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
z : Q ⊗[R] P
⊢ ∃ a, (lTensor Q g) a = z

Proof state:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] P
hx : ∃ a, (lTensor Q g) a = x
hy : ∃ a, (lTensor Q g) a = y
⊢ ∃ a, (lTensor Q g) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Result:
case add.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : Q ⊗[R] P
hy : ∃ a, (lTensor Q g) a = y
x : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + y

Proof state:
case add.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + (lTensor Q g) y

Tactic:
exact ⟨x + y, map_add _ _ _⟩

Result:
no goals

Proof state:
case tmul.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
n : N
⊢ ∃ a, (lTensor Q g) a = q ⊗ₜ[R] g n

Tactic:
exact ⟨q ⊗ₜ[R] n, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
z : Q ⊗[R] P
⊢ ∃ a, (lTensor Q g) a = z

Tactic:
induction z with
| zero => exact ⟨0, map_zero _⟩
| tmul q p =>
  obtain ⟨n, rfl⟩ := hg p
  exact ⟨q ⊗ₜ[R] n, rfl⟩
| add x y hx hy =>
  obtain ⟨x, rfl⟩ := hx
  obtain ⟨y, rfl⟩ := hy
  exact ⟨x + y, map_add _ _ _⟩

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
⊢ ∃ a, (lTensor Q g) a = 0

Tactic:
exact ⟨0, map_zero _⟩

Result:
no goals

Proof state:
case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
p : P
⊢ ∃ a, (lTensor Q g) a = q ⊗ₜ[R] p

Tactic:
obtain ⟨n, rfl⟩ := hg p

Result:
case tmul.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
n : N
⊢ ∃ a, (lTensor Q g) a = q ⊗ₜ[R] g n

Proof state:
case add.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : Q ⊗[R] P
hy : ∃ a, (lTensor Q g) a = y
x : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + y

Tactic:
obtain ⟨y, rfl⟩ := hy

Result:
case add.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + (lTensor Q g) y