awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
q : Q
n : N
⊢ ∃ (a : N ⊗[R] Q),
    Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) ((g : (a : N) → P) n ⊗ₜ[R] q : P ⊗[R] Q)

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

Premises used: Exists.intro, TensorProduct.tmul, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
q : Q
n : N
⊢ ∃ (a : N ⊗[R] Q),
    Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) ((g : (a : N) → P) n ⊗ₜ[R] q : P ⊗[R] Q)

Tactic:
exact ⟨n ⊗ₜ[R] q, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x y : P ⊗[R] Q
hx : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x
hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y
add :
  ∀ (x : N ⊗[R] Q),
    ∃ (a : N ⊗[R] Q),
      (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
        HAdd.hAdd (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q) y
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
y : P ⊗[R] Q
hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y
x : N ⊗[R] Q
add :
  ∀ (y : N ⊗[R] Q),
    ∃ (a : N ⊗[R] Q),
      (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
        HAdd.hAdd (α := P ⊗[R] Q) (β := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q)
          ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)
⊢ ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q) y

Tactic:
obtain ⟨y, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x y : N ⊗[R] Q
⊢ ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) (β := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q)
        ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)

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

Premises used: map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x y : N ⊗[R] Q
⊢ ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) (β := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q)
        ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)

Tactic:
exact ⟨x + y, map_add _ _ _⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
z : P ⊗[R] Q
zero : ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)
tmul :
  ∀ (p : P) (q : Q),
    ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (p ⊗ₜ[R] q : P ⊗[R] Q)
add :
  ∀ (x y : P ⊗[R] Q) (hx : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x)
    (hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y),
    ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x + y
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = z

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

Premises used: TensorProduct.tmul, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
nth_rewrite :
  Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (rTensor Q g.range.subtype))
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g)) (range (rTensor Q g.range.subtype))

Tactic:
nth_rewrite 1 [this]
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
rw :
  Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict))
    (range (rTensor Q g.range.subtype))
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (rTensor Q g.range.subtype))

Tactic:
rw [rTensor_comp]

Premises used: LinearMap.rTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Eq (α := Submodule R (TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)) (range (rTensor Q g.rangeRestrict)) ⊤
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict))
    (range (rTensor Q g.range.subtype))

Tactic:
apply range_comp_of_range_eq_top

Premises used: LinearMap.range_comp_of_range_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf :
  Function.Surjective (α := N ⊗[R] Q) (β := TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)
    (⇑(rTensor Q g.rangeRestrict) : (a : N ⊗[R] Q) → ↥g.range ⊗[R] Q)
⊢ Eq (α := Submodule R (TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)) (range (rTensor Q g.rangeRestrict)) ⊤

Tactic:
rw [range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
⊢ Function.Surjective (α := N ⊗[R] Q) (β := TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)
    (⇑(rTensor Q g.rangeRestrict) : (a : N ⊗[R] Q) → ↥g.range ⊗[R] Q)

Tactic:
apply rTensor_surjective

Premises used: LinearMap.rTensor_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
a :
  ∀ (x : Q) (x_1 : M),
    Eq (α := N ⊗[R] Q)
      (((((AlgebraTensorModule.curry (rTensor Q f ∘ₗ (↑(TensorProduct.comm R Q M) : Q ⊗[R] M →ₗ[R] M ⊗[R] Q)) :
                    Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] N ⊗[R] Q)
                x :
              M →ₗ[R] N ⊗[R] Q) :
            (a : M) → N ⊗[R] Q)
          x_1 :
        N ⊗[R] Q)
      (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q) ∘ₗ lTensor Q f) :
                    Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] N ⊗[R] Q)
                x :
              M →ₗ[R] N ⊗[R] Q) :
            (a : M) → N ⊗[R] Q)
          x_1 :
        N ⊗[R] Q)
⊢ Eq (α := Q ⊗[R] M →ₗ[R] N ⊗[R] Q) (rTensor Q f ∘ₗ (↑(TensorProduct.comm R Q M) : Q ⊗[R] M →ₗ[R] M ⊗[R] Q))
    ((↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q) ∘ₗ lTensor Q f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x : Q
x_1 : M
⊢ Eq (α := N ⊗[R] Q)
    (((((AlgebraTensorModule.curry (rTensor Q f ∘ₗ (↑(TensorProduct.comm R Q M) : Q ⊗[R] M →ₗ[R] M ⊗[R] Q)) :
                  Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                (a : Q) → M →ₗ[R] N ⊗[R] Q)
              x :
            M →ₗ[R] N ⊗[R] Q) :
          (a : M) → N ⊗[R] Q)
        x_1 :
      N ⊗[R] Q)
    (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q) ∘ₗ lTensor Q f) :
                  Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                (a : Q) → M →ₗ[R] N ⊗[R] Q)
              x :
            M →ₗ[R] N ⊗[R] Q) :
          (a : M) → N ⊗[R] Q)
        x_1 :
      N ⊗[R] Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
