awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
a₁ : Membership.mem (γ := Ideal (A ⊗[R] B)) (map (F := B →ₐ[R] A ⊗[R] B) includeRight I) (1 ⊗ₜ[R] (↑b : B))
⊢ Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B)) (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)
    (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B)))

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
a₁ : (↑b : B) ∈ I
⊢ Membership.mem (γ := Ideal (A ⊗[R] B)) (map (F := B →ₐ[R] A ⊗[R] B) includeRight I) (1 ⊗ₜ[R] (↑b : B))

Tactic:
apply Ideal.mem_map_of_mem includeRight

Premises used: Ideal.mem_map_of_mem, Algebra.TensorProduct.includeRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
⊢ (↑b : B) ∈ I

Tactic:
Submodule.coe_mem b

Premises used: Set.Mem, Submodule.coe_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
⊢ (↑b : B) ∈ I

Tactic:
exact Submodule.coe_mem b

Premises used: Submodule.coe_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
a₁ : a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))
⊢ a ⊗ₜ[R] (↑b : B) ∈ (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))

Tactic:
suffices a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B)) by
          rw [this]
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          apply Ideal.mul_mem_left
          -- Note: adding `includeRight` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeRight
          exact Submodule.coe_mem b
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
⊢ a ⊗ₜ[R] (↑b : B) = HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑b : B))

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

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        x :
      A ⊗[R] B)
hy :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y :
      A ⊗[R] B)
a :
  HAdd.hAdd (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y :
        A ⊗[R] B) ∈
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
⊢ Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        (x + y) :
      A ⊗[R] B)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
x y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
hx :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        x :
      A ⊗[R] B)
hy :
  Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
    ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y :
      A ⊗[R] B)
⊢ HAdd.hAdd (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          x :
        A ⊗[R] B)
      ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y :
        A ⊗[R] B) ∈
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))

Tactic:
apply Submodule.add_mem _ hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Algebra R S
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal B
rw :
  Eq (α := Submodule R (A ⊗[R] B))
    (Submodule.restrictScalars R (R := S)
      (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_2, u_3} R A ↥I) (τ₁₂ := RingHom.id S)
        (((lTensor S A : (↥I →ₗ[R] B) →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥I →ₗ[S] A ⊗[R] B) :
            (a : ↥I →ₗ[R] B) → A ⊗[R] ↥I →ₗ[S] A ⊗[R] B)
          ((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.subtype I)))))
    (Submodule.restrictScalars R (Submodule.restrictScalars S (Ideal.map (F := B →ₐ[R] A ⊗[R] B) includeRight I)))
⊢ Eq (α := Submodule S (A ⊗[R] B))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_2, u_3} R A ↥I) (τ₁₂ := RingHom.id S)
      (((lTensor S A : (↥I →ₗ[R] B) →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥I →ₗ[S] A ⊗[R] B) :
          (a : ↥I →ₗ[R] B) → A ⊗[R] ↥I →ₗ[S] A ⊗[R] B)
        ((↑R :
            {S M M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Submodule.subtype I))))
    (Submodule.restrictScalars S (Ideal.map (F := B →ₐ[R] A ⊗[R] B) includeRight I))

Tactic:
rw [← (Submodule.restrictScalars_injective R _ _).eq_iff]

Premises used: Function.Injective.eq_iff, Submodule.restrictScalars_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Algebra R S
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal B
⊢ Eq (α := Submodule R (A ⊗[R] B))
    (Submodule.restrictScalars R (R := S)
      (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_2, u_3} R A ↥I) (τ₁₂ := RingHom.id S)
        (((lTensor S A : (↥I →ₗ[R] B) →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥I →ₗ[S] A ⊗[R] B) :
            (a : ↥I →ₗ[R] B) → A ⊗[R] ↥I →ₗ[S] A ⊗[R] B)
          ((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.subtype I)))))
    (Submodule.restrictScalars R (Submodule.restrictScalars S (Ideal.map (F := B →ₐ[R] A ⊗[R] B) includeRight I)))

Tactic:
(I.map_includeRight_eq (R := R) (A := A)).symm

