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)
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (ker (lTensor.inverse Q hfg hg)) ⊥
have a : Injective (α := Q ⊗[R] P) (β := HasQuotient.Quotient (Q ⊗[R] N) (B := Submodule R (Q ⊗[R] N)) (range (lTensor Q f)))
  (⇑(lTensor.inverse Q hfg hg) : (a : Q ⊗[R] P) → Q ⊗[R] N ⧸ (lTensor Q f).range)
Tactic: rw [LinearMap.ker_eq_bot]
-- 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 (Q ⊗[R] M)) (ker (M₂ := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N)) (lTensor Q N.mkQ))
    (range (lTensor Q N.subtype))
have rw : Exact (M := TensorProduct.{u_1, u_5, u_2} R Q ↥N) (N := Q ⊗[R] M) (P := TensorProduct.{u_1, u_5, u_2} R Q (M ⧸ N))
  (⇑(lTensor Q N.subtype) : (a : Q ⊗[R] ↥N) → Q ⊗[R] M) (⇑(lTensor Q N.mkQ) : (a : Q ⊗[R] M) → Q ⊗[R] (M ⧸ N))
Tactic: rw [← exact_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_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 (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw : Eq (α := Submodule R (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw₂ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q (g ∘ₗ f))) ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q (g ∘ₗ f))) ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw₃ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (M₂ := P ⊗[R] Q) (rTensor Q 0)) ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (M₂ := P ⊗[R] Q) (rTensor Q 0)) ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw₄ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (R₂ := R) (M₂ := P ⊗[R] Q) (τ₁₂ := RingHom.id R) 0) ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (M ⊗[R] Q)) (Submodule.comap (rTensor Q f) (ker (rTensor Q g))) ⊤
rw₁ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q g ∘ₗ rTensor Q f)) ⊤
rw₂ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (rTensor Q (g ∘ₗ f))) ⊤
rw₃ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (M₂ := P ⊗[R] Q) (rTensor Q 0)) ⊤
rw₄ : Eq (α := Submodule R (M ⊗[R] Q)) (ker (R₂ := R) (M₂ := P ⊗[R] Q) (τ₁₂ := RingHom.id R) 0) ⊤
⊢ LE.le (α := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) (ker (rTensor Q g))
have rw₅ : Eq (α := Submodule R (M ⊗[R] Q)) ⊤ ⊤
Tactic: rw [range_le_iff_comap, ← ker_comp, ← rTensor_comp,
      hfg.linearMap_comp_eq_zero, rTensor_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 (N ⊗[R] Q)) (range (rTensor Q f))
    (h (p + p') ⊗ₜ[R] q - HAdd.hAdd (α := N ⊗[R] Q) (h p ⊗ₜ[R] q) (h p' ⊗ₜ[R] q))
have rw : Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h (p + p') - (h p + h p')) ⊗ₜ[R] q)
Tactic: rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]
-- 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 (N ⊗[R] Q)) (range (rTensor Q f)) ((h (p + p') - (h p + h p')) ⊗ₜ[R] q)
have a : h (p + p') - (h p + h p') ∈ f.range
Tactic: apply le_comap_range_rTensor 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 (N ⊗[R] Q)) (range (rTensor Q f))
    (HSub.hSub (α := N ⊗[R] Q) (β := N ⊗[R] Q)
      ((((TensorProduct.mk R N Q : (a : N) → Q →ₗ[R] N ⊗[R] Q) (h (r • p)) : Q →ₗ[R] N ⊗[R] Q) : (a : Q) → N ⊗[R] Q) q :
        N ⊗[R] Q)
      ((fun (x : N ⊗[R] Q) ↦ HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
          ((((TensorProduct.mk R N Q : (a : N) → Q →ₗ[R] N ⊗[R] Q) (h p) : Q →ₗ[R] N ⊗[R] Q) : (a : Q) → N ⊗[R] Q) q) :
        N ⊗[R] Q))
have change : Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f))
  (h (r • p) ⊗ₜ[R] q - HSMul.hSMul (β := N ⊗[R] Q) r (h p ⊗ₜ[R] q))
Tactic: change h (r • p) ⊗ₜ[R] q - r • h p ⊗ₜ[R] q ∈ range (rTensor 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 (N ⊗[R] Q)) (range (rTensor Q f))
    (h (r • p) ⊗ₜ[R] q - HSMul.hSMul (β := N ⊗[R] Q) r (h p ⊗ₜ[R] q))
have rw : Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h (r • p) - r • h p) ⊗ₜ[R] q)
Tactic: rw [TensorProduct.smul_tmul', ← TensorProduct.sub_tmul]
-- 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 (N ⊗[R] Q)) (range (rTensor Q f)) ((h (r • p) - r • h p) ⊗ₜ[R] q)
have a : h (r • p) - r • h p ∈ f.range
Tactic: apply le_comap_range_rTensor 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 : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh : (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 simp : Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
  ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
    HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
  ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
    HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
Tactic: simp only [← LinearMap.comp_apply, ← Submodule.mkQ_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)
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
have rw : ∀ (hfg_1 : g.ker = f.range) {h : P → N} (hgh : RightInverse h (⇑g : (a : N) → P)) (y : N ⊗[R] Q),
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
Tactic: 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 : N ⊗[R] Q
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((Submodule.mkQ (range (rTensor Q f)) : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range) y :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
have h₁ : 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_1 hgh ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor 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 : N ⊗[R] Q
⊢ 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_1 hgh ∘ₗ rTensor Q g) (Submodule.mkQ (range (rTensor Q f)))
have h₁ : ∀ (x : N) (y : Q),
  Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        (x ⊗ₜ[R] 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) (x ⊗ₜ[R] y) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor 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 : N ⊗[R] Q
n : N
q : Q
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    ((inverse_of_rightInverse Q hfg_1 hgh ∘ₗ rTensor Q g : (a : N ⊗[R] Q) → N ⊗[R] Q ⧸ (rTensor Q f).range)
        (n ⊗ₜ[R] q) :
      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) (n ⊗ₜ[R] q) :
      HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
have h₁ : Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
  (Submodule.Quotient.mk (h ((g : (a : N) → P) n) ⊗ₜ[R] q)) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
Tactic: suffices Submodule.Quotient.mk (h (g n) ⊗ₜ[R] 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 : N ⊗[R] Q
n : N
q : Q
⊢ Eq (α := HasQuotient.Quotient (N ⊗[R] Q) (B := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)))
    (Submodule.Quotient.mk (h ((g : (a : N) → P) n) ⊗ₜ[R] q)) (Submodule.Quotient.mk (n ⊗ₜ[R] q))
have h₁ : Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h ((g : (a : N) → P) n) - n) ⊗ₜ[R] q)
Tactic: rw [Submodule.Quotient.eq, ← TensorProduct.sub_tmul]
-- 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
⊢ Membership.mem (γ := Submodule R (N ⊗[R] Q)) (range (rTensor Q f)) ((h ((g : (a : N) → P) n) - n) ⊗ₜ[R] q)
have h₁ : h ((g : (a : N) → P) n) - n ∈ f.range
Tactic: apply le_comap_range_rTensor 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)
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h (⇑g : (a : N) → P)
y : N ⊗[R] Q
n : N
q : Q
⊢ h ((g : (a : N) → P) n) - n ∈ f.range
have h₁ : h ((g : (a : N) → P) n) - n ∈ 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 : N ⊗[R] Q
n : N
q : Q
h₁ : h ((g : (a : N) → P) n) - n ∈ g.ker
⊢ 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) - n) : P) (0 : P)
Tactic: rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]