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
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 A
x_1 : A ⊗[R] B
hx_1 :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hx :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
hy :
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)
have a₁ : ∀ (x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
  (hx' :
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        x' =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)),
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)
Tactic: obtain ⟨x', hx'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hy :
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)
x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hx' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      x' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)
have a₁ : ∀ (y' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
  (hy' :
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y' =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)),
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)
Tactic: obtain ⟨y', hy'⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
a : A
b : B
x y x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hx' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      x' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hy' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      y' =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          y :
        A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x + y) :
          A ⊗[R] B)
have h : (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
      (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
    (x' + y') =
  HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
    ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        (x + y) :
      A ⊗[R] B)
Tactic: use x' + y'
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a : A
b : B
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have a₁ : ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      y =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        0)
Tactic: induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a : A
b : B
a₁ :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          0)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have a₂ : ∀ (x : ↥(Submodule.restrictScalars R I)) (y : B),
  ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y_1 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            (x ⊗ₜ[R] y) :
          A ⊗[R] B)
Tactic: induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a b : A ⊗[R] B
ha :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) a
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
hb :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) b
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have a₁ : ∀ (x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
  (ha' :
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        x' =
      HSMul.hSMul (β := A ⊗[R] B) a
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)),
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
Tactic: obtain ⟨x', ha'⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a b : A ⊗[R] B
hb :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) b
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
ha' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      x' =
    HSMul.hSMul (β := A ⊗[R] B) a
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have a₁ : ∀ (y' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
  (hb' :
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y' =
      HSMul.hSMul (β := A ⊗[R] B) b
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)),
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
Tactic: obtain ⟨y', hb'⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a b : A ⊗[R] B
x' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
ha' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      x' =
    HSMul.hSMul (β := A ⊗[R] B) a
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
y' : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hb' :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      y' =
    HSMul.hSMul (β := A ⊗[R] B) b
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) (a + b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have h : (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
      (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
    (x' + y') =
  HSMul.hSMul (β := A ⊗[R] B) (a + b)
    ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        x :
      A ⊗[R] B)
Tactic: use x' + y'
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 A
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
a : A ⊗[R] B
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      HSMul.hSMul (β := A ⊗[R] B) a
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
have a₁ : ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      y =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) 0
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
Tactic: induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']
Cleared hypotheses: a