Premises used: iInf, Set.Mem, Set.iInter, Submodule.restrictScalars, setOf, Ideal.map_includeRight_eq, LinearMap.range, Ideal.map, Quotient, Submodule.span, TensorProduct, TensorProduct.tmul, Set.range, AddCon.Quotient, Eq.symm, AddCon.toQuotient, Submodule.copy
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Algebra R S
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
I : Ideal B
⊢ Eq (α := Submodule R (A ⊗[R] B))
    (Submodule.restrictScalars R (R := S)
      (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_2, u_3} R A ↥I) (τ₁₂ := RingHom.id S)
        (((lTensor S A : (↥I →ₗ[R] B) →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥I →ₗ[S] A ⊗[R] B) :
            (a : ↥I →ₗ[R] B) → A ⊗[R] ↥I →ₗ[S] A ⊗[R] B)
          ((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.subtype I)))))
    (Submodule.restrictScalars R (Submodule.restrictScalars S (Ideal.map (F := B →ₐ[R] A ⊗[R] B) includeRight I)))

Tactic:
exact (I.map_includeRight_eq (R := R) (A := A)).symm

Premises used: Ideal.map_includeRight_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst_1 : Ring A
inst_2 : Ring C
inst_3 : Ring D
inst_4 : Algebra R A
inst_5 : Algebra R C
inst_6 : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
rw :
  Eq (α := Submodule R (A ⊗[R] C))
    (Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)))
    (Submodule.restrictScalars R (Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g)))
⊢ Eq (α := Ideal (A ⊗[R] C))
    (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D))
    (Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))

Tactic:
rw [← Submodule.restrictScalars_inj R]

Premises used: Submodule.restrictScalars_inj
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst_1 : Ring A
inst_2 : Ring C
inst_3 : Ring D
inst_4 : Algebra R A
inst_5 : Algebra R C
inst_6 : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
⊢ Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)) =
    LinearMap.ker (LinearMap.lTensor A g.toLinearMap)

Tactic:
have : (RingHom.ker (map (AlgHom.id R A) g)).restrictScalars R =
    LinearMap.ker (LinearMap.lTensor A (AlgHom.toLinearMap g)) := rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst_1 : Ring A
inst_2 : Ring C
inst_3 : Ring D
inst_4 : Algebra R A
inst_5 : Algebra R C
inst_6 : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)) =
    LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
rw :
  Eq (α := Submodule R (A ⊗[R] C)) (LinearMap.ker (LinearMap.lTensor A g.toLinearMap))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R A ↥(Submodule.restrictScalars R (RingHom.ker g)))
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker g)))))
⊢ Eq (α := Submodule R (A ⊗[R] C))
    (Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)))
    (Submodule.restrictScalars R (Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g)))

Tactic:
rw [this, Ideal.map_includeRight_eq]

Premises used: Ideal.map_includeRight_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst_1 : Ring A
inst_2 : Ring C
inst_3 : Ring D
inst_4 : Algebra R A
inst_5 : Algebra R C
inst_6 : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)) =
    LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
rw :
  Eq (α := Submodule R (A ⊗[R] C)) (LinearMap.range (LinearMap.lTensor A g.toLinearMap.ker.subtype))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R A ↥(Submodule.restrictScalars R (RingHom.ker g)))
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker g)))))
⊢ Eq (α := Submodule R (A ⊗[R] C)) (LinearMap.ker (LinearMap.lTensor A g.toLinearMap))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R A ↥(Submodule.restrictScalars R (RingHom.ker g)))
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker g)))))

Tactic:
rw [(lTensor_exact A g.toLinearMap.exact_subtype_ker_map hg).linearMap_ker_eq]

Premises used: AlgHom.toLinearMap, Function.Exact.linearMap_ker_eq, lTensor_exact, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst_1 : Ring A
inst_2 : Ring C
inst_3 : Ring D
inst_4 : Algebra R A
inst_5 : Algebra R C
inst_6 : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)) =
    LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ Eq (α := Submodule R (A ⊗[R] C)) (LinearMap.range (LinearMap.lTensor A g.toLinearMap.ker.subtype))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R A ↥(Submodule.restrictScalars R (RingHom.ker g)))
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker g)))))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Algebra R A
inst_7 : Algebra R B
inst_8 : Algebra R C
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
rw :
  Eq (α := Submodule R (A ⊗[R] C))
    (Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)))
    (Submodule.restrictScalars R (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))
