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 A
a : ↥(Submodule.restrictScalars R I)
b : B
a₁ : (↑a : A) ⊗ₜ[R] b ∈ (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
⊢ Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
    ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        (a ⊗ₜ[R] b) :
      A ⊗[R] B)

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

Premises used: LinearMap.rTensor_tmul, Submodule.coe_subtype
-- 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
rw :
  Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B)) (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)
    (HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1))
⊢ Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B)) (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I) ((↑a : A) ⊗ₜ[R] b)

Tactic:
rw [this]
-- 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
a₁ : Membership.mem (γ := Ideal (A ⊗[R] B)) (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I) ((↑a : A) ⊗ₜ[R] 1)
⊢ Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B)) (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)
    (HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1))

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
a₁ : (↑a : A) ∈ I
⊢ Membership.mem (γ := Ideal (A ⊗[R] B)) (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I) ((↑a : A) ⊗ₜ[R] 1)

Tactic:
apply Ideal.mem_map_of_mem includeLeft

Premises used: Ideal.mem_map_of_mem, Algebra.TensorProduct.includeLeft
-- 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
⊢ (↑a : A) ∈ I

Tactic:
Submodule.coe_mem a

Premises used: Set.Mem, Submodule.coe_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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
⊢ (↑a : A) ∈ I

Tactic:
exact Submodule.coe_mem a

Premises used: Submodule.coe_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 A
a : ↥(Submodule.restrictScalars R I)
b : B
a₁ : (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)
⊢ (↑a : A) ⊗ₜ[R] b ∈ (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))

Tactic:
suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a
-- 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
⊢ (↑a : A) ⊗ₜ[R] b = HMul.hMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) ((↑a : A) ⊗ₜ[R] 1)

Tactic:
simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- 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 A
x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hx :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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 :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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)
a :
  HAdd.hAdd (α := 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)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          y :
        A ⊗[R] B) ∈
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
⊢ Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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:
rw [map_add]

Premises used: map_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 A
x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
hx :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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 :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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)
⊢ HAdd.hAdd (α := 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)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          y :
        A ⊗[R] B) ∈
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))

Tactic:
apply Submodule.add_mem _ hx hy

Premises used: Submodule.add_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
rw :
  (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B)) =
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
          (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B))
⊢ Eq (α := Submodule R (A ⊗[R] B)) (Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I))
    (LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I))))

Tactic:
rw [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- 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 :
  (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B)) ≤
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
          (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B))
a₁ :
  (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
          (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B)) ≤
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
⊢ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B)) =
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
          (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : A ⊗[R] B
hx : x ∈ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
⊢ x ∈
    (↑(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))

Tactic:
rw [Ideal.map, ← submodule_span_eq] at hx

Premises used: Ideal.submodule_span_eq, Ideal.map
-- 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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))
⊢ ∃ (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 =
      x

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hx

Premises used: Submodule.span_induction
-- 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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))
y : B
hy : y ∈ I
h :
  Eq (α := A ⊗[R] B)
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        (1 ⊗ₜ[R]
          Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submodule R B) (Submodule.restrictScalars R I) x) y hy) :
      A ⊗[R] B)
    (1 ⊗ₜ[R] y : A ⊗[R] B)
⊢ ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    Eq (α := A ⊗[R] B)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y_1 :
        A ⊗[R] B)
      (1 ⊗ₜ[R] y : A ⊗[R] B)

Tactic:
use 1 ⊗ₜ[R] ⟨y, 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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))
y : B
hy : y ∈ I
⊢ Eq (α := A ⊗[R] B)
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        (1 ⊗ₜ[R]
          Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submodule R B) (Submodule.restrictScalars R I) x) y hy) :
      A ⊗[R] B)
    (1 ⊗ₜ[R] y : A ⊗[R] 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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))
h :
  Eq (α := A ⊗[R] B)
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0)
    0
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    Eq (α := 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)
      (0 : A ⊗[R] B)

Tactic:
use 0
-- 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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))
⊢ Eq (α := A ⊗[R] B)
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0)
    0

Tactic:
simp only [map_zero]

Premises used: map_zero
-- 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 y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
h :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      (x + y) =
    HAdd.hAdd (α := 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)
      ((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 =
      HAdd.hAdd (α := 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)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            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))
x 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)
      (x + y) =
    HAdd.hAdd (α := 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)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y :
        A ⊗[R] B)

Tactic:
simp only [map_add]

Premises used: map_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)
h :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0 =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) 0
      ((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 ⊗[R] B) 0
        ((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 0
-- 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)
⊢ (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0 =
    HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) 0
      ((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_zero, smul_eq_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero, smul_eq_mul
-- 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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
h :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0 =
    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)
        0)
⊢ ∃ (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)
          0)

Tactic:
use 0
-- 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 : A ⊗[R] B
hx :
  x ∈
    (↑(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
⊢ (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0 =
    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)
        0)

Tactic:
simp only [map_zero, smul_eq_mul, mul_zero]

Premises used: map_zero, MulZeroClass.mul_zero, smul_eq_mul
-- 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 :
  (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)
⊢ ∃ (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 ⊗ₜ[R] y) :
          A ⊗[R] B)

Tactic:
use (a * x) ⊗ₜ[R] (b • y)

Premises used: HMul.hMul, HSMul.hSMul