awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
h : Eq (α := A ⊗[R] B) ((a * x) ⊗ₜ[R] (↑(b • y) : B)) ((a * x) ⊗ₜ[R] (b * (↑y : B)))
⊢ (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      ((a * x) ⊗ₜ[R] (b • y)) =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          (x ⊗ₜ[R] y) :
        A ⊗[R] B)

Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, Submodule.coe_subtype, smul_eq_mul, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ Eq (α := A ⊗[R] B) ((a * x) ⊗ₜ[R] (↑(b • y) : B)) ((a * x) ⊗ₜ[R] (b * (↑y : B)))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx_1 :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)
hy :
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            y :
          A ⊗[R] B)
a₁ :
  ∀ (x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
    (hx' :
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x' =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              x :
            A ⊗[R] B)),
    ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y_1 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              (x + y) :
            A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)

Tactic:
obtain ⟨x', hx'⟩ := hx
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hy :
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            y :
          A ⊗[R] B)
x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
a₁ :
  ∀ (y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
    (hy' :
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y' =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              y :
            A ⊗[R] B)),
    ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y_1 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              (x + y) :
            A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)

Tactic:
obtain ⟨y', hy'⟩ := hy
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hy' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      y' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y :
        A ⊗[R] B)
h :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      (x' + y') =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          (x + y) :
        A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)

Tactic:
use x' + y'
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hy' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      y' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y :
        A ⊗[R] B)
⊢ (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      (x' + y') =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          (x + y) :
        A ⊗[R] B)

Tactic:
simp only [map_add, hx', smul_add, hy']

Premises used: map_add, smul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
ha :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) a
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)
hb :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) b
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)
a₁ :
  ∀ (x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
    (ha' :
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x' =
        HSMul.hSMul (β := A ⊗[R] B) a
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              x :
            A ⊗[R] B)),
    ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y =
        HSMul.hSMul (β := A ⊗[R] B) (a + b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              x :
            A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)

Tactic:
obtain ⟨x', ha'⟩ := ha
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
hb :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) b
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)
x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (β := A ⊗[R] B) a
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
a₁ :
  ∀ (y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
    (hb' :
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y' =
        HSMul.hSMul (β := A ⊗[R] B) b
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              x :
            A ⊗[R] B)),
    ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y =
        HSMul.hSMul (β := A ⊗[R] B) (a + b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              x :
            A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)

Tactic:
obtain ⟨y', hb'⟩ := hb
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (β := A ⊗[R] B) a
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hb' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      y' =
    HSMul.hSMul (β := A ⊗[R] B) b
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
h :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      (x' + y') =
    HSMul.hSMul (β := A ⊗[R] B) (a + b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)

Tactic:
use x' + y'
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
x' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      x' =
    HSMul.hSMul (β := A ⊗[R] B) a
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hb' :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      y' =
    HSMul.hSMul (β := A ⊗[R] B) b
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      (x' + y') =
    HSMul.hSMul (β := A ⊗[R] B) (a + b)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)

Tactic:
simp only [map_add, ha', add_smul, hb']

Premises used: map_add, add_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
⊢ 0 ∈ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))

Tactic:
apply zero_mem

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
a₁ : a ⊗ₜ[R] (↑b : B) ∈ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
⊢ Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        (a ⊗ₜ[R] b) :
      A ⊗[R] B)

Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype]

Premises used: Submodule.coe_subtype, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
rw :
  HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B)) ∈
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
⊢ a ⊗ₜ[R] (↑b : B) ∈ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))

Tactic:
rw [this]