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_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 ((g : (a : N) → P) n) - n ∈ f.range
have h₃ : HSub.hSub (α := P) (β := P) ((g : (a : N) → P) (h ((g : (a : N) → P) n)) : P) ((g : (a : N) → P) n : 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 : 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 ((g : (a : N) → P) n) - n ∈ f.range
have h₄ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) (h ((g : (a : N) → P) n)) : P) ((g : (a : N) → P) n : 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 : 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 ((g : (a : N) → P) n) - n ∈ f.range
have h₅ : Eq.{u_4 + 1} (α := P) ((g : (a : N) → P) n : P) ((g : (a : N) → P) n : 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)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
⊢ 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)))
have 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)))
Tactic: rw [LinearMap.ext_iff]
-- 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 : N ⊗[R] Q
⊢ 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)))
have rw : Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
  ((inverse_of_rightInverse Q hfg sorry : (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]
-- 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 : 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)))
⊢ 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)))
have 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)
Tactic: rw [rTensor.inverse, rTensor.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 (α := 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)))
have 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 sorry ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))
Tactic: rw [rTensor.inverse, rTensor.inverse_of_rightInverse_comp_rTensor]
-- 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 (α := 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)))
⊢ 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)))
have 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)))
Tactic: rw [rTensor.inverse, rTensor.inverse_of_rightInverse_comp_rTensor]
-- 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 (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
have 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) sorry : (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: 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 : 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
have 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)
Tactic: obtain ⟨y, rfl⟩ := rTensor_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 : 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)
have 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)
Tactic: rw [rTensor.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 := 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)
have 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)
Tactic: rw [rTensor_exact_iff_lTensor_exact]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
⊢ 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))
have 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)
Tactic: rw [← exact_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
⊢ 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 ⊤
have 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 ⊤)
Tactic: apply comap_injective_of_surjective (TensorProduct.lid R Q).surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
⊢ 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 ⊤)
have 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 ⊤)
Tactic: rw [← ker_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
⊢ 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 ⊤)
have 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))
Tactic: convert! rTensor_mkQ Q I
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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))
⊢ 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 ⊤)
have h₁ : comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
  range (rTensor Q (Submodule.subtype I))
Tactic: convert! rTensor_mkQ Q I
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 (α := 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommRing R
Q : Type u_5
inst_1 : AddCommGroup Q
inst_2 : Module R Q
I : Ideal R
⊢ comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))
have 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))
Tactic: rw [comap_equiv_eq_map_symm, map_symm_eq_iff, map_range_rTensor_subtype_lid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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))
⊢ comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))
have h₁ : Submodule.map (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (range (rTensor Q (Submodule.subtype I))) =
  HSMul.hSMul (β := Submodule R Q) I ⊤
Tactic: rw [comap_equiv_eq_map_symm, map_symm_eq_iff, map_range_rTensor_subtype_lid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 ⊤
⊢ comap (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (HSMul.hSMul (β := Submodule R Q) I ⊤) =
    range (rTensor Q (Submodule.subtype I))
have h₂ : HSMul.hSMul (β := Submodule R Q) I ⊤ = HSMul.hSMul (β := Submodule R Q) I ⊤
Tactic: rw [comap_equiv_eq_map_symm, map_symm_eq_iff, map_range_rTensor_subtype_lid]
-- 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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
⊢ (map g g').ker = range (lTensor N f') ⊔ range (rTensor N' f)
have rw : (lTensor P g' ∘ₗ rTensor N' g).ker = range (lTensor N f') ⊔ range (rTensor N' f)
Tactic: rw [← lTensor_comp_rTensor]
-- 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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
⊢ (lTensor P g' ∘ₗ rTensor N' g).ker = range (lTensor N f') ⊔ range (rTensor N' f)
have rw : Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ range (rTensor N' f)
Tactic: rw [ker_comp]