awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (x y : B),
    ZeroHom.toFun
        (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := instModule) (σ := RingHom.id R)
              ((AlgebraTensorModule.mk R R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
          ZeroHom B (A ⊗[R] B))
        (x * y) =
      HMul.hMul (α := A ⊗[R] B)
        (ZeroHom.toFun
          (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := instModule) (σ := RingHom.id R)
                ((AlgebraTensorModule.mk R R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
            ZeroHom B (A ⊗[R] B))
          x)
        (ZeroHom.toFun
          (↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := instModule) (σ := RingHom.id R)
                ((AlgebraTensorModule.mk R R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
            ZeroHom B (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
r : R
⊢ Eq (α := A ⊗[R] B)
    (ZeroHom.toFun (M := B)
        ((↑(LinearMap.toAddMonoidHom (R := R) (S := R) (modM₁ := toModule) (modM₂ := instModule) (σ := RingHom.id R)
                ((AlgebraTensorModule.mk R R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
            ZeroHom B (A ⊗[R] B)) :
          ZeroHom B (A ⊗[R] B))
        ((algebraMap R B : (a : R) → B) r : B) :
      A ⊗[R] B)
    ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)

Tactic:
simp [algebraMap_eq_smul_one', smul_tmul]

Premises used: Algebra.algebraMap_eq_smul_one', TensorProduct.smul_tmul
-- 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
b : B
⊢ Eq (α := A ⊗[R] B) ((includeRight : (a : B) → A ⊗[R] B) b : A ⊗[R] B) (1 ⊗ₜ[R] b : 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
⊢ Eq (α := B →ₗ[R] A ⊗[R] B) (AlgHom.toLinearMap includeRight)
    ((AlgebraTensorModule.mk R R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, 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
a :
  ∀ (x : R),
    Eq (α := A ⊗[R] B) ((RingHom.comp includeLeftRingHom (algebraMap R A) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)
      ((RingHom.comp (AlgHom.toRingHom includeRight) (algebraMap R B) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)
⊢ Eq (α := R →+* A ⊗[R] B) (RingHom.comp includeLeftRingHom (algebraMap R A))
    (RingHom.comp (AlgHom.toRingHom includeRight) (algebraMap R B))

Tactic:
ext
-- 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
x : R
⊢ Eq (α := A ⊗[R] B) ((RingHom.comp includeLeftRingHom (algebraMap R A) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)
    ((RingHom.comp (AlgHom.toRingHom includeRight) (algebraMap R B) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : f.toLinearMap = g.toLinearMap
⊢ f = g

Tactic:
apply AlgHom.toLinearMap_injective

Premises used: AlgHom.toLinearMap_injective
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a :
  ∀ (a : A) (b : B),
    Eq.{uC + 1} (α := C)
      (((((AlgebraTensorModule.curry f.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
            (a : B) → C)
          b :
        C)
      (((((AlgebraTensorModule.curry g.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
            (a : B) → C)
          b :
        C)
⊢ f.toLinearMap = g.toLinearMap

Tactic:
ext a b
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
⊢ HMul.hMul (α := C) (β := C) ((f.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R f) includeRight : (a : B) → C) b : C) =
    HMul.hMul (α := C) (β := C) ((g.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R g) includeRight : (a : B) → C) b : C)

Tactic:
have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R f) includeRight : (a : B) → C) b : C) =
    HMul.hMul (α := C) (β := C) ((g.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R g) includeRight : (a : B) → C) b : C)
a₁ : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry f.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
    (((((AlgebraTensorModule.curry g.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)

Tactic:
dsimp at *
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
a₁ :
  ∀
    (this :
      (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
        HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
          ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₂ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)
        ((g : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₃ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)
        ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₄ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)
        ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₅ a₆ a₇ a₈ :
  ∀ (this : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)

Tactic:
rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this

Premises used: Algebra.TensorProduct.tmul_mul_tmul, map_mul, mul_one, one_mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
g h : A ⊗[R] B →ₐ[S] C
H :
  ∀ (a : A) (b : B),
    Eq.{uC + 1} (α := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((h : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ g = h

Tactic:
ext (AlgHom.ext fun _ => H _ _) (AlgHom.ext fun _ => H _ _)

Premises used: AlgHom.ext, OfNat.ofNat, Algebra.TensorProduct.ext
-- 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
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
a : ∀ (x : A ⊗[R] B), Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
⊢ f = g

Tactic:
ext x
-- 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
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) 0 : C) ((g : (a : A ⊗[R] B) → C) 0 : C)

Tactic:
simp
-- 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
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x y : A ⊗[R] B
h : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
h_1 : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) y : C) ((g : (a : A ⊗[R] B) → C) y : C)
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x + y) : C) ((g : (a : A ⊗[R] B) → C) (x + y) : C)

Tactic:
simp_all
-- 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
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x : A
y : B
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C) ((g : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C)

Tactic:
simpa [← map_mul] using congr($h₁ x * $h₂ y)

Premises used: map_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
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x : A ⊗[R] B
a : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) 0 : C) ((g : (a : A ⊗[R] B) → C) 0 : C)
a₁ :
  ∀ (x y : A ⊗[R] B),
    Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C) →
      Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) y : C) ((g : (a : A ⊗[R] B) → C) y : C) →
        Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x + y) : C) ((g : (a : A ⊗[R] B) → C) (x + y) : C)
a₂ :
  ∀ (x : A) (y : B),
    Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C) ((g : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C)
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)

Tactic:
induction x with
  | zero => simp
  | add x y _ _ => simp_all
  | tmul x y => simpa [← map_mul] using congr($h₁ x * $h₂ y)

Premises used: map_mul, TensorProduct.tmul
-- 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 : AddCommGroupWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
⊢ Eq (α := A ⊗[R] B) ((↑(↑n : ℤ) : A) ⊗ₜ[R] 1) (↑n : A ⊗[R] B)

Tactic:
simp [natCast_def]

Premises used: Algebra.TensorProduct.natCast_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 : AddCommGroupWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
⊢ Eq (α := A ⊗[R] B) ((↑(Int.negSucc n) : A) ⊗ₜ[R] 1) (-(↑(n + 1) : A ⊗[R] B))

Tactic:
simp [natCast_def, add_tmul, neg_tmul, one_def]

Premises used: TensorProduct.neg_tmul, Algebra.TensorProduct.natCast_def, TensorProduct.add_tmul, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommGroupWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
z : ℤ
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1)

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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
⊢ x * y = y * x

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

Premises used: TensorProduct.induction_on
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
refine_1 : 0 * y = y * 0
refine_2 : ∀ (x : A) (y_1 : B), x ⊗ₜ[R] y_1 * y = y * x ⊗ₜ[R] y_1
refine_3 : ∀ (x y_1 : A ⊗[R] B), x * y = y * x → y_1 * y = y * y_1 → (x + y_1) * y = y * (x + y_1)
⊢ x * y = y * x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
⊢ 0 * y = y * 0

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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁

Tactic:
TensorProduct.induction_on y ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
refine_2 : HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) 0 = HMul.hMul (α := A ⊗[R] B) 0 (a₁ ⊗ₜ[R] b₁)
refine_2₁ :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (x ⊗ₜ[R] y) = HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (a₁ ⊗ₜ[R] b₁)
refine_2₂ :
  ∀ (x y : A ⊗[R] B),
    a₁ ⊗ₜ[R] b₁ * x = x * a₁ ⊗ₜ[R] b₁ →
      a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁ → a₁ ⊗ₜ[R] b₁ * (x + y) = (x + y) * a₁ ⊗ₜ[R] b₁
⊢ a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) 0 = HMul.hMul (α := A ⊗[R] B) 0 (a₁ ⊗ₜ[R] b₁)

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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
a₂ : A
b₂ : B
⊢ HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = HMul.hMul (α := A ⊗[R] B) (a₂ ⊗ₜ[R] b₂) (a₁ ⊗ₜ[R] b₁)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
a₂ b₂ : A ⊗[R] B
ha : a₁ ⊗ₜ[R] b₁ * a₂ = a₂ * a₁ ⊗ₜ[R] b₁
hb : a₁ ⊗ₜ[R] b₁ * b₂ = b₂ * a₁ ⊗ₜ[R] b₁
⊢ a₁ ⊗ₜ[R] b₁ * (a₂ + b₂) = (a₂ + b₂) * a₁ ⊗ₜ[R] b₁

Tactic:
simp [mul_add, add_mul, ha, hb]

Premises used: add_mul, mul_add
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y x₁ x₂ : A ⊗[R] B
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)

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

Premises used: add_mul, mul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra R B
z : ℤ
rw : Eq (α := A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) z 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) z 1) (1 ⊗ₜ[R] (↑z : B))
rw₃ rw₄ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B)) (1 ⊗ₜ[R] (↑z : B))
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B))

Tactic:
rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.intCast_def, zsmul_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 : Ring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := AddCommGroup (A ⊗[R] B)) (Ring.toAddCommGroup : AddCommGroup (A ⊗[R] B))
    (addCommGroup.{uR, uA, uB} (R := R) (M := A) (N := B) : AddCommGroup (A ⊗[R] B))

Tactic:
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 : Ring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := AddCommGroup (A ⊗[R] B)) (Ring.toAddCommGroup : AddCommGroup (A ⊗[R] B))
    (addCommGroup.{uR, uA, uB} (R := R) (M := A) (N := B) : AddCommGroup (A ⊗[R] B))

Tactic:
with_reducible_and_instances 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 : Ring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq.{uA + 1} (α := Algebra ℤ (ℤ ⊗[ℤ] A)) (Ring.toIntAlgebra (ℤ ⊗[ℤ] A)) leftAlgebra

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct, TensorProduct.tmul, AddCon.toQuotient, 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 : CommSemiring B
inst_4 : Algebra R B
b : B
x : A ⊗[R] B
suffices :
  Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
⊢ HMul.hMul (α := A ⊗[R] B) ((AlgHom.toRingHom includeRight : (a : B) → A ⊗[R] B) b : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((AlgHom.toRingHom includeRight : (a : B) → A ⊗[R] B) b : A ⊗[R] B)

Tactic:
suffices LinearMap.mulLeft R (includeRight b) = LinearMap.mulRight R (includeRight b) from
      congr($this x)