awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a :
  (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
      0 ∈
    (↑(Submodule.restrictScalars R (map (F := B →ₐ[R] A ⊗[R] B) includeRight I)) : Set (A ⊗[R] B))
a₁ :
  ∀ (a : A) (b : ↥(Submodule.restrictScalars R I)),
    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)
          (a ⊗ₜ[R] b) :
        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)
        y :
      A ⊗[R] B)
have a₂ : ∀ (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)),
  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: 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 [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
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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 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))
have 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)))
Tactic: rw [← (Submodule.restrictScalars_injective R _ _).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ 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))
have 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)))
Tactic: rw [← Submodule.restrictScalars_inj R]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (hypothesis)
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)
⊢ 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)))
have 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)
Tactic: have : (RingHom.ker (map (AlgHom.id R A) g)).restrictScalars R =
    LinearMap.ker (LinearMap.lTensor A (AlgHom.toLinearMap g)) := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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))
    (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)))
have 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)))))
Tactic: rw [this, Ideal.map_includeRight_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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.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)))))
have 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)))))
Tactic: rw [(lTensor_exact A g.toLinearMap.exact_subtype_ker_map hg).linearMap_ker_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ 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))
have 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)))
Tactic: rw [← Submodule.restrictScalars_inj R]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (hypothesis)
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)
⊢ 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)))
have 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)))
Tactic: have : (RingHom.ker (map f (AlgHom.id R C))).restrictScalars R =
    LinearMap.ker (LinearMap.rTensor C (f.restrictScalars R).toLinearMap) := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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))
    (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)))
have 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)))))
Tactic: rw [this, Ideal.map_includeLeft_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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.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)))))
have 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)))))
Tactic: rw [(rTensor_exact C (f.restrictScalars R).toLinearMap.exact_subtype_ker_map hf).linearMap_ker_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (hypothesis)
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
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
⊢ Eq (α := Ideal (A ⊗[R] C)) (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
have this : Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
  (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
      (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
    A ⊗[R] C →ₐ[S] B ⊗[R] D)
Tactic: have : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g) := ext rfl rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C)) (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
have rw : Eq (α := Ideal (A ⊗[R] C))
  (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D))
  (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
    Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (RingHom.ker (F := A ⊗[R] C →ₐ[S] B ⊗[R] D)
      (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
          (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
        A ⊗[R] C →ₐ[S] B ⊗[R] D))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
have simp : Eq (α := Ideal (A ⊗[R] C))
  (RingHom.ker (F := A ⊗[R] C →+* B ⊗[R] D)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D) : A ⊗[R] D →+* B ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)))
  (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker (F := A →+* B) (↑f : A →+* B)) ⊔
    Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker (F := C →+* D) (↑g : C →+* D)))
Tactic: simp only [AlgHom.ker_coe, AlgHom.comp_toRingHom]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (RingHom.ker (F := A ⊗[R] C →+* B ⊗[R] D)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D) : A ⊗[R] D →+* B ⊗[R] D)
        (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker (F := A →+* B) (↑f : A →+* B)) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker (F := C →+* D) (↑g : C →+* D)))
have rw : Eq (α := Ideal (A ⊗[R] C))
  (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D) (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
    (RingHom.ker (F := A ⊗[R] D →+* B ⊗[R] D)
      (↑(map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D) : A ⊗[R] D →+* B ⊗[R] D)))
  (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker (F := A →+* B) (↑f : A →+* B)) ⊔
    Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker (F := C →+* D) (↑g : C →+* D)))
Tactic: rw [← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
      (RingHom.ker (F := A ⊗[R] D →+* B ⊗[R] D)
        (↑(map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D) : A ⊗[R] D →+* B ⊗[R] D)))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker (F := A →+* B) (↑f : A →+* B)) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker (F := C →+* D) (↑g : C →+* D)))
have simp : Eq (α := Ideal (A ⊗[R] C))
  (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D) (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
    (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
  (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
    Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
Tactic: simp only [← AlgHom.ker_coe]