-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem TensorProduct.map_ker :
    ker (TensorProduct.map g g') = range (lTensor N f') ⊔ range (rTensor N' f)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ range (rTensor N' f)

Tactic:
rw [← Exact.linearMap_ker_eq (rTensor_exact N' hfg hg)]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ ker (rTensor N' g)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = Submodule.map (rTensor N' g) (range (lTensor N f'))

Tactic:
rw [range_eq_map, ← Submodule.map_comp, rTensor_comp_lTensor,
  Submodule.map_top]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = range (map g f')

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = Submodule.map (lTensor P f') (range (rTensor M' g))

Tactic:
rw [range_eq_top.mpr (rTensor_surjective M' hg), Submodule.map_top]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = range (lTensor P f')

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = range (map g f')

Tactic:
rw [← lTensor_comp_rTensor, range_eq_map, Submodule.map_comp,
  Submodule.map_top]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = Submodule.map (lTensor P f') (range (rTensor M' g))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) =
    Submodule.comap (rTensor N' g) (Submodule.map (rTensor N' g) (range (lTensor N f')))

Tactic:
apply congr_arg₂ _ rfl

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g') = Submodule.map (rTensor N' g) (range (lTensor N f'))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (map g g') = range (lTensor N f') ⊔ range (rTensor N' f)

Tactic:
rw [← lTensor_comp_rTensor]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ ker (lTensor P g' ∘ₗ rTensor N' g) = range (lTensor N f') ⊔ range (rTensor N' f)