awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ Function.Surjective (α := A ⊗[R] C) (β := B ⊗[R] D) (⇑(map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D) : (a : A ⊗[R] C) → B ⊗[R] D)

Tactic:
_root_.TensorProduct.map_surjective (g := f.toLinearMap.restrictScalars R) hf hg

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct, TensorProduct.tmul, AddCon.toQuotient, TensorProduct.map_surjective
-- 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
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 (α := 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
-- 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
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)
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))
⊢ 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))

Tactic:
rw [this]
-- 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
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)
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)))
⊢ 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:
simp only [AlgHom.ker_coe, AlgHom.comp_toRingHom]

Premises used: AlgHom.comp_toRingHom, AlgHom.ker_coe
-- 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
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)
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)))
⊢ 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:
rw [← RingHom.comap_ker]

Premises used: RingHom.comap_ker
-- 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
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)
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))
⊢ 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:
simp only [← AlgHom.ker_coe]

Premises used: AlgHom.ker_coe
-- 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
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)
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 →ₐ[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.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[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 →ₐ[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:
rw [← Algebra.TensorProduct.lTensor_ker _ hg, RingHom.ker_eq_comap_bot (map (AlgHom.id R A) g)]

Premises used: Algebra.TensorProduct.map, AlgHom.id, RingHom.ker_eq_comap_bot, Algebra.TensorProduct.lTensor_ker
-- 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
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)
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 →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
    (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
⊢ 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.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) ⊥)

Tactic:
rw [← Ideal.comap_map_of_surjective (map (AlgHom.id R A) g) (LinearMap.lTensor_surjective A hg)]

Premises used: Algebra.TensorProduct.map, AlgHom.id, LinearMap.lTensor_surjective, Ideal.comap_map_of_surjective
-- 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
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)
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)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f)))
    (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
⊢ 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.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))

Tactic:
rw [Algebra.TensorProduct.rTensor_ker _ hf]

Premises used: Algebra.TensorProduct.rTensor_ker
-- 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
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)
apply :
  Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f))
    (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))
⊢ 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)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f)))
    (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))

Tactic:
apply congr_arg₂ _ rfl

Premises used: rfl, congr_arg₂
-- 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
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)
simp :
  Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
    (Ideal.map (F := A →+* A ⊗[R] D)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] C))
      (RingHom.ker f))
⊢ Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f))
    (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))

Tactic:
simp only [AlgHom.coe_ideal_map, Ideal.map_map]

Premises used: AlgHom.coe_ideal_map, Ideal.map_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
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)
rw :
  Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
    (Ideal.map (F := A →+* A ⊗[R] D) (↑(AlgHom.comp includeLeft (AlgHom.id R A)) : A →+* A ⊗[R] D) (RingHom.ker f))
⊢ Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
    (Ideal.map (F := A →+* A ⊗[R] D)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] C))
      (RingHom.ker f))

Tactic:
rw [← AlgHom.comp_toRingHom, Algebra.TensorProduct.map_comp_includeLeft]

Premises used: AlgHom.comp_toRingHom, Algebra.TensorProduct.map_comp_includeLeft
-- 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
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] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
    (Ideal.map (F := A →+* A ⊗[R] D) (↑(AlgHom.comp includeLeft (AlgHom.id R A)) : A →+* A ⊗[R] D) (RingHom.ker f))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
refine_1 :
  ∀ (a₁ a₂ : ↥⊥) (b₁ b₂ : ↥A),
    ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥⊥ ⊗[R] ↥A) → ↥A)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := ↥A) (β := ↥A)
        (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥⊥ ⊗[R] ↥A) → ↥A)
            (a₁ ⊗ₜ[R] b₁) :
          ↥A)
        (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥⊥ ⊗[R] ↥A) → ↥A)
            (a₂ ⊗ₜ[R] b₂) :
          ↥A)
refine_2 :
  Eq.{u_2 + 1} (α := ↥A)
    (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥⊥ ⊗[R] ↥A) → ↥A)
        (1 ⊗ₜ[R] 1) :
      ↥A)
    (1 : ↥A)
⊢ ↥⊥ ⊗[R] ↥A ≃ₐ[R] ↥A

Tactic:
refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).lTensorOne ?_ ?_

Premises used: Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct