-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- The ideal of `A ⊗[R] B` generated by `I` is the image of `A ⊗[R] I` -/
lemma Ideal.map_includeRight_eq (I : Ideal B) :
    (I.map (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B)).restrictScalars R
      = LinearMap.range (LinearMap.lTensor A (Submodule.subtype (I.restrictScalars R)))

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) ((a * x) ⊗ₜ[R] (b • y)) =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

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

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (a * x) ⊗ₜ[R] ↑(b • y) = (a * x) ⊗ₜ[R] (b * ↑y)

Proof state:
case a.refine_4.intro.refl.add.intro
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
hb :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
x' : A ⊗[R] ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x' =
    a • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
obtain ⟨y', hb'⟩ := hb

Result:
case a.refine_4.intro.refl.add.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
x' : A ⊗[R] ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x' =
    a • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
y' : A ⊗[R] ↥(Submodule.restrictScalars R I)
hb' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y' =
    b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Proof state:
case a.refine_4.intro.refl.tmul.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ ∃ y_1,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

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

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) ((a * x) ⊗ₜ[R] (b • y)) =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b ∈ (Submodule.restrictScalars R (map includeRight I)).carrier

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
  Submodule.mem_toAddSubmonoid, Submodule.restrictScalars_mem]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b ∈ map includeRight I

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
a : A
b : B
x y x' : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x' =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
y' : A ⊗[R] ↥(Submodule.restrictScalars R I)
hy' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y' =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x' + y') =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y)

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

Result:
no goals

Proof state:
case a.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = 0

Tactic:
use 0

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 = 0

Proof state:
case a.intro.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier
hy :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y) ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier

Tactic:
rw [map_add]

Result:
case a.intro.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier
hy :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x +
      (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier