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)
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 (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (r • p) - r • 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)
r : R
p : P
q : Q
a :
  ∀ (hfg : g.ker = f.range) (hgh : RightInverse h (⇑g : (a : N) → P)) (r : R) (p : P) (q : Q),
    h (r • p) - r • h p ∈ f.range
⊢ h (r • p) - r • 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)
r : R
p : P
q : Q
⊢ h (r • p) - r • h p ∈ f.range

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

Premises used: map_sub, sub_self, LinearMap.mem_ker, map_smul
-- 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 : Q ⊗[R] N
simp :
  Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
        ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk y : HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor 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 : Q ⊗[R] N
rw :
  ∀ (hfg_1 : g.ker = f.range) {h : P → N} (hgh : RightInverse h (⇑g : (a : N) → P)) (y : Q ⊗[R] N),
    Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
      ((inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
        HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
      ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
        HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor 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 : Q ⊗[R] N
h₁ :
  Eq (α := Q ⊗[R] N →ₗ[R] HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g) (Submodule.mkQ (range (lTensor Q f)))
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor 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 : Q ⊗[R] N
h₁ :
  ∀ (x : Q) (y : N),
    Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
      ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range)
          (x ⊗ₜ[R] y) :
        HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
      ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) (x ⊗ₜ[R] y) :
        HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
⊢ Eq (α := Q ⊗[R] N →ₗ[R] HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g) (Submodule.mkQ (range (lTensor 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 : Q ⊗[R] N
n : Q
q : N
this :
  Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk (n ⊗ₜ[R] h ((g : (a : N) → P) q))) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range)
        (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor 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 : Q ⊗[R] N
n : Q
q : N
h₁ :
  Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk (n ⊗ₜ[R] h ((g : (a : N) → P) q))) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range)
        (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))

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

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

Premises used: Submodule.Quotient.eq, TensorProduct.tmul_sub
-- 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 : Q ⊗[R] N
n : Q
q : N
h₁ : h ((g : (a : N) → P) q) - q ∈ f.range
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (n ⊗ₜ[R] (h ((g : (a : N) → P) q) - q))

Tactic:
apply le_comap_range_lTensor f n

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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : Q ⊗[R] N
n : Q
q : N
h₁ : h ((g : (a : N) → P) q) - q ∈ g.ker
h₂ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q) - q) : P) (0 : P)
h₃ : HSub.hSub (α := P) (β := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q)) : P) ((g : (a : N) → P) q : P) = 0
h₄ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q)) : P) ((g : (a : N) → P) q : P)
h₅ h₆ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) q : P) ((g : (a : N) → P) q : P)
⊢ h ((g : (a : N) → P) q) - q ∈ 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)
y : Q ⊗[R] N
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((Submodule.mkQ (range (lTensor Q f)) : (a : Q ⊗[R] N) → Q ⊗[R] N ⧸ (lTensor Q f).range) y :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))

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

Premises used: lTensor.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 : Q ⊗[R] N
rw :
  Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse_of_rightInverse Q hfg ⋯ : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
        ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk y : HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
rw₁ rw₂ :
  Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk y) (Submodule.Quotient.mk y)
⊢ Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    ((inverse Q hfg hg : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
        ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y) :
      HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
    (Submodule.Quotient.mk y : HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))

Tactic:
rw [lTensor.inverse, lTensor.inverse_of_rightInverse_apply]

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

Tactic:
rw [lTensor.inverse, lTensor.inverse_of_rightInverse_comp_lTensor]

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

Tactic:
simp only [Submodule.mkQ_apply, Submodule.liftQ_apply, lTensor.inverse_of_rightInverse_apply]

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

Tactic:
obtain ⟨y, rfl⟩ := lTensor_surjective Q (hgh.surjective) z

Premises used: LinearMap.lTensor_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 : Q ⊗[R] N
rw :
  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)
⊢ Eq (α := Q ⊗[R] P)
    ((toFun Q hfg : (a : Q ⊗[R] N ⧸ (lTensor Q f).range) → Q ⊗[R] P)
        ((inverse_of_rightInverse Q hfg hgh : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
          ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y)) :
      Q ⊗[R] P)
    ((lTensor Q g : (a : Q ⊗[R] N) → Q ⊗[R] P) y : Q ⊗[R] P)

Tactic:
rw [lTensor.inverse_of_rightInverse_apply]

Premises used: lTensor.inverse_of_rightInverse_apply