awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
this :
  Function.Bijective (α := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β :=
    ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (⇑(lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
          ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x)) :
      (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
refine :
  Eq (α := ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
            ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        (((of (fun (i : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) i :
              TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →+ ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (a : (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i) → ⨁ (i : ι), (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i)
          x) :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
            ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        (((of (fun (i : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) i :
              TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →+ ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (a : (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i) → ⨁ (i : ι), (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i)
          y) :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
⊢ x = y

Tactic:
refine of_injective (β := fun i ↦ S ⊗[R] ℳ i) i <| this.injective ?_

Premises used: Function.Bijective.injective, DirectSum.of_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
x y : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)
h :
  Eq (α := ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) x :
      ↥(Submodule.baseChange S (ℳ i)))
    ((Submodule.toBaseChange S (ℳ i) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i))) y :
      ↥(Submodule.baseChange S (ℳ i)))
this :
  Function.Bijective (α := ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β :=
    ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (⇑(lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
          ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x)) :
      (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
⊢ Eq (α := ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
            ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        (((of (fun (i : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) i :
              TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →+ ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (a : (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i) → ⨁ (i : ι), (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i)
          x) :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (x : ι) ↦
            ↥(Submodule.baseChange S (ℳ x))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (a : ⨁ (i : ι), S ⊗[R] ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
        (((of (fun (i : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) i :
              TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →+ ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
            (a : (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i) → ⨁ (i : ι), (fun (i : ι) ↦ S ⊗[R] ↥(ℳ i)) i)
          y) :
      ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))

Tactic:
simpa using congr(of (fun i ↦ (ℳ i).baseChange S) i $h)
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
⊢ Function.Bijective (α := TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β := ↥(Submodule.baseChange S (ℳ i)))
    (⇑(Submodule.toBaseChange S (ℳ i)) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i)))

Tactic:
⟨toBaseChange_injective ℳ i, (ℳ i).toBaseChange_surjective S⟩

Premises used: Submodule.toBaseChange_surjective, DirectSum.toBaseChange_injective, And.intro, Function.Bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
hm : IsInternal ℳ
⊢ IsInternal (S := Submodule S (S ⊗[R] M)) fun (i : ι) ↦ Submodule.baseChange S (ℳ i)

Tactic:
haveI := hm.chooseDecomposition
  Decomposition.isInternal _

Premises used: DirectSum.Decomposition.isInternal, Submodule.baseChange
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
hm : IsInternal ℳ
i : ι
⊢ Function.Bijective (α := TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β := ↥(Submodule.baseChange S (ℳ i)))
    (⇑(Submodule.toBaseChange S (ℳ i)) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i)))

Tactic:
haveI := hm.chooseDecomposition
  DirectSum.toBaseChange_bijective ℳ i

Premises used: DirectSum.toBaseChange_bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
hm : IsInternal ℳ
i : ι
⊢ Function.Injective (α := TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) (β := ↥(Submodule.baseChange S (ℳ i)))
    (⇑(Submodule.toBaseChange S (ℳ i)) : (a : S ⊗[R] ↥(ℳ i)) → ↥(Submodule.baseChange S (ℳ i)))

Tactic:
(toBaseChange_bijective ℳ hm i).injective

Premises used: Function.Bijective.injective, DirectSum.IsInternal.toBaseChange_bijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x_1 : M × N
y : FreeAddMonoid (M × N)
ih : motive (↑y : (addConGen (Eqv R M N)).Quotient)
m : M
n : N
rw :
  motive
    (HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R M N)))
      (↑(FreeAddMonoid.of (m, n)) : (addConGen (Eqv R M N)).Quotient) (↑y : (addConGen (Eqv R M N)).Quotient))
⊢ motive (↑(FreeAddMonoid.of (m, n) + y) : (addConGen (Eqv R M N)).Quotient)

Tactic:
rw [AddCon.coe_add]

Premises used: AddCon.coe_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x_1 : M × N
y : FreeAddMonoid (M × N)
ih : motive (↑y : (addConGen (Eqv R M N)).Quotient)
m : M
n : N
⊢ motive
    (HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R M N)))
      (↑(FreeAddMonoid.of (m, n)) : (addConGen (Eqv R M N)).Quotient) (↑y : (addConGen (Eqv R M N)).Quotient))

Tactic:
add _ _ (tmul ..) ih
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x_1 : M × N
y : FreeAddMonoid (M × N)
ih : motive (↑y : (addConGen (Eqv R M N)).Quotient)
m : M
n : N
⊢ motive
    (HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R M N)))
      (↑(FreeAddMonoid.of (m, n)) : (addConGen (Eqv R M N)).Quotient) (↑y : (addConGen (Eqv R M N)).Quotient))

Tactic:
exact add _ _ (tmul ..) ih
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : N
⊢ Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] n) 0

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_left _

Premises used: Quotient.sound', AddConGen.Rel.of, TensorProduct.Eqv.of_zero_left, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m₁ m₂ : M
n : N
⊢ (m₁ + m₂) ⊗ₜ[R] n = HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n) (m₂ ⊗ₜ[R] n)

Tactic:
Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_left _ _ _

Premises used: Quotient.sound', AddConGen.Rel.of, Eq.symm, TensorProduct.Eqv.of_add_left
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] 0) 0

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_right _

Premises used: Quotient.sound', AddConGen.Rel.of, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, TensorProduct.Eqv.of_zero_right
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
n₁ n₂ : N
⊢ m ⊗ₜ[R] (n₁ + n₂) = HAdd.hAdd (α := M ⊗[R] N) (m ⊗ₜ[R] n₁) (m ⊗ₜ[R] n₂)

Tactic:
Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_right _ _ _

Premises used: Quotient.sound', TensorProduct.Eqv.of_add_right, AddConGen.Rel.of, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Subsingleton M
z : M ⊗[R] N
x : M
y : N
rw : Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] y) 0
rw₁ rw₂ : Eq (α := M ⊗[R] N) 0 0
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0

Tactic:
rw [Subsingleton.elim x 0, zero_tmul]

Premises used: TensorProduct.zero_tmul, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Subsingleton M
z : M ⊗[R] N
⊢ HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Subsingleton N
z : M ⊗[R] N
x : M
y : N
rw : Eq (α := M ⊗[R] N) (x ⊗ₜ[R] 0) 0
rw₁ rw₂ : Eq (α := M ⊗[R] N) 0 0
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0

Tactic:
rw [Subsingleton.elim y 0, tmul_zero]

Premises used: TensorProduct.tmul_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Subsingleton N
z : M ⊗[R] N
⊢ HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
rw : (r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n
| (r • m) ⊗ₜ[R] n

Tactic:
rw [← one_smul R m]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
conv_lhs : Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))
⊢ Eq (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))

Tactic:
conv_lhs => rw [← one_smul R m]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
rw : m ⊗ₜ[R] (r • HSMul.hSMul.{u_1, u_8, u_8} (α := R) 1 n)
| m ⊗ₜ[R] (r • n)

Tactic:
rw [← one_smul R n]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
conv_rhs :
  Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n)
    (m ⊗ₜ[R] (r • HSMul.hSMul.{u_1, u_8, u_8} (α := R) 1 n))
⊢ Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))

Tactic:
conv_rhs => rw [← one_smul R n]

Premises used: one_smul