awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
z : P ⊗[R] Q
zero : ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)
tmul :
  ∀ (p : P) (q : Q),
    ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (p ⊗ₜ[R] q : P ⊗[R] Q)
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = z
have add : ∀ (x y : P ⊗[R] Q) (hx : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x)
  (hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y),
  ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x + y
Tactic: induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul p q =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g)) (range (rTensor Q g.range.subtype))
have this : g = g.range.subtype ∘ₗ g.rangeRestrict
Tactic: have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g)) (range (rTensor Q g.range.subtype))
have nth_rewrite : Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
  (range (rTensor Q g.range.subtype))
Tactic: nth_rewrite 1 [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (rTensor Q g.range.subtype))
have rw : Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict))
  (range (rTensor Q g.range.subtype))
Tactic: rw [rTensor_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (P ⊗[R] Q)) (range (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict))
    (range (rTensor Q g.range.subtype))
have hf : Eq (α := Submodule R (TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)) (range (rTensor Q g.rangeRestrict)) ⊤
Tactic: apply range_comp_of_range_eq_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)) (range (rTensor Q g.rangeRestrict)) ⊤
have hf : Function.Surjective (α := N ⊗[R] Q) (β := TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)
  (⇑(rTensor Q g.rangeRestrict) : (a : N ⊗[R] Q) → ↥g.range ⊗[R] Q)
Tactic: rw [range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective (α := N ⊗[R] Q) (β := TensorProduct.{u_1, u_4, u_5} R (↥g.range) Q)
    (⇑(rTensor Q g.rangeRestrict) : (a : N ⊗[R] Q) → ↥g.range ⊗[R] Q)
have hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
Tactic: apply rTensor_surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Eq (α := Q ⊗[R] M →ₗ[R] N ⊗[R] Q) (rTensor Q f ∘ₗ (↑(TensorProduct.comm R Q M) : Q ⊗[R] M →ₗ[R] M ⊗[R] Q))
    ((↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q) ∘ₗ lTensor Q f)
have a : ∀ (x : Q) (x_1 : M),
  Eq (α := N ⊗[R] Q)
    (((((AlgebraTensorModule.curry (rTensor Q f ∘ₗ (↑(TensorProduct.comm R Q M) : Q ⊗[R] M →ₗ[R] M ⊗[R] Q)) :
                  Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                (a : Q) → M →ₗ[R] N ⊗[R] Q)
              x :
            M →ₗ[R] N ⊗[R] Q) :
          (a : M) → N ⊗[R] Q)
        x_1 :
      N ⊗[R] Q)
    (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q) ∘ₗ lTensor Q f) :
                  Q →ₗ[R] M →ₗ[R] N ⊗[R] Q) :
                (a : Q) → M →ₗ[R] N ⊗[R] Q)
              x :
            M →ₗ[R] N ⊗[R] Q) :
          (a : M) → N ⊗[R] Q)
        x_1 :
      N ⊗[R] Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Eq (α := Q ⊗[R] N →ₗ[R] P ⊗[R] Q) (rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q))
    ((↑(TensorProduct.comm R Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ lTensor Q g)
have a : ∀ (x : Q) (x_1 : N),
  Eq (α := P ⊗[R] Q)
    (((((AlgebraTensorModule.curry (rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q)) :
                  Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                (a : Q) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    (((((AlgebraTensorModule.curry ((↑(TensorProduct.comm R Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ lTensor Q g) :
                  Q →ₗ[R] N →ₗ[R] P ⊗[R] Q) :
                (a : Q) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
N' : Type u_6
P' : Type u_7
inst_5 : AddCommMonoid N'
inst_6 : AddCommMonoid P'
inst_7 : Module R N'
inst_8 : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective.{u_6 + 1, u_7 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
⊢ Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P') (⇑(map g g') : (a : N ⊗[R] N') → P ⊗[R] P')
have rw : Function.Surjective (α := N ⊗[R] N') (β := P ⊗[R] P')
  (Function.comp (β := P ⊗[R] N') (⇑(lTensor P g') : (a : P ⊗[R] N') → P ⊗[R] P')
    (⇑(rTensor N' g) : (a : N ⊗[R] N') → P ⊗[R] N'))
Tactic: rw [← lTensor_comp_rTensor, coe_comp]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw₂ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q (g ∘ₗ f))) ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q (g ∘ₗ f))) ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw₃ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (M₂ := Q ⊗[R] P) (lTensor Q 0)) ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (M₂ := Q ⊗[R] P) (lTensor Q 0)) ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw₄ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (R₂ := R) (M₂ := Q ⊗[R] P) (τ₁₂ := RingHom.id R) 0) ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
rw : Eq (α := Submodule R (Q ⊗[R] M)) (Submodule.comap (lTensor Q f) (ker (lTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q g ∘ₗ lTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (lTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (M₂ := Q ⊗[R] P) (lTensor Q 0)) ⊤
rw₄ : Eq (α := Submodule R (Q ⊗[R] M)) (ker (R₂ := R) (M₂ := Q ⊗[R] P) (τ₁₂ := RingHom.id R) 0) ⊤
⊢ LE.le (α := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (ker (lTensor Q g))
have rw₅ : Eq (α := Submodule R (Q ⊗[R] M)) ⊤ ⊤
Tactic: rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (q ⊗ₜ[R] h (p + p') - HAdd.hAdd (α := Q ⊗[R] N) (q ⊗ₜ[R] h p) (q ⊗ₜ[R] h p'))
have rw : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (p + p') - (h p + h p')))
Tactic: rw [← TensorProduct.tmul_add, ← 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (p + p') - (h p + h p')))
have a : h (p + p') - (h p + h p') ∈ f.range
Tactic: apply le_comap_range_lTensor f
-- 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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : P → N
hfg : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hgh : RightInverse h (⇑g : (a : N) → P)
p p' : P
q : Q
⊢ h (p + p') - (h p + h p') ∈ f.range
have a : ∀ (hfg : g.ker = f.range) (hgh : RightInverse h (⇑g : (a : N) → P)) (p p' : P) (q : Q),
  h (p + p') - (h p + h p') ∈ f.range
Tactic: rw [exact_iff] at hfg
Cleared hypotheses: hfg, hgh, p, p', q
-- 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)
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
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (HSub.hSub (α := Q ⊗[R] N) (β := Q ⊗[R] N)
      ((((LinearMap.flip (TensorProduct.mk R Q N) : (a : N) → Q →ₗ[R] Q ⊗[R] N) (h (r • p)) : Q →ₗ[R] Q ⊗[R] N) :
            (a : Q) → Q ⊗[R] N)
          q :
        Q ⊗[R] N)
      ((fun (x : Q ⊗[R] N) ↦ HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
          ((((LinearMap.flip (TensorProduct.mk R Q N) : (a : N) → Q →ₗ[R] Q ⊗[R] N) (h p) : Q →ₗ[R] Q ⊗[R] N) :
              (a : Q) → Q ⊗[R] N)
            q) :
        Q ⊗[R] N))
have change : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
  (q ⊗ₜ[R] h (r • p) - HSMul.hSMul (β := Q ⊗[R] N) r (q ⊗ₜ[R] h p))
Tactic: change q ⊗ₜ[R] (h (r • p)) - r • q ⊗ₜ[R] (h p) ∈ range (lTensor Q f)
-- 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)
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
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f))
    (q ⊗ₜ[R] h (r • p) - HSMul.hSMul (β := Q ⊗[R] N) r (q ⊗ₜ[R] h p))
have rw : Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (r • p) - r • h p))
Tactic: rw [← TensorProduct.tmul_smul, ← 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)
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
⊢ Membership.mem (γ := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)) (q ⊗ₜ[R] (h (r • p) - r • h p))
have a : h (r • p) - r • h p ∈ f.range
Tactic: apply le_comap_range_lTensor f
-- 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)
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
⊢ h (r • p) - r • h p ∈ f.range
have 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
Tactic: rw [exact_iff] at hfg
Cleared hypotheses: hfg, hgh, r, p, q
-- 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 : (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 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)))
Tactic: simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]