⊢ Eq (α := Ideal (A ⊗[R] C))
    (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))

Tactic:
rw [← Submodule.restrictScalars_inj R]

Premises used: Submodule.restrictScalars_inj
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Algebra R A
inst_7 : Algebra R B
inst_8 : Algebra R C
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)) =
    LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f)))

Tactic:
have : (RingHom.ker (map f (AlgHom.id R C))).restrictScalars R =
    LinearMap.ker (LinearMap.rTensor C (f.restrictScalars R).toLinearMap) := rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Algebra R A
inst_7 : Algebra R B
inst_8 : Algebra R C
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)) =
    LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f)))
rw :
  Eq (α := Submodule R (A ⊗[R] C))
    (LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f))))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R (↥(Submodule.restrictScalars R (RingHom.ker f))) C)
      (LinearMap.rTensor C (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker f)))))
⊢ Eq (α := Submodule R (A ⊗[R] C))
    (Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)))
    (Submodule.restrictScalars R (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))

Tactic:
rw [this, Ideal.map_includeLeft_eq]

Premises used: Ideal.map_includeLeft_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Algebra R A
inst_7 : Algebra R B
inst_8 : Algebra R C
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)) =
    LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f)))
rw :
  Eq (α := Submodule R (A ⊗[R] C))
    (LinearMap.range (M :=
      TensorProduct.{u_4, u_6, u_8} R
        (↥(LinearMap.ker.{u_4, u_4, u_6, u_7} (R₂ := R) (M₂ := B) (τ₁₂ := RingHom.id R)
              (AlgHom.toLinearMap (AlgHom.restrictScalars R f)) :
            Submodule R A))
        C)
      (LinearMap.rTensor C
        (Submodule.subtype
          (LinearMap.ker.{u_4, u_4, u_6, u_7} (R₂ := R) (M₂ := B) (τ₁₂ := RingHom.id R)
            (AlgHom.toLinearMap (AlgHom.restrictScalars R f))))))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R (↥(Submodule.restrictScalars R (RingHom.ker f))) C)
      (LinearMap.rTensor C (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker f)))))
⊢ Eq (α := Submodule R (A ⊗[R] C))
    (LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f))))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R (↥(Submodule.restrictScalars R (RingHom.ker f))) C)
      (LinearMap.rTensor C (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker f)))))

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

Premises used: AlgHom.toLinearMap, Function.Exact.linearMap_ker_eq, AlgHom.restrictScalars, rTensor_exact, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Algebra R A
inst_7 : Algebra R B
inst_8 : Algebra R C
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this :
  Submodule.restrictScalars R
      (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] C) (map f (AlgHom.id R C) : A ⊗[R] C →ₐ[S] B ⊗[R] C)) =
    LinearMap.ker (M₂ := B ⊗[R] C) (LinearMap.rTensor C (AlgHom.toLinearMap (AlgHom.restrictScalars R f)))
⊢ Eq (α := Submodule R (A ⊗[R] C))
    (LinearMap.range (M :=
      TensorProduct.{u_4, u_6, u_8} R
        (↥(LinearMap.ker.{u_4, u_4, u_6, u_7} (R₂ := R) (M₂ := B) (τ₁₂ := RingHom.id R)
              (AlgHom.toLinearMap (AlgHom.restrictScalars R f)) :
            Submodule R A))
        C)
      (LinearMap.rTensor C
        (Submodule.subtype
          (LinearMap.ker.{u_4, u_4, u_6, u_7} (R₂ := R) (M₂ := B) (τ₁₂ := RingHom.id R)
            (AlgHom.toLinearMap (AlgHom.restrictScalars R f))))))
    (LinearMap.range (M := TensorProduct.{u_4, u_6, u_8} R (↥(Submodule.restrictScalars R (RingHom.ker f))) C)
      (LinearMap.rTensor C (Submodule.subtype (Submodule.restrictScalars R (RingHom.ker f)))))

Tactic:
rfl