-- 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:
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

Tactic:
apply Ideal.mul_mem_left

Result:
case a
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
⊢ 1 ⊗ₜ[R] ↑b ∈ map includeRight I

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
⊢ (Submodule.restrictScalars R (map includeRight I)).carrier =
    (LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier

Tactic:
apply le_antisymm

Result:
case a
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
⊢ (Submodule.restrictScalars R (map includeRight I)).carrier ≤
    (LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier

case a
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
⊢ (LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier ≤
    (Submodule.restrictScalars R (map includeRight I)).carrier

Proof state:
case a
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
⊢ x ∈ map includeRight I → ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
intro hx

Result:
case a
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 ∈ map includeRight I
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Proof state:
case a.refine_1.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)
y : B
hy : y ∈ I
⊢ ∃ y_1, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 = 1 ⊗ₜ[R] y

Tactic:
use 1 ⊗ₜ[R] ⟨y, hy⟩

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)
y : B
hy : y ∈ I
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (1 ⊗ₜ[R] ⟨y, hy⟩) = 1 ⊗ₜ[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] ↑b ∈ (Submodule.restrictScalars R (map includeRight I)).carrier

Tactic:
rw [this]

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 ∈ (Submodule.restrictScalars R (map includeRight I)).carrier

Proof state:
case a.intro.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
a : A
b : ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (a ⊗ₜ[R] b) ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier

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

Result:
case a.intro.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
a : A
b : ↥(Submodule.restrictScalars R I)
⊢ a ⊗ₜ[R] ↑b ∈ (Submodule.restrictScalars R (map includeRight I)).carrier

Proof state:
case a.refine_4.intro.refl.tmul.zero
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
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 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)
a : A
b : B
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0

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)
y : B
hy : y ∈ I
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (1 ⊗ₜ[R] ⟨y, hy⟩) = 1 ⊗ₜ[R] y

Tactic:
rfl

Result:
no goals

Proof state:
case a.refine_1
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] B
⊢ (∃ x_1 ∈ I, 1 ⊗ₜ[R] x_1 = x) → ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case a.refine_1.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)
y : B
hy : y ∈ I
⊢ ∃ y_1, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 = 1 ⊗ₜ[R] y

Proof state:
case a.intro.zero
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
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier

Tactic:
rw [map_zero]

Result:
case a.intro.zero
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
⊢ 0 ∈ (Submodule.restrictScalars R (map includeRight I)).carrier

Proof state:
case a
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
⊢ 1 ⊗ₜ[R] ↑b ∈ map includeRight I

Tactic:
apply Ideal.mem_map_of_mem includeRight

Result:
case a
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
⊢ ↑b ∈ I