-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- If `f` is surjective, then the kernel of `f ⊗ (id B)` is generated by the kernel of `f` -/
lemma Algebra.TensorProduct.rTensor_ker (hf : Function.Surjective f) :
    RingHom.ker (map f (AlgHom.id R C)) =
      (RingHom.ker f).map (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] C)

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ LinearMap.range (LinearMap.rTensor C (LinearMap.ker f.toLinearMap).subtype) =
    LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
⊢ Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))

Tactic:
have : (RingHom.ker (map f (AlgHom.id R C))).restrictScalars R =
  LinearMap.ker (LinearMap.rTensor C (AlgHom.toLinearMap f)) := rfl

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
⊢ RingHom.ker (map f (AlgHom.id R C)) = Ideal.map includeLeft (RingHom.ker f)

Tactic:
rw [← Submodule.restrictScalars_inj R]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
⊢ Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))

Tactic:
rw [this, Ideal.map_includeLeft_eq]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ LinearMap.ker (LinearMap.rTensor C f.toLinearMap) =
    LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ LinearMap.ker (LinearMap.rTensor C f.toLinearMap) =
    LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)

Tactic:
rw [(rTensor_exact C f.toLinearMap.exact_subtype_ker_map hf).linearMap_ker_eq]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
B : Type u_6
C : Type u_7
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Ring C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)
⊢ LinearMap.range (LinearMap.rTensor C (LinearMap.ker f.toLinearMap).subtype) =
    LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)