awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : (lTensor P g' ∘ₗ rTensor N' g).ker = range (lTensor N f') ⊔ range (rTensor N' f)
⊢ (map g g').ker = range (lTensor N f') ⊔ range (rTensor N' f)

Tactic:
rw [← lTensor_comp_rTensor]

Premises used: LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ range (rTensor N' f)
⊢ (lTensor P g' ∘ₗ rTensor N' g).ker = range (lTensor N f') ⊔ range (rTensor N' f)

Tactic:
rw [ker_comp]

Premises used: LinearMap.ker_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ ker (rTensor N' g)
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ range (rTensor N' f)

Tactic:
rw [← Exact.linearMap_ker_eq (rTensor_exact N' hfg hg)]

Premises used: Function.Exact.linearMap_ker_eq, rTensor_exact
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw :
  Submodule.comap (rTensor N' g) (ker (lTensor P g')) =
    Submodule.comap (rTensor N' g) (Submodule.map (rTensor N' g) (range (lTensor N f')))
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ ker (rTensor N' g)

Tactic:
rw [← Submodule.comap_map_eq]

Premises used: Submodule.comap_map_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
apply : ker (lTensor P g') = Submodule.map (rTensor N' g) (range (lTensor N f'))
⊢ Submodule.comap (rTensor N' g) (ker (lTensor P g')) =
    Submodule.comap (rTensor N' g) (Submodule.map (rTensor N' g) (range (lTensor N f')))

Tactic:
apply congr_arg₂ _ rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : ker (lTensor P g') = (map g f').range
⊢ ker (lTensor P g') = Submodule.map (rTensor N' g) (range (lTensor N f'))

Tactic:
rw [range_eq_map, ← Submodule.map_comp, rTensor_comp_lTensor,
    Submodule.map_top]

Premises used: LinearMap.rTensor_comp_lTensor, Submodule.map_top, Submodule.map_comp, LinearMap.range_eq_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : ker (lTensor P g') = Submodule.map (lTensor P f') (range (rTensor M' g))
⊢ ker (lTensor P g') = (map g f').range

Tactic:
rw [← lTensor_comp_rTensor, range_eq_map, Submodule.map_comp,
    Submodule.map_top]

Premises used: Submodule.map_top, Submodule.map_comp, LinearMap.lTensor_comp_rTensor, LinearMap.range_eq_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw : Eq (α := Submodule R (P ⊗[R] N')) (ker (lTensor P g')) (range (lTensor P f'))
⊢ ker (lTensor P g') = Submodule.map (lTensor P f') (range (rTensor M' g))

Tactic:
rw [range_eq_top.mpr (rTensor_surjective M' hg), Submodule.map_top]

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top, LinearMap.rTensor_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
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
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)
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup P'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact.{u_6, u_7, u_8} (M := M') (N := N') (P := P') (⇑f' : (a : M') → N') (⇑g' : (a : N') → P')
hg' : Surjective.{u_7 + 1, u_8 + 1} (α := N') (β := P') (⇑g' : (a : N') → P')
rw rw₁ : Eq (α := Submodule R (P ⊗[R] N')) (range (lTensor P f')) (range (lTensor P f'))
⊢ Eq (α := Submodule R (P ⊗[R] N')) (ker (lTensor P g')) (range (lTensor P f'))

Tactic:
rw [Exact.linearMap_ker_eq (lTensor_exact P hfg' hg')]

Premises used: Function.Exact.linearMap_ker_eq, lTensor_exact
-- 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
rw :
  (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B)) =
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
          (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B))
⊢ Eq (α := Submodule R (A ⊗[R] B)) (Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I))
    (LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
      (LinearMap.rTensor B (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 A
a :
  (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B)) ≤
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
          (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B))
a₁ :
  (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
          (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)))) :
      Set (A ⊗[R] B)) ≤
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
⊢ (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B)) =
    (↑(LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
          (LinearMap.rTensor B (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 A
x : A ⊗[R] B
hx : x ∈ (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
⊢ x ∈
    (↑(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))

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

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 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 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)
      (x + y) =
    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)

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

Premises used: map_zero, MulZeroClass.mul_zero, smul_eq_mul