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_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₁ : h ((g : (a : N) → P) n) - n ∈ f.range
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h ((g : (a : N) → P) n) - n) ⊗ₜ[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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
n : N
q : Q
h₁ : h ((g : (a : N) → P) n) - n ∈ g.ker
h₂ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) n) - n) : P) (0 : P)
h₃ : HSub.hSub (α := P) (β := P) ((g : (a : N) → P) (h ((g : (a : N) → P) n)) : P) ((g : (a : N) → P) n : P) = 0
h₄ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) n)) : P) ((g : (a : N) → P) n : P)
h₅ h₆ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) n : P) ((g : (a : N) → P) n : P)
⊢ h ((g : (a : N) → P) n) - n ∈ f.range

Tactic:
rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]

Premises used: map_sub, sub_eq_zero, 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 : 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)
rw :
  ∀ (x : 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) x :
        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 :
        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 hgh ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))

Tactic:
rw [LinearMap.ext_iff]

Premises used: LinearMap.ext_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)
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)))

Tactic:
simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply,
    rTensor.inverse_of_rightInverse_apply]

Premises used: rTensor.inverse_of_rightInverse_apply, Submodule.mkQ_apply, LinearMap.coe_comp, Function.comp_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)
y : N ⊗[R] Q
rw :
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg ⋯ : (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)))
rw₁ rw₂ :
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk y) (Submodule.Quotient.mk y)
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse Q hfg hg : (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:
rw [rTensor.inverse, rTensor.inverse_of_rightInverse_apply]

Premises used: rTensor.inverse, rTensor.inverse_of_rightInverse_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 (α := N ⊗[R] Q →ₗ[R] HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (inverse_of_rightInverse Q hfg ⋯ ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))
rw₁ rw₂ :
  Eq (α := N ⊗[R] Q →ₗ[R] HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.mkQ (range (rTensor Q f))) (Submodule.mkQ (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 Q hfg hg ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))

Tactic:
rw [rTensor.inverse, rTensor.inverse_of_rightInverse_comp_rTensor]

Premises used: rTensor.inverse, rTensor.inverse_of_rightInverse_comp_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)
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 : HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f))
obtain :
  ∀ (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 : (a : P ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
          ((Submodule.liftQ (range (rTensor Q f)) (rTensor Q g) ⋯ : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q)
            ((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)))
      ((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)))
⊢ (inverse_of_rightInverse Q hfg hgh : (a : P ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
      ((Submodule.liftQ (range (rTensor Q f)) (rTensor Q g) ⋯ : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q) y) =
    y

Tactic:
obtain ⟨y, rfl⟩ := Submodule.mkQ_surjective _ y

Premises used: Submodule.mkQ_surjective, rfl
-- 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 : 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 : (a : P ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        ((Submodule.liftQ (range (rTensor Q f)) (rTensor Q g) ⋯ : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q)
          ((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)))
    ((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:
simp only [Submodule.mkQ_apply, Submodule.liftQ_apply, rTensor.inverse_of_rightInverse_apply]

Premises used: rTensor.inverse_of_rightInverse_apply, Submodule.mkQ_apply, 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)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
z : P ⊗[R] Q
obtain :
  ∀ (y : N ⊗[R] Q),
    Eq (α := P ⊗[R] Q)
      ((toFun Q hfg : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q)
          ((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)) :
        P ⊗[R] Q)
      ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)
⊢ (toFun Q hfg : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q)
      ((inverse_of_rightInverse Q hfg hgh : (a : P ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) z) =
    z

Tactic:
obtain ⟨y, rfl⟩ := rTensor_surjective Q hgh.surjective z

Premises used: LinearMap.rTensor_surjective, Function.RightInverse.surjective, rfl
-- 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 : N ⊗[R] Q
rw :
  Eq (α := P ⊗[R] Q)
    ((toFun Q hfg : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q) (Submodule.Quotient.mk y) : P ⊗[R] Q)
    ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)
⊢ Eq (α := P ⊗[R] Q)
    ((toFun Q hfg : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q)
        ((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)) :
      P ⊗[R] Q)
    ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)

Tactic:
rw [rTensor.inverse_of_rightInverse_apply]

Premises used: rTensor.inverse_of_rightInverse_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)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
⊢ Eq (α := P ⊗[R] Q)
    ((toFun Q hfg : (a : N ⊗[R] Q ⧸ (rTensor Q f).range) → P ⊗[R] Q) (Submodule.Quotient.mk y) : P ⊗[R] Q)
    ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)

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

Premises used: Submodule.liftQ_apply, rTensor.toFun
-- 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 :
  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)
⊢ Exact (M := M ⊗[R] Q) (N := N ⊗[R] Q) (P := P ⊗[R] Q) (⇑(rTensor Q f) : (a : M ⊗[R] Q) → N ⊗[R] Q)
    (⇑(rTensor Q g) : (a : N ⊗[R] Q) → P ⊗[R] Q)

Tactic:
rw [rTensor_exact_iff_lTensor_exact]

Premises used: LinearMap.rTensor_exact_iff_lTensor_exact
-- 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)
⊢ 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:
lTensor_exact Q hfg hg

Premises used: lTensor_exact
-- 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)
⊢ 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:
exact lTensor_exact Q hfg hg

Premises used: lTensor_exact
-- 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_2, u_5} R (↥N) Q) (N := M ⊗[R] Q) (P := TensorProduct.{u_1, u_2, u_5} R (M ⧸ N) Q)
    (⇑(rTensor Q N.subtype) : (a : ↥N ⊗[R] Q) → M ⊗[R] Q) (⇑(rTensor Q N.mkQ) : (a : M ⊗[R] Q) → (M ⧸ N) ⊗[R] Q)
