-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- The ideal of `A ⊗[R] B` generated by `I` is the image of `I ⊗[R] B` -/
lemma Ideal.map_includeLeft_eq (I : Ideal A) :
    (I.map (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B)).restrictScalars R
      = LinearMap.range (LinearMap.rTensor B (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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
a : A
b : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 =
    a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0

Tactic:
simp only [map_zero, smul_eq_mul, mul_zero]

Result:
no goals

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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

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

Result:
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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∀ x ∈ ⇑includeLeft '' ↑I, ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = 0

case a.refine_3
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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∀ (x y : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
      y ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
        (∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x) →
          (∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = y) →
            ∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = x + y

case a.refine_4
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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∀ (a x : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
      (∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x) →
        ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = a • x

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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1 ∈ map includeLeft 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ⊗ₜ[R] 1 ∈ map includeLeft I

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 A
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x ∈
    (Submodule.restrictScalars R (map includeLeft I)).carrier
hy :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeLeft I)).carrier
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x +
      (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeLeft I)).carrier

Tactic:
apply Submodule.add_mem _ hx hy

Result:
no goals

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 A
⊢ (Submodule.restrictScalars R (map includeLeft I)).carrier ≤
    (LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier

Tactic:
intro x

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 A
x : A ⊗[R] B
⊢ x ∈ (Submodule.restrictScalars R (map includeLeft I)).carrier →
    x ∈ (LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier

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 A
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y) =
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x +
      (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y

Tactic:
simp only [map_add]

Result:
no goals

Proof state:
case a.refine_4.intro.refl.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 A
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      0 • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

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 A
x✝ : A ⊗[R] B
hx : x✝ ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 =
    0 • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

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 A
x : A ⊗[R] B
hx : x ∈ map includeLeft I
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

Tactic:
rw [Ideal.map, ← submodule_span_eq] at 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 A
x : A ⊗[R] B
hx : x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x