awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          x =
        x →
      (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            y =
          y →
        (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            (x + y) =
          x + y

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      (1 ⊗ₜ[R] 1) =
    x

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
refine_1 :
  Eq (α := A ⊗[R] B)
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) 0 : (a : A ⊗[R] B) → A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B)
    (0 : A ⊗[R] B)
refine_2 :
  ∀ (x : A) (y : B),
    Eq (α := A ⊗[R] B)
      ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x ⊗ₜ[R] y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) :
        A ⊗[R] B)
      (x ⊗ₜ[R] y : A ⊗[R] B)
refine_3 :
  ∀ (x y : A ⊗[R] B),
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) =
        x →
      (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
            (1 ⊗ₜ[R] 1) =
          y →
        (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x + y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            (1 ⊗ₜ[R] 1) =
          x + y
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      (1 ⊗ₜ[R] 1) =
    x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ Eq (α := A ⊗[R] B)
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) 0 : (a : A ⊗[R] B) → A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B)
    (0 : A ⊗[R] B)

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B),
    Eq (α := A ⊗[R] B)
      ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x ⊗ₜ[R] y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) :
        A ⊗[R] B)
      (x ⊗ₜ[R] y : A ⊗[R] B)

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) =
        x →
      (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
            (1 ⊗ₜ[R] 1) =
          y →
        (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x + y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            (1 ⊗ₜ[R] 1) =
          x + y

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x y z : A ⊗[R] B
this :
  Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          mul ∘ₗ
        mul :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.flip
        ((((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                (↑LinearMap.lflip :
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
              (LinearMap.flip mul) ∘ₗ
            mul)) :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
              ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A ⊗[R] B) → A ⊗[R] B)
                y) :
            A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        z :
      A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
        ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          z) :
      A ⊗[R] B)

Tactic:
DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x y z : A ⊗[R] B
this :
  Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          mul ∘ₗ
        mul :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.flip
        ((((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                (↑LinearMap.lflip :
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
              (LinearMap.flip mul) ∘ₗ
            mul)) :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
              ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A ⊗[R] B) → A ⊗[R] B)
                y) :
            A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        z :
      A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
        ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          z) :
      A ⊗[R] B)

Tactic:
exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x y z : A ⊗[R] B
suffices :
  Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          mul ∘ₗ
        mul :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.flip
        ((((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                    (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                (↑LinearMap.lflip :
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
          ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
              (LinearMap.flip mul) ∘ₗ
            mul)) :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
              ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A ⊗[R] B) → A ⊗[R] B)
                y) :
            A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        z :
      A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
        ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          z) :
      A ⊗[R] B)

Tactic:
suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
a : A ⊗[R] B
⊢ 0 * a = 0

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
a : A ⊗[R] B
⊢ a * 0 = 0

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
a b c : A ⊗[R] B
⊢ a * (b + c) = a * b + a * c

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
a b c : A ⊗[R] B
⊢ (a + b) * c = a * c + b * c

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A
b : B
⊢ HPow.hPow (α := A ⊗[R] B) (β := ℕ) (a ⊗ₜ[R] b) 0 = HPow.hPow (β := ℕ) a 0 ⊗ₜ[R] HPow.hPow (β := ℕ) b 0

Tactic:
simp [one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A
b : B
k : ℕ
ih : HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))

Tactic:
simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A
b : B
k : ℕ
zero : HPow.hPow (α := A ⊗[R] B) (β := ℕ) (a ⊗ₜ[R] b) 0 = HPow.hPow (β := ℕ) a 0 ⊗ₜ[R] HPow.hPow (β := ℕ) b 0
succ :
  ∀ (k : ℕ) (ih : HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)),
    HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))
⊢ HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)

Tactic:
induction k with
  | zero => simp [one_def]
  | succ k ih => simp [pow_succ, ih]

Premises used: pow_succ, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
⊢ ∀ (x y : A),
    ZeroHom.toFun
        (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := leftModule) (σ := RingHom.id R)
              ((LinearMap.flip (AlgebraTensorModule.mk R R A B) : (a : B) → A →ₗ[R] A ⊗[R] B) 1)) :
          ZeroHom A (A ⊗[R] B))
        (x * y) =
      HMul.hMul (α := A ⊗[R] B)
        (ZeroHom.toFun
          (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := leftModule) (σ := RingHom.id R)
                ((LinearMap.flip (AlgebraTensorModule.mk R R A B) : (a : B) → A →ₗ[R] A ⊗[R] B) 1)) :
            ZeroHom A (A ⊗[R] B))
          x)
        (ZeroHom.toFun
          (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := leftModule) (σ := RingHom.id R)
                ((LinearMap.flip (AlgebraTensorModule.mk R R A B) : (a : B) → A →ₗ[R] A ⊗[R] B) 1)) :
            ZeroHom A (A ⊗[R] B))
          y)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
rw₃ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = r • (x * 1)
rw₄ : r • (1 * x) = r • (x * 1)
rw₅ : r • (1 * x) = r • x
rw₆ rw₇ : r • x = r • x
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)

Tactic:
rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]

Premises used: smul_mul_assoc, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul', mul_smul_comm, mul_one, one_mul, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
rw₁ : r • x = HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x
rw₂ : r • x = r • (1 ⊗ₜ[R] 1 * x)
rw₃ : r • x = r • (1 * x)
rw₄ rw₅ : r • x = r • x
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x

Tactic:
rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]

Premises used: smul_mul_assoc, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul', one_mul, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
⊢ Eq (α := S →+* A ⊗[R] B) (algebraMap S (A ⊗[R] B)) (RingHom.comp includeLeftRingHom (algebraMap S A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
⊢ Eq.{uB + 1} (α := Algebra ℕ (ℕ ⊗[ℕ] B)) Semiring.toNatAlgebra leftAlgebra

Tactic:
rfl

Premises used: TensorProduct, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
r : S
⊢ Eq (α := A ⊗[R] B) ((algebraMap S (A ⊗[R] B) : (a : S) → A ⊗[R] B) r : A ⊗[R] B)
    ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
r : R
rw :
  Eq (α := A ⊗[R] B) ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
rw₁ :
  Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 : A ⊗[R] B) (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
rw₂ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
rw₃ rw₄ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)

Tactic:
rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
⊢ ∀ (r : S),
    Eq (α := A ⊗[R] B)
      (OneHom.toFun (↑(↑includeLeftRingHom : A →* A ⊗[R] B) : OneHom A (A ⊗[R] B)) ((algebraMap S A : (a : S) → A) r) :
        A ⊗[R] B)
      ((algebraMap S (A ⊗[R] B) : (a : S) → A ⊗[R] B) r : A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
a : A
⊢ Eq (α := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) a : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
⊢ Eq (α := A →ₗ[S] A ⊗[R] B) (AlgHom.toLinearMap includeLeft)
    ((LinearMap.flip (AlgebraTensorModule.mk R S A B) : (a : B) → A →ₗ[S] A ⊗[R] B) 1)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, TensorProduct.tmul, AddCon.toQuotient, rfl