awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a :
  ∀ (x x_1 : A) (x_2 x_3 : B),
    Eq (α := A ⊗[R] B)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (AlgebraTensorModule.curry
                                      (LinearMap.mul' R (A ⊗[R] B) ∘ₗ
                                        (↑(tensorTensorTensorComm R A A B B) :
                                          A ⊗[R] A ⊗[R] (B ⊗[R] B) →ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))) :
                                  A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                              x :
                            A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                          (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                        x_1) :
                    B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : B) → B →ₗ[R] A ⊗[R] B)
                x_2 :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_3 :
        A ⊗[R] B)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B))) :
                                  A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                              x :
                            A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                          (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                        x_1) :
                    B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : B) → B →ₗ[R] A ⊗[R] B)
                x_2 :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_3 :
        A ⊗[R] B)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)
    (LinearMap.mul' R (A ⊗[R] B) ∘ₗ
        (↑(tensorTensorTensorComm R A A B B) : A ⊗[R] A ⊗[R] (B ⊗[R] B) →ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
      TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)
    (map (LinearMap.mul' R A) (LinearMap.mul' R B) :
      TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
x x_1 : A
x_2 x_3 : B
⊢ Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (AlgebraTensorModule.curry
                                    (LinearMap.mul' R (A ⊗[R] B) ∘ₗ
                                      (↑(tensorTensorTensorComm R A A B B) :
                                        A ⊗[R] A ⊗[R] (B ⊗[R] B) →ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))) :
                                A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                            x :
                          A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                      x_1) :
                  B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : B) → B →ₗ[R] A ⊗[R] B)
              x_2 :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_3 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B))) :
                                A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                            x :
                          A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                      x_1) :
                  B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : B) → B →ₗ[R] A ⊗[R] B)
              x_2 :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_3 :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
