-- 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
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
ha :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hb :
  ∃ y,
    (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:
obtain ⟨x', ha'⟩ := ha

Result:
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 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
hb :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
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,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 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
⊢ (Submodule.restrictScalars R (map includeLeft I)).carrier =
    (LinearMap.range (LinearMap.rTensor B (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 A
⊢ (Submodule.restrictScalars R (map includeLeft I)).carrier ≤
    (LinearMap.range (LinearMap.rTensor B (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 A
⊢ (LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier ≤
    (Submodule.restrictScalars R (map includeLeft 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 A
a : ↥(Submodule.restrictScalars R I)
b : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (a ⊗ₜ[R] b) ∈
    (Submodule.restrictScalars R (map includeLeft I)).carrier

Tactic:
simp only [LinearMap.rTensor_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 A
a : ↥(Submodule.restrictScalars R I)
b : B
⊢ ↑a ⊗ₜ[R] b ∈ (Submodule.restrictScalars R (map includeLeft I)).carrier

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

Tactic:
rw [← Submodule.carrier_inj]

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

Tactic:
simp only [Submodule.coe_restrictScalars, Algebra.TensorProduct.tmul_mul_tmul,
  mul_one, one_mul]

Result:
no goals

Proof state:
case a.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
y : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeLeft I)).carrier

Tactic:
induction y with
| zero =>
    rw [map_zero]
    apply zero_mem
| tmul a b =>
    simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]
    suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Submodule.restrictScalars_mem]
      rw [this]
      apply Ideal.mul_mem_left
      apply Ideal.mem_map_of_mem includeLeft
      exact Submodule.coe_mem a
    simp only [Submodule.coe_restrictScalars, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one, one_mul]
| add x y hx hy =>
    rw [map_add]
    apply Submodule.add_mem _ hx hy

Result:
no goals

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