awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)))
have 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)))
Tactic: rw [exact_iff] at hfg
Cleared hypotheses: h, hgh, y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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)))
have 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)))
Tactic: apply LinearMap.congr_fun
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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)))
have 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)))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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)))
have 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))
Tactic: suffices Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by
    simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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))
have h₁ : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (n ⊗ₜ[R] (h ((g : (a : N) → P) q) - q))
Tactic: rw [Submodule.Quotient.eq, ← TensorProduct.tmul_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (n ⊗ₜ[R] (h ((g : (a : N) → P) q) - q))
have h₁ : h ((g : (a : N) → P) q) - q ∈ f.range
Tactic: apply le_comap_range_lTensor f n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ((g : (a : N) → P) q) - q ∈ f.range
have h₁ : h ((g : (a : N) → P) q) - q ∈ g.ker
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ((g : (a : N) → P) q) - q ∈ f.range
have h₂ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q) - q) : P) (0 : P)
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ((g : (a : N) → P) q) - q ∈ f.range
have h₃ : HSub.hSub (α := P) (β := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q)) : P) ((g : (a : N) → P) q : P) = 0
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ((g : (a : N) → P) q) - q ∈ f.range
have h₄ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) q)) : P) ((g : (a : N) → P) q : P)
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ((g : (a : N) → P) q) - q ∈ f.range
have h₅ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) q : P) ((g : (a : N) → P) q : P)
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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)))
have rw : Eq (α := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
  ((inverse_of_rightInverse Q hfg sorry : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)))
⊢ 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)))
have 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)
Tactic: rw [lTensor.inverse, lTensor.inverse_of_rightInverse_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ 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)))
have 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 sorry ∘ₗ lTensor Q g) (Submodule.mkQ (range (lTensor Q f)))
Tactic: rw [lTensor.inverse, lTensor.inverse_of_rightInverse_comp_lTensor]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [lTensor.inverse, lTensor.inverse_of_rightInverse_comp_lTensor]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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))
⊢ (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
have 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) sorry : (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: obtain ⟨y, rfl⟩ := Submodule.mkQ_surjective _ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ (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
have 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)
Tactic: obtain ⟨y, rfl⟩ := lTensor_surjective Q (hgh.surjective) z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
        ((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)
have 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)
Tactic: rw [lTensor.inverse_of_rightInverse_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
have rw : Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor Q g)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g))
Tactic: rw [exact_iff, ← Submodule.ker_mkQ (p := range (lTensor Q f)),
    ← lTensor.inverse_comp_lTensor Q hfg hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor Q g)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g))
have a : Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g)) (ker (lTensor Q g))
Tactic: apply symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ Eq (α := Submodule R (Q ⊗[R] N)) (ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g)) (ker (lTensor Q g))
have a : Eq (α := Submodule R (Q ⊗[R] P)) (ker (lTensor.inverse Q hfg hg)) ⊥
Tactic: apply LinearMap.ker_comp_of_ker_eq_bot