⊢ ∀ (w : A) (x : B) (y : A) (z : B),
    Eq (α := A ⊗[R] B)
      (((mul' R (A ⊗[R] B) : A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → A ⊗[R] B)
          (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) :
        A ⊗[R] B)
      ((map (mul' R A) (mul' R B) ∘ₗ
              (↑(tensorTensorTensorComm R A B A B) : A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₗ[R] A ⊗[R] A ⊗[R] (B ⊗[R] B)) :
            (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → A ⊗[R] B)
          (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) :
        A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
a₁ :
  ∀ (x : A) (x_1 : B),
    Eq (α := A ⊗[R] B)
      (((((AlgebraTensorModule.curry (mulLeft R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                x :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_1 :
        A ⊗[R] B)
      (((((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                x :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_1 :
        A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B) (mulLeft R (A := A ⊗[R] B) (a ⊗ₜ[R] b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (map (mulLeft R a) (mulLeft R b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
x : A
x_1 : B
⊢ Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (mulLeft R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
a₁ :
  ∀ (x : A) (x_1 : B),
    Eq (α := A ⊗[R] B)
      (((((AlgebraTensorModule.curry (mulRight R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                x :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_1 :
        A ⊗[R] B)
      (((((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                x :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          x_1 :
        A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B) (mulRight R (A := A ⊗[R] B) (a ⊗ₜ[R] b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (map (mulRight R a) (mulRight R b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
x : A
x_1 : B
⊢ Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (mulRight R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
x y : A ⊗[R] B
⊢ star (0 * y) = star y * star 0

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
x y : A ⊗[R] B
x_1 : A
x_2 : B
⊢ star (HMul.hMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] x_2) 0) = HMul.hMul (α := A ⊗[R] B) (star 0) (star (x_1 ⊗ₜ[R] x_2))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
x y : A ⊗[R] B
x_1 : A
x_2 : B
x_3 : A
x_4 : B
⊢ star (HMul.hMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] x_2) (x_3 ⊗ₜ[R] x_4)) =
    HMul.hMul (α := A ⊗[R] B) (star (x_3 ⊗ₜ[R] x_4)) (star (x_1 ⊗ₜ[R] x_2))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
x y : A ⊗[R] B
x_1 : A
x_2 : B
x_3 x_4 : A ⊗[R] B
h₁ : star (x_1 ⊗ₜ[R] x_2 * x_3) = star x_3 * star (x_1 ⊗ₜ[R] x_2)
h₂ : star (x_1 ⊗ₜ[R] x_2 * x_4) = star x_4 * star (x_1 ⊗ₜ[R] x_2)
⊢ star (x_1 ⊗ₜ[R] x_2 * (x_3 + x_4)) = star (x_3 + x_4) * star (x_1 ⊗ₜ[R] x_2)

Tactic:
simp [add_mul, mul_add, h₁, h₂]

Premises used: add_mul, mul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
x y x_1 x_2 : A ⊗[R] B
h₁ : star (x_1 * y) = star y * star x_1
h₂ : star (x_2 * y) = star y * star x_2
⊢ star ((x_1 + x_2) * y) = star y * star (x_1 + x_2)

Tactic:
simp [add_mul, mul_add, h₁, h₂]

Premises used: add_mul, mul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
inst_9 : StarRing R
inst_10 : StarRing A
inst_11 : StarRing B
inst_12 : StarModule R A
inst_13 : StarModule R B
⊢ ∀ (r s : A ⊗[R] B), star (r + s) = star r + star s

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
⊢ Eq.{u_7 + 1} (α := B)
    ((LinearMap.liftBaseChange S
            (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : S ⊗[R] A) → B)
        1 :
      B)
    (1 : B)

Tactic:
simp [Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
rw :
  Eq.{u_7 + 1} (α := B)
    ((((LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)
    ((((LinearMap.compl₁₂ (LinearMap.mul S B)
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)
⊢ (LinearMap.liftBaseChange S
          (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : S ⊗[R] A) → B)
      (x * y) =
    HMul.hMul (α := B) (β := B)
      ((LinearMap.liftBaseChange S
              (↑f :
                [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : S ⊗[R] A) → B)
          x :
        B)
      ((LinearMap.liftBaseChange S
              (↑f :
                [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : S ⊗[R] A) → B)
          y :
        B)

Tactic:
rw [← LinearMap.mul_apply_apply S, ← LinearMap.compr₂_apply,
        ← LinearMap.mul_apply_apply S, ← LinearMap.compl₁₂_apply]

Premises used: LinearMap.mul_apply_apply, LinearMap.compr₂_apply, LinearMap.compl₁₂_apply
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
e_a :
  Eq (α := S ⊗[R] A →ₗ[S] S ⊗[R] A →ₗ[S] B)
    (LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
    (LinearMap.compl₁₂ (LinearMap.mul S B)
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
⊢ Eq.{u_7 + 1} (α := B)
    ((((LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)
    ((((LinearMap.compl₁₂ (LinearMap.mul S B)
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)

Tactic:
congr
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
x_1 x_2 : A
⊢ Eq.{u_7 + 1} (α := B)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry
                              (LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))) :
                            S →ₗ[S] A →ₗ[R] S ⊗[R] A →ₗ[S] B) :
                          (a : S) → A →ₗ[R] S ⊗[R] A →ₗ[S] B)
                        1 :
                      (a : A) → S ⊗[R] A →ₗ[S] B)
                    x_1) :
                S →ₗ[S] A →ₗ[R] B) :
              (a : S) → A →ₗ[R] B)
            1 :
          (a : A) → B)
        x_2 :
      B)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry
                              (LinearMap.compl₁₂ (LinearMap.mul S B)
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))) :
                            S →ₗ[S] A →ₗ[R] S ⊗[R] A →ₗ[S] B) :
                          (a : S) → A →ₗ[R] S ⊗[R] A →ₗ[S] B)
                        1 :
                      (a : A) → S ⊗[R] A →ₗ[S] B)
                    x_1) :
                S →ₗ[S] A →ₗ[R] B) :
              (a : S) → A →ₗ[R] B)
            1 :
          (a : A) → B)
        x_2 :
      B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
H :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := B)
      (((fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
              ((fun (f : A →ₐ[R] B) ↦
                  (ofLinearMap
                      (LinearMap.liftBaseChange S
                        (↑f :
                          [inst : FunLike (A →ₐ[R] B) A B] →
                            [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                      ⋯ ⋯ :
                    S ⊗[R] A →ₐ[S] B))
                f) :
            (a : A) → B)
          x :
        B)
      ((f : (a : A) → B) x : B)
⊢ (fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
      ((fun (f : A →ₐ[R] B) ↦
          (ofLinearMap
              (LinearMap.liftBaseChange S
                (↑f :
                  [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
              ⋯ ⋯ :
            S ⊗[R] A →ₐ[S] B))
        f) =
    f

Tactic:
ext