awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
hgh : RightInverse h (⇑g : (a : N) → P)
y : Q ⊗[R] N
⊢ Eq (α := Q ⊗[R] P)
    ((toFun Q hfg : (a : Q ⊗[R] N ⧸ (lTensor Q f).range) → Q ⊗[R] P) (Submodule.Quotient.mk y) : Q ⊗[R] P)
    ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y : Q ⊗[R] P)

Tactic:
simp only [lTensor.toFun, Submodule.liftQ_apply]

Premises used: lTensor.toFun, Submodule.liftQ_apply
-- 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 : 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)
rw : Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor Q g)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g))
⊢ Exact (M := Q ⊗[R] M) (N := Q ⊗[R] N) (P := Q ⊗[R] P) (⇑(lTensor Q f) : (a : Q ⊗[R] M) → Q ⊗[R] N)
    (⇑(lTensor Q g) : (a : Q ⊗[R] N) → Q ⊗[R] P)

Tactic:
rw [exact_iff, ← Submodule.ker_mkQ (p := range (lTensor Q f)),
    ← lTensor.inverse_comp_lTensor Q hfg hg]

Premises used: lTensor.inverse_comp_lTensor, LinearMap.lTensor, LinearMap.range, Submodule.ker_mkQ, 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 : 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)
a : Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g)) (ker (lTensor Q g))
⊢ Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor Q g)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g))

Tactic:
apply symm

Premises used: symm
-- 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 : 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)
a : Eq (α := Submodule R (Q ⊗[R] P)) (ker (lTensor.inverse Q hfg hg)) ⊥
⊢ Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g)) (ker (lTensor Q g))

Tactic:
apply LinearMap.ker_comp_of_ker_eq_bot

Premises used: LinearMap.ker_comp_of_ker_eq_bot
-- 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 : 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)
a :
  Injective (α := Q ⊗[R] P) (β := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (⇑(lTensor.inverse Q hfg hg) : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (ker (lTensor.inverse Q hfg hg)) ⊥

Tactic:
rw [LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- 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 : 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)
⊢ Injective (α := Q ⊗[R] P) (β := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (⇑(lTensor.inverse Q hfg hg) : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)

Tactic:
(lTensor.equiv Q hfg hg).symm.injective

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, lTensor.equiv, TensorProduct, LinearEquiv.injective
-- 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 : 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)
⊢ Injective (α := Q ⊗[R] P) (β := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (⇑(lTensor.inverse Q hfg hg) : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)

Tactic:
exact (lTensor.equiv Q hfg hg).symm.injective

Premises used: LinearEquiv.symm, lTensor.equiv, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : Type u_5
inst_3 : AddCommGroup Q
inst_4 : Module R Q
N : Submodule R M
rw :
  Exact (M := TensorProduct.{u_1, u_5, u_2} R Q ↥N) (N := Q ⊗[R] M) (P := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N))
    (⇑(lTensor Q N.subtype) : (a : Q ⊗[R] ↥N) → Q ⊗[R] M) (⇑(lTensor Q N.mkQ) : (a : Q ⊗[R] M) → Q ⊗[R] (M ⧸ N))
⊢ Eq (α := Submodule R (Q ⊗[R] M)) (ker (M₂ := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N)) (lTensor Q N.mkQ))
    (range (lTensor Q N.subtype))

Tactic:
rw [← exact_iff]

Premises used: LinearMap.exact_iff
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : Type u_5
inst_3 : AddCommGroup Q
inst_4 : Module R Q
N : Submodule R M
⊢ Exact (M := TensorProduct.{u_1, u_5, u_2} R Q ↥N) (N := Q ⊗[R] M) (P := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N))
    (⇑(lTensor Q N.subtype) : (a : Q ⊗[R] ↥N) → Q ⊗[R] M) (⇑(lTensor Q N.mkQ) : (a : Q ⊗[R] M) → Q ⊗[R] (M ⧸ N))

Tactic:
lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)

Premises used: LinearMap.exact_subtype_mkQ, lTensor_exact, Submodule.mkQ_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : Type u_5
inst_3 : AddCommGroup Q
inst_4 : Module R Q
N : Submodule R M
⊢ Exact (M := TensorProduct.{u_1, u_5, u_2} R Q ↥N) (N := Q ⊗[R] M) (P := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N))
    (⇑(lTensor Q N.subtype) : (a : Q ⊗[R] ↥N) → Q ⊗[R] M) (⇑(lTensor Q N.mkQ) : (a : Q ⊗[R] M) → Q ⊗[R] (M ⧸ N))

Tactic:
exact lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)

