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

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

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
x : ↥(Submodule.restrictScalars R I)
y : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) ((a • x) ⊗ₜ[R] (b * y)) =
    a ⊗ₜ[R] b * (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Tactic:
rfl

Result:
no goals

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 + y) ∈
    (Submodule.restrictScalars R (map includeLeft 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 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

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

Proof state:
case a.refine_4.intro.refl
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 ⊗[R] B
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
induction a with
| zero =>
  use 0
  simp only [map_zero, smul_eq_mul, zero_mul]
| tmul a b =>
  induction x with
  | zero =>
    use 0
    simp only [map_zero, smul_eq_mul, mul_zero]
  | tmul x y =>
    use (a • x) ⊗ₜ[R] (b * y)
    simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
    with_unfolding_all rfl
  | add x y hx hy =>
    obtain ⟨x', hx'⟩ := hx
    obtain ⟨y', hy'⟩ := hy
    use x' + y'
    simp only [map_add, hx', smul_add, hy']
| add a b ha hb =>
  obtain ⟨x', ha'⟩ := ha
  obtain ⟨y', hb'⟩ := hb
  use x' + y'
  simp only [map_add, ha', add_smul, hb']

Result:
no goals

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

Tactic:
induction x with
| zero =>
  use 0
  simp only [map_zero, smul_eq_mul, mul_zero]
| tmul x y =>
  use (a • x) ⊗ₜ[R] (b * y)
  simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
  with_unfolding_all rfl
| add x y hx hy =>
  obtain ⟨x', hx'⟩ := hx
  obtain ⟨y', hy'⟩ := hy
  use x' + y'
  simp only [map_add, hx', smul_add, hy']

Result:
no goals

Proof state:
case a.refine_3.intro.refl.intro.refl
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
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x +
        (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y

Tactic:
use x + 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 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