a :
  ∀ (x : Q) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      (((((AlgebraTensorModule.curry (rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q)) :
                    Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ lTensor Q g) :
                    Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ Eq (α := Q ⊗[R] N →ₗ[R] P ⊗[R] Q) (rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q))
    ((↑(TensorProduct.comm R Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ lTensor Q g)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x : Q
x_1 : N
⊢ Eq (α := P ⊗[R] Q)
    (((((AlgebraTensorModule.curry (rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q)) :
                  Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                (a : Q) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ lTensor Q g) :
                  Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                (a : Q) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
N' : Type u_6
P' : Type u_7
inst_5 : AddCommMonoid N'
inst_6 : AddCommMonoid P'
inst_7 : Module R N'
inst_8 : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective.{u_6 + 1, u_7 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw :
  Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P')
    (Function.comp (β := P ⊗[R] N') (⇑(lTensor P g') : (a : P ⊗[R] N') → P ⊗[R] P')
      (⇑(rTensor N' g) : (a : N ⊗[R] N') → P ⊗[R] N'))
⊢ Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P') (⇑(map g g') : (a : N ⊗[R] N') → P ⊗[R] P')

Tactic:
rw [← lTensor_comp_rTensor, coe_comp]

Premises used: LinearMap.lTensor_comp_rTensor, LinearMap.coe_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
N' : Type u_6
P' : Type u_7
inst_5 : AddCommMonoid N'
inst_6 : AddCommMonoid P'
inst_7 : Module R N'
inst_8 : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective.{u_6 + 1, u_7 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
⊢ Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P')
    (Function.comp (β := P ⊗[R] N') (⇑(lTensor P g') : (a : P ⊗[R] N') → P ⊗[R] P')
      (⇑(rTensor N' g) : (a : N ⊗[R] N') → P ⊗[R] N'))

Tactic:
Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)

Premises used: LinearMap.lTensor_surjective, LinearMap.rTensor_surjective, Function.Surjective.comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
N' : Type u_6
P' : Type u_7
inst_5 : AddCommMonoid N'
inst_6 : AddCommMonoid P'
inst_7 : Module R N'
inst_8 : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective.{u_6 + 1, u_7 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
⊢ Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P')
    (Function.comp (β := P ⊗[R] N') (⇑(lTensor P g') : (a : P ⊗[R] N') → P ⊗[R] P')
      (⇑(rTensor N' g) : (a : N ⊗[R] N') → P ⊗[R] N'))

Tactic:
exact Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)

Premises used: LinearMap.lTensor_surjective, LinearMap.rTensor_surjective, Function.Surjective.comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (M₂ := Q ⊗[R] P) (lTensor Q 0)) ⊤
rw₄ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (R₂ := R) (M₂ := Q ⊗[R] P) (τ₁₂ := RingHom.id R) 0) ⊤
rw₅ rw₆ : Eq (α := Submodule R (Q ⊗[R] M)) ⊤ ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))

Tactic:
rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]

Premises used: LinearMap.ker_comp, LinearMap.lTensor_zero, LinearMap.range_le_iff_comap, LinearMap.ker_zero, Function.Exact.linearMap_comp_eq_zero, LinearMap.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
rw : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (p + p') - (h p + h p')))
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (q ⊗ₜ[R] h (p + p') - HAdd.hAdd (α := Q ⊗[R] N) (q ⊗ₜ[R] h p) (q ⊗ₜ[R] h p'))

Tactic:
rw [← TensorProduct.tmul_add, ← TensorProduct.tmul_sub]

Premises used: TensorProduct.tmul_sub, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
a : h (p + p') - (h p + h p') ∈ f.range
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (p + p') - (h p + h p')))

Tactic:
apply le_comap_range_lTensor f

Premises used: le_comap_range_lTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
a :
  ∀ (hfg : g.ker = f.range) (hgh : RightInverse h (⇑g : (a : N) → P)) (p p' : P) (q : Q),
    h (p + p') - (h p + h p') ∈ f.range
⊢ h (p + p') - (h p + h p') ∈ f.range

Tactic:
rw [exact_iff] at hfg

Premises used: LinearMap.exact_iff
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : g.ker = f.range
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
⊢ h (p + p') - (h p + h p') ∈ f.range

Tactic:
simp only [← hfg, mem_ker, map_sub, map_add, hgh _, sub_self]

Premises used: map_sub, sub_self, map_add, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
r : R
p : P
q : Q
change :
  Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (q ⊗ₜ[R] h (r • p) - HSMul.hSMul (β := Q ⊗[R] N) r (q ⊗ₜ[R] h p))
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (HSub.hSub (α := Q ⊗[R] N) (β := Q ⊗[R] N)
      ((((LinearMap.flip (TensorProduct.mk R Q N) : (a : N) → Q →ₗ[R] Q ⊗[R] N) (h (r • p)) : Q →ₗ[R] Q ⊗[R] N) :
            (a : Q) → Q ⊗[R] N)
          q :
        Q ⊗[R] N)
      ((fun (x : Q ⊗[R] N) ↦ HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
          ((((LinearMap.flip (TensorProduct.mk R Q N) : (a : N) → Q →ₗ[R] Q ⊗[R] N) (h p) : Q →ₗ[R] Q ⊗[R] N) :
              (a : Q) → Q ⊗[R] N)
            q) :
        Q ⊗[R] N))

Tactic:
change q ⊗ₜ[R] (h (r • p)) - r • q ⊗ₜ[R] (h p) ∈ range (lTensor Q f)

Premises used: LinearMap.lTensor, LinearMap.range, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst_7 : AddCommGroup Q
inst_8 : Module R Q
hfg_1 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
r : R
p : P
q : Q
rw : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (r • p) - r • h p))
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (q ⊗ₜ[R] h (r • p) - HSMul.hSMul (β := Q ⊗[R] N) r (q ⊗ₜ[R] h p))

Tactic:
rw [← TensorProduct.tmul_smul, ← TensorProduct.tmul_sub]

Premises used: TensorProduct.tmul_sub, TensorProduct.tmul_smul