Premises used: LinearMap.exact_subtype_mkQ, lTensor_exact, Submodule.mkQ_surjective
-- 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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (M₂ := P ⊗[R] Q) (rTensor Q 0)) ⊤
rw₄ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (R₂ := R) (M₂ := P ⊗[R] Q) (τ₁₂ := RingHom.id R) 0) ⊤
rw₅ rw₆ : Eq (α := Submodule R (M ⊗[R] Q)) ⊤ ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))

Tactic:
rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_zero, ker_zero]

Premises used: LinearMap.ker_comp, LinearMap.range_le_iff_comap, LinearMap.ker_zero, Function.Exact.linearMap_comp_eq_zero, LinearMap.rTensor_comp, LinearMap.rTensor_zero
-- 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 (N ⊗[R] Q)) (range (rTensor Q f)) ((h (p + p') - (h p + h p')) ⊗ₜ[R] q)
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f))
    (h (p + p') ⊗ₜ[R] q - HAdd.hAdd (α := N ⊗[R] Q) (h p ⊗ₜ[R] q) (h p' ⊗ₜ[R] q))

Tactic:
rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]

Premises used: TensorProduct.sub_tmul, TensorProduct.add_tmul
-- 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 (N ⊗[R] Q)) (range (rTensor Q f)) ((h (p + p') - (h p + h p')) ⊗ₜ[R] q)

Tactic:
apply le_comap_range_rTensor f

Premises used: le_comap_range_rTensor
-- 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 (N ⊗[R] Q)) (range (rTensor Q f))
    (h (r • p) ⊗ₜ[R] q - HSMul.hSMul (β := N ⊗[R] Q) r (h p ⊗ₜ[R] q))
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f))
    (HSub.hSub (α := N ⊗[R] Q) (β := N ⊗[R] Q)
      ((((TensorProduct.mk R N Q : (a : N) → Q →ₗ[R] N ⊗[R] Q) (h (r • p)) : Q →ₗ[R] N ⊗[R] Q) : (a : Q) → N ⊗[R] Q) q :
        N ⊗[R] Q)
      ((fun (x : N ⊗[R] Q) ↦ HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
          ((((TensorProduct.mk R N Q : (a : N) → Q →ₗ[R] N ⊗[R] Q) (h p) : Q →ₗ[R] N ⊗[R] Q) : (a : Q) → N ⊗[R] Q) q) :
        N ⊗[R] Q))

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

Premises used: LinearMap.range, HSMul.hSMul, LinearMap.rTensor
-- 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 (N ⊗[R] Q)) (range (rTensor Q f)) ((h (r • p) - r • h p) ⊗ₜ[R] q)
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f))
    (h (r • p) ⊗ₜ[R] q - HSMul.hSMul (β := N ⊗[R] Q) r (h p ⊗ₜ[R] q))

Tactic:
rw [TensorProduct.smul_tmul', ← TensorProduct.sub_tmul]

Premises used: TensorProduct.sub_tmul, TensorProduct.smul_tmul'
-- 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
a : h (r • p) - r • h p ∈ f.range
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h (r • p) - r • h p) ⊗ₜ[R] q)

Tactic:
apply le_comap_range_rTensor f

Premises used: le_comap_range_rTensor
-- 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 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
simp :
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh : (a : P ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk y : HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))

Tactic:
simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]

Premises used: LinearMap.comp_apply, Submodule.mkQ_apply
-- 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 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
rw :
  ∀ (hfg_1 : g.ker = f.range) {h : P → N} (hgh : RightInverse h (⇑g : (a : N) → P)) (y : N ⊗[R] Q),
    Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
      ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
        HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
      ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
        HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))

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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
h₁ :
  Eq (α := N ⊗[R] Q →ₗ[R] HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))

Tactic:
apply LinearMap.congr_fun

Premises used: LinearMap.congr_fun
-- 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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
h₁ :
  ∀ (x : N) (y : Q),
    Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
      ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
          (x ⊗ₜ[R] y) :
        HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
      ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) (x ⊗ₜ[R] y) :
        HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
⊢ Eq (α := N ⊗[R] Q →ₗ[R] HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- 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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
n : N
q : Q
this :
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk (h ((g : (a : N) → P) n) ⊗ₜ[R] q)) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))

Tactic:
simpa
-- 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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
n : N
q : Q
h₁ :
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk (h ((g : (a : N) → P) n) ⊗ₜ[R] q)) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))

Tactic:
suffices Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by simpa
-- 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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
n : N
q : Q
h₁ : Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h ((g : (a : N) → P) n) - n) ⊗ₜ[R] q)
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk (h ((g : (a : N) → P) n) ⊗ₜ[R] q)) (Submodule.Quotient.mk (n ⊗ₜ[R] q))

Tactic:
rw [Submodule.Quotient.eq, ← TensorProduct.sub_tmul]

Premises used: Submodule.Quotient.eq, TensorProduct.sub_tmul