⊢ Eq (α := Submodule R (M ⊗[R] Q)) (ker (M₂ := TensorProduct.{u_1, u_2, u_5} R (M ⧸ N) Q) (rTensor Q N.mkQ))
    (range (rTensor 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_2, u_5} R (↥N) Q) (N := M ⊗[R] Q) (P := TensorProduct.{u_1, u_2, u_5} R (M ⧸ N) Q)
    (⇑(rTensor Q N.subtype) : (a : ↥N ⊗[R] Q) → M ⊗[R] Q) (⇑(rTensor Q N.mkQ) : (a : M ⊗[R] Q) → (M ⧸ N) ⊗[R] Q)

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

Premises used: LinearMap.exact_subtype_mkQ, rTensor_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_2, u_5} R (↥N) Q) (N := M ⊗[R] Q) (P := TensorProduct.{u_1, u_2, u_5} R (M ⧸ N) Q)
    (⇑(rTensor Q N.subtype) : (a : ↥N ⊗[R] Q) → M ⊗[R] Q) (⇑(rTensor Q N.mkQ) : (a : M ⊗[R] Q) → (M ⧸ N) ⊗[R] Q)

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

Premises used: LinearMap.exact_subtype_mkQ, rTensor_exact, Submodule.mkQ_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
a :
  comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)
      (ker (R₂ := R) (M₂ := (R ⧸ I) ⊗[R] Q) (τ₁₂ := RingHom.id R)
        ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1)) =
    comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
⊢ ker (R₂ := R) (M₂ := (R ⧸ I) ⊗[R] Q) (τ₁₂ := RingHom.id R)
      ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1) =
    HSMul.hSMul (β := Submodule R Q) I ⊤

Tactic:
apply comap_injective_of_surjective (TensorProduct.lid R Q).surjective

Premises used: LinearEquiv.surjective, Submodule.comap_injective_of_surjective, TensorProduct.lid
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
a :
  ker (M₂ := (R ⧸ I) ⊗[R] Q)
      ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
        (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)) =
    comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
⊢ comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)
      (ker (R₂ := R) (M₂ := (R ⧸ I) ⊗[R] Q) (τ₁₂ := RingHom.id R)
        ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1)) =
    comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)

Tactic:
rw [← ker_comp]

Premises used: LinearMap.ker_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
⊢ Eq (α := Submodule R (R ⊗[R] Q)) (ker (M₂ := (R ⧸ I) ⊗[R] Q) (rTensor Q (mkQ I)))
    (range (rTensor Q (Submodule.subtype I)))

Tactic:
rTensor_mkQ Q I

Premises used: rTensor_mkQ
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
h :
  Eq (α := R ⊗[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
    ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
      (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q))
    (rTensor Q (mkQ I))
h₁ :
  comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))
⊢ ker (M₂ := (R ⧸ I) ⊗[R] Q)
      ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
        (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)) =
    comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)

Tactic:
convert! rTensor_mkQ Q I

Premises used: rTensor_mkQ
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
h :
  ∀ (x : Q),
    Eq (α := (R ⧸ I) ⊗[R] Q)
      ((((AlgebraTensorModule.curry
                    ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
                      (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)) :
                  R →ₗ[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q) :
                (a : R) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
              1 :
            (a : Q) → (R ⧸ I) ⊗[R] Q)
          x :
        (R ⧸ I) ⊗[R] Q)
      ((((AlgebraTensorModule.curry (rTensor Q (mkQ I)) : R →ₗ[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q) :
                (a : R) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
              1 :
            (a : Q) → (R ⧸ I) ⊗[R] Q)
          x :
        (R ⧸ I) ⊗[R] Q)
⊢ Eq (α := R ⊗[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
    ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
      (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q))
    (rTensor Q (mkQ I))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
x : Q
⊢ Eq (α := (R ⧸ I) ⊗[R] Q)
    ((((AlgebraTensorModule.curry
                  ((TensorProduct.mk R (R ⧸ I) Q : (a : R ⧸ I) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q) 1 ∘ₗ
                    (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q)) :
                R →ₗ[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q) :
              (a : R) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
            1 :
          (a : Q) → (R ⧸ I) ⊗[R] Q)
        x :
      (R ⧸ I) ⊗[R] Q)
    ((((AlgebraTensorModule.curry (rTensor Q (mkQ I)) : R →ₗ[R] Q →ₗ[R] (R ⧸ I) ⊗[R] Q) :
              (a : R) → Q →ₗ[R] (R ⧸ I) ⊗[R] Q)
            1 :
          (a : Q) → (R ⧸ I) ⊗[R] Q)
        x :
      (R ⧸ I) ⊗[R] Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
h :
  Submodule.map (↑(LinearEquiv.symm (TensorProduct.lid R Q)) : Q →ₗ[R] R ⊗[R] Q)
      (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))
h₁ :
  Submodule.map (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (range (rTensor Q (Submodule.subtype I))) =
    HSMul.hSMul (β := Submodule R Q) I ⊤
h₂ h₃ : HSMul.hSMul (β := Submodule R Q) I ⊤ = HSMul.hSMul (β := Submodule R Q) I ⊤
⊢ comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))

Tactic:
rw [comap_equiv_eq_map_symm, map_symm_eq_iff, map_range_rTensor_subtype_lid]

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.map_symm_eq_iff, Submodule.map_range_rTensor_subtype_lid