-- 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)
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y) =
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x +
      (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y

Tactic:
simp only [map_add]

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 B
y : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈
    (Submodule.restrictScalars R (map includeRight I)).carrier

Tactic:
induction y with
| zero =>
    rw [map_zero]
    apply zero_mem
| tmul a b =>
    simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype]
    suffices a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B)) by
      rw [this]
      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Submodule.restrictScalars_mem]
      apply Ideal.mul_mem_left
      apply Ideal.mem_map_of_mem includeRight
      exact Submodule.coe_mem b
    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
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 ⊗[R] B
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.lTensor A (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]
    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 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)
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
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x' + y') =
    (a + b) • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
simp only [map_add, ha', add_smul, hb']

Result:
no goals

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

Tactic:
apply zero_mem

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

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

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 ∈ ⇑includeRight '' ↑I, ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
intro x

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