-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem LinearMap.rTensor_range :
    range (rTensor Q g) =
      range (rTensor Q (Submodule.subtype (range 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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q (range g).subtype ∘ₗ rTensor Q g.rangeRestrict) = range (rTensor Q (range g).subtype)

Tactic:
apply range_comp_of_range_eq_top

Result:
case hf
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q g.rangeRestrict) = ⊤

Proof state:
case hf.hg
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑g.rangeRestrict

Tactic:
rw [← range_eq_top, range_rangeRestrict]

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
⊢ range (rTensor Q g) = range (rTensor Q (range g).subtype)

Tactic:
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl

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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q g) = range (rTensor Q (range g).subtype)

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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q ((range g).subtype ∘ₗ g.rangeRestrict)) = range (rTensor Q (range g).subtype)

Tactic:
rw [rTensor_comp]

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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q (range g).subtype ∘ₗ rTensor Q g.rangeRestrict) = range (rTensor Q (range g).subtype)

Proof state:
case hf
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q g.rangeRestrict) = ⊤

Tactic:
rw [range_eq_top]

Result:
case hf
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(rTensor Q g.rangeRestrict)

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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q g) = range (rTensor Q (range g).subtype)

Tactic:
nth_rewrite 1 [this]

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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ range (rTensor Q ((range g).subtype ∘ₗ g.rangeRestrict)) = range (rTensor Q (range g).subtype)

Proof state:
case hf
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(rTensor Q g.rangeRestrict)

Tactic:
apply rTensor_surjective

Result:
case hf.hg
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
this : g = (range g).subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑g.rangeRestrict