awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
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 ℳ
⊢ Eq (α := (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
            lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
              ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
        ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
    (LinearMap.id ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M) :
      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)
have refine_1 : ∀ (i : ι) (x : ↥(ℳ i)),
  Eq (α := S ⊗[R] M)
    (((((AlgebraTensorModule.curry
                      (((coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
                            lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                              ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] S ⊗[R] M) ∘ₗ
                        ((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                            (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) :
                    S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                  (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                1 ∘ₗ
              lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
            ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
          (a : ↥(ℳ i)) → S ⊗[R] M)
        x :
      S ⊗[R] M)
    (((((AlgebraTensorModule.curry
                      (LinearMap.id ∘ₗ
                        (↑(LinearEquiv.symm
                              (LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) :
                          (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] S ⊗[R] M)) :
                    S →ₗ[S] (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M) :
                  (a : S) → (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] S ⊗[R] M)
                1 ∘ₗ
              lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i :
            ↥(ℳ i) →ₗ[R] S ⊗[R] M) :
          (a : ↥(ℳ i)) → S ⊗[R] M)
        x :
      S ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
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 ℳ
⊢ Eq (α := (⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
            ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
          (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
        (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
              (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
            ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
          S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
      coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i))
    LinearMap.id
have refine_2 : ∀ (i : ι),
  Eq (α := ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    ((((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
              (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
            (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                  (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
                ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                    S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                  S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
              S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
          coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
        lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
      ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (LinearMap.id ∘ₗ lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
      ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (hypothesis)
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)))
⊢ x = y
have 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)))
Tactic: have := (Function.Bijective.of_comp_iff (lmap (ℳ · |>.toBaseChange S))
    (by rw [← LinearEquiv.coe_trans]; exact LinearEquiv.bijective _)).1
    (decompose (M := S ⊗[R] M) fun i ↦ (ℳ i).baseChange S).bijective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Decomposition (goal)
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)))
⊢ x = y
have 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)))
Tactic: refine of_injective (β := fun i ↦ S ⊗[R] ℳ i) i <| this.injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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 (↑(FreeAddMonoid.of (m, n) + y) : (addConGen (Eqv R M N)).Quotient)
have 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))
Tactic: rw [AddCon.coe_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0
have rw : Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] y) 0
Tactic: rw [Subsingleton.elim x 0, zero_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0
have rw₁ : Eq (α := M ⊗[R] N) 0 0
Tactic: rw [Subsingleton.elim x 0, zero_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0
have rw : Eq (α := M ⊗[R] N) (x ⊗ₜ[R] 0) 0
Tactic: rw [Subsingleton.elim y 0, tmul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) 0
have rw₁ : Eq (α := M ⊗[R] N) 0 0
Tactic: rw [Subsingleton.elim y 0, tmul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
| (r • m) ⊗ₜ[R] n
have rw : (r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n
Tactic: rw [← one_smul R m]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))
have conv_lhs : Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))
Tactic: conv_lhs => rw [← one_smul R m]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
| m ⊗ₜ[R] (r • n)
have rw : m ⊗ₜ[R] (r • HSMul.hSMul.{u_1, u_8, u_8} (α := R) 1 n)
Tactic: rw [← one_smul R n]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))
have 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))
Tactic: conv_rhs => rw [← one_smul R n]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ 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))
have rw : Eq (α := M ⊗[R] N) ((HSMul.hSMul (β := R) r 1 • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (HSMul.hSMul (β := R) r 1 • n))
Tactic: rw [← smul_assoc, ← smul_assoc]