awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
x y : ⨂[R] (i : ι), A i
suffices :
  Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (mul (A := A))
    (LinearMap.flip (mul (A := A)))
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        y :
      ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) y :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        x :
      ⨂[R] (i : ι), A i)

Tactic:
suffices mul (R := R) (A := A) = mul.flip from
    DFunLike.congr_fun (DFunLike.congr_fun this x) y
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
x y : ⨂[R] (i : ι), A i
H :
  ∀ (x y : (i : ι) → A i),
    Eq (α := ⨂[R] (i : ι), A i)
      ((LinearMap.compMultilinearMap (M₁ := A)
              ((LinearMap.compMultilinearMap (M₁ := A) (mul (A := A)) (tprod R (s := A)) :
                  (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                x)
              (tprod R (s := A)) :
            (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
          y :
        ⨂[R] (i : ι), A i)
      ((LinearMap.compMultilinearMap (M₁ := A)
              ((LinearMap.compMultilinearMap (M₁ := A) (LinearMap.flip (mul (A := A))) (tprod R (s := A)) :
                  (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                x)
              (tprod R (s := A)) :
            (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
          y :
        ⨂[R] (i : ι), A i)
⊢ Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (mul (A := A))
    (LinearMap.flip (mul (A := A)))

Tactic:
ext x y
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
x_1 y_1 : ⨂[R] (i : ι), A i
x y : (i : ι) → A i
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y) :
      ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) y) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) x) :
      ⨂[R] (i : ι), A i)

Tactic:
simp only [mul_tprod_tprod, mul_tprod_tprod, mul_comm x y]

Premises used: PiTensorProduct.mul_tprod_tprod, mul_comm
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
κ : Type u_5
s : Finset κ
x : κ → (i : ι) → A i
⊢ Eq (α := ⨂[R] (i : ι), A i) ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (∏ k ∈ s, x k))
    (∏ k ∈ s, (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (x k))

Tactic:
map_prod (tprodMonoidHom R) x s

Premises used: PiTensorProduct.tprodMonoidHom, map_prod, PiTensorProduct.tprodCoeff, AddCon.toQuotient
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
this_1 : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
rw : LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
⊢ ∀ (x y : ⨂[R] (x : ι), R),
    (toFun : (a : ⨂[R] (x : ι), R) → R) (x * y) =
      HMul.hMul (α := R) (β := R) ((toFun : (a : ⨂[R] (x : ι), R) → R) x : R)
        ((toFun : (a : ⨂[R] (x : ι), R) → R) y : R)

Tactic:
rw [LinearMap.map_mul_iff]

Premises used: LinearMap.map_mul_iff
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
this_1 : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
H :
  Eq.{u_3 + 1} (α := R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
            ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
                  (LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun) (tprod R (s := fun (i : ι) ↦ R)) :
                (a : (i : ι) → R) → (⨂[R] (x : ι), R) →ₗ[R] R)
              fun (x : ι) ↦ 1)
            (tprod R (s := fun (i : ι) ↦ R)) :
          (a : (i : ι) → R) → R)
        fun (x : ι) ↦ 1 :
      R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
            ((((LinearMap.mul R R ∘ₗ toFun).compl₂ toFun).compMultilinearMap (M₁ := fun (i : ι) ↦ R)
                  (tprod R (s := fun (i : ι) ↦ R)) :
                (a : (i : ι) → R) → (⨂[R] (x : ι), R) →ₗ[R] R)
              fun (x : ι) ↦ 1)
            (tprod R (s := fun (i : ι) ↦ R)) :
          (a : (i : ι) → R) → R)
        fun (x : ι) ↦ 1 :
      R)
⊢ LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun

Tactic:
ext
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
this_1 : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
H :
  (toFun : (a : ⨂[R] (i : ι), R) → R)
      (HMul.hMul (α := ⨂[R] (i : ι), R)
        ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1)
        ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1)) =
    HMul.hMul (α := R) (β := R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
⊢ Eq.{u_3 + 1} (α := R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
            ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
                  (LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun) (tprod R (s := fun (i : ι) ↦ R)) :
                (a : (i : ι) → R) → (⨂[R] (x : ι), R) →ₗ[R] R)
              fun (x : ι) ↦ 1)
            (tprod R (s := fun (i : ι) ↦ R)) :
          (a : (i : ι) → R) → R)
        fun (x : ι) ↦ 1 :
      R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ R)
            ((((LinearMap.mul R R ∘ₗ toFun).compl₂ toFun).compMultilinearMap (M₁ := fun (i : ι) ↦ R)
                  (tprod R (s := fun (i : ι) ↦ R)) :
                (a : (i : ι) → R) → (⨂[R] (x : ι), R) →ₗ[R] R)
              fun (x : ι) ↦ 1)
            (tprod R (s := fun (i : ι) ↦ R)) :
          (a : (i : ι) → R) → R)
        fun (x : ι) ↦ 1 :
      R)

Tactic:
change toFun (tprod R _ * tprod R _) = toFun (tprod R _) * toFun (tprod R _)

Premises used: HMul.hMul, PiTensorProduct.tprod, DFunLike.coe
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
⊢ (AlgHom.ofLinearMap toFun ⋯ ⋯).comp (Algebra.ofId R (⨂[R] (x : ι), R)) = AlgHom.id R R

Tactic:
ext
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
⊢ AlgHom.comp (Algebra.ofId R (⨂[R] (x : ι), R)) (AlgHom.ofLinearMap toFun ⋯ ⋯) = AlgHom.id R (⨂[R] (x : ι), R)

Tactic:
ext
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
⊢ AlgHom.comp (Algebra.ofId R (⨂[R] (x : ι), R)) (AlgHom.ofLinearMap toFun ⋯ ⋯) = AlgHom.id R (⨂[R] (x : ι), R)

Tactic:
classical ext
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : Fintype ι
x : ι → R
⊢ Eq.{u_3 + 1} (α := R)
    ((constantBaseRingEquiv ι R : (a : ⨂[R] (x : ι), R) → R)
        ((tprod R (s := fun (x : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) x : ⨂[R] (i : ι), R) :
      R)
    (∏ i : ι, x i : R)

Tactic:
simp [constantBaseRingEquiv]

Premises used: PiTensorProduct.constantBaseRingEquiv
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : Fintype ι
r : R
⊢ Eq (α := ⨂[R] (x : ι), R)
    ((AlgEquiv.symm (constantBaseRingEquiv ι R) : (a : R) → ⨂[R] (x : ι), R) r : ⨂[R] (x : ι), R)
    ((algebraMap R (⨂[R] (x : ι), R) : (a : R) → ⨂[R] (x : ι), R) r : ⨂[R] (x : ι), R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, PiTensorProduct.tprodCoeff, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
rw :
  (↑(leftCancelEquiv Q e) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] Q) ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) =
    f ∘ₗ (↑(leftCancelEquiv P e) : M ⊗[R] (N ⊗[R] P) →ₗ[R] P)
⊢ (↑(leftCancelEquiv Q e) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] Q) ∘ₗ
      LinearMap.lTensor M (LinearMap.lTensor N f) ∘ₗ
        (↑(LinearEquiv.symm (leftCancelEquiv P e)) : P →ₗ[R] M ⊗[R] (N ⊗[R] P)) =
    f

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq]

Premises used: LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq.{u_3 + 1} (α := Q)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              ((↑(leftCancelEquiv Q e) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] Q) ∘ₗ
                                LinearMap.lTensor M (LinearMap.lTensor N f)) :
                            M →ₗ[R] N ⊗[R] P →ₗ[R] Q) :
                          (a : M) → N ⊗[R] P →ₗ[R] Q)
                        x) :
                    N →ₗ[R] P →ₗ[R] Q) :
                  (a : N) → P →ₗ[R] Q)
                x_1 :
              P →ₗ[R] Q) :
            (a : P) → Q)
          x_2 :
        Q)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry (f ∘ₗ (↑(leftCancelEquiv P e) : M ⊗[R] (N ⊗[R] P) →ₗ[R] P)) :
                            M →ₗ[R] N ⊗[R] P →ₗ[R] Q) :
                          (a : M) → N ⊗[R] P →ₗ[R] Q)
                        x) :
                    N →ₗ[R] P →ₗ[R] Q) :
                  (a : N) → P →ₗ[R] Q)
                x_1 :
              P →ₗ[R] Q) :
            (a : P) → Q)
          x_2 :
        Q)
⊢ (↑(leftCancelEquiv Q e) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] Q) ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) =
    f ∘ₗ (↑(leftCancelEquiv P e) : M ⊗[R] (N ⊗[R] P) →ₗ[R] P)

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
x : M
x_1 : N
x_2 : P
⊢ Eq.{u_3 + 1} (α := Q)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            ((↑(leftCancelEquiv Q e) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] Q) ∘ₗ
                              LinearMap.lTensor M (LinearMap.lTensor N f)) :
                          M →ₗ[R] N ⊗[R] P →ₗ[R] Q) :
                        (a : M) → N ⊗[R] P →ₗ[R] Q)
                      x) :
                  N →ₗ[R] P →ₗ[R] Q) :
                (a : N) → P →ₗ[R] Q)
              x_1 :
            P →ₗ[R] Q) :
          (a : P) → Q)
        x_2 :
      Q)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (f ∘ₗ (↑(leftCancelEquiv P e) : M ⊗[R] (N ⊗[R] P) →ₗ[R] P)) :
                          M →ₗ[R] N ⊗[R] P →ₗ[R] Q) :
                        (a : M) → N ⊗[R] P →ₗ[R] Q)
                      x) :
                  N →ₗ[R] P →ₗ[R] Q) :
                (a : N) → P →ₗ[R] Q)
              x_1 :
            P →ₗ[R] Q) :
          (a : P) → Q)
        x_2 :
      Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
rw :
  (↑(rightCancelEquiv Q e) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M f) =
    f ∘ₗ (↑(rightCancelEquiv P e) : P ⊗[R] M ⊗[R] N →ₗ[R] P)
⊢ (↑(rightCancelEquiv Q e) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q) ∘ₗ
      LinearMap.rTensor N (LinearMap.rTensor M f) ∘ₗ
        (↑(LinearEquiv.symm (rightCancelEquiv P e)) : P →ₗ[R] P ⊗[R] M ⊗[R] N) =
    f

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq]

Premises used: LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
a :
  ∀ (x : P) (x_1 : M) (x_2 : N),
    Eq.{u_3 + 1} (α := Q)
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              ((↑(rightCancelEquiv Q e) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q) ∘ₗ
                                LinearMap.rTensor N (LinearMap.rTensor M f))) :
                          P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                        (a : P) → M →ₗ[R] N →ₗ[R] Q)
                      x :
                    M →ₗ[R] N →ₗ[R] Q) :
                  (a : M) → N →ₗ[R] Q)
                x_1 :
              N →ₗ[R] Q) :
            (a : N) → Q)
          x_2 :
        Q)
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry (f ∘ₗ (↑(rightCancelEquiv P e) : P ⊗[R] M ⊗[R] N →ₗ[R] P))) :
                          P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                        (a : P) → M →ₗ[R] N →ₗ[R] Q)
                      x :
                    M →ₗ[R] N →ₗ[R] Q) :
                  (a : M) → N →ₗ[R] Q)
                x_1 :
              N →ₗ[R] Q) :
            (a : N) → Q)
          x_2 :
        Q)
⊢ (↑(rightCancelEquiv Q e) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M f) =
    f ∘ₗ (↑(rightCancelEquiv P e) : P ⊗[R] M ⊗[R] N →ₗ[R] P)

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
x : P
x_1 : M
x_2 : N
⊢ Eq.{u_3 + 1} (α := Q)
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry
                            ((↑(rightCancelEquiv Q e) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q) ∘ₗ
                              LinearMap.rTensor N (LinearMap.rTensor M f))) :
                        P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                      (a : P) → M →ₗ[R] N →ₗ[R] Q)
                    x :
                  M →ₗ[R] N →ₗ[R] Q) :
                (a : M) → N →ₗ[R] Q)
              x_1 :
            N →ₗ[R] Q) :
          (a : N) → Q)
        x_2 :
      Q)
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry (f ∘ₗ (↑(rightCancelEquiv P e) : P ⊗[R] M ⊗[R] N →ₗ[R] P))) :
                        P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                      (a : P) → M →ₗ[R] N →ₗ[R] Q)
                    x :
                  M →ₗ[R] N →ₗ[R] Q) :
                (a : M) → N →ₗ[R] Q)
              x_1 :
            N →ₗ[R] Q) :
          (a : N) → Q)
        x_2 :
      Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
x : P →ₗ[R] Q
simp_rw :
  (LinearEquiv.congrLeft Q R (rightCancelEquiv P e) : (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q) → P →ₗ[R] Q)
      ((LinearEquiv.congrRight (rightCancelEquiv Q e) :
          (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        ((LinearMap.rTensorHom N : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N)
          ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x))) =
    x
⊢ (rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q)
      ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x) =
    x

Tactic:
simp_rw [rTensorInv, LinearEquiv.coe_trans, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap]

Premises used: Module.Invertible.rTensorInv, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, LinearEquiv.coe_trans
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
x : P →ₗ[R] Q
rw :
  Eq (α := P ⊗[R] M ⊗[R] N →ₗ[R] Q)
    ((LinearEquiv.congrRight (rightCancelEquiv Q e) :
          (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        ((LinearMap.rTensorHom N : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N)
          ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x)) :
      P ⊗[R] M ⊗[R] N →ₗ[R] Q)
    ((LinearEquiv.symm (LinearEquiv.congrLeft Q R (rightCancelEquiv P e)) : (a : P →ₗ[R] Q) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        x :
      P ⊗[R] M ⊗[R] N →ₗ[R] Q)
⊢ (LinearEquiv.congrLeft Q R (rightCancelEquiv P e) : (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q) → P →ₗ[R] Q)
      ((LinearEquiv.congrRight (rightCancelEquiv Q e) :
          (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        ((LinearMap.rTensorHom N : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N)
          ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x))) =
    x

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
x : P →ₗ[R] Q
a :
  ∀ (x_1 : P) (x_2 : M) (x_3 : N),
    Eq.{u_3 + 1} (α := Q)
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              ((LinearEquiv.congrRight (rightCancelEquiv Q e) :
                                  (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
                                ((LinearMap.rTensorHom N :
                                    (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N)
                                  ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x)))) :
                          P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                        (a : P) → M →ₗ[R] N →ₗ[R] Q)
                      x_1 :
                    M →ₗ[R] N →ₗ[R] Q) :
                  (a : M) → N →ₗ[R] Q)
                x_2 :
              N →ₗ[R] Q) :
            (a : N) → Q)
          x_3 :
        Q)
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              ((LinearEquiv.symm (LinearEquiv.congrLeft Q R (rightCancelEquiv P e)) :
                                  (a : P →ₗ[R] Q) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
                                x)) :
                          P →ₗ[R] M →ₗ[R] N →ₗ[R] Q) :
                        (a : P) → M →ₗ[R] N →ₗ[R] Q)
                      x_1 :
                    M →ₗ[R] N →ₗ[R] Q) :
                  (a : M) → N →ₗ[R] Q)
                x_2 :
              N →ₗ[R] Q) :
            (a : N) → Q)
          x_3 :
        Q)
⊢ Eq (α := P ⊗[R] M ⊗[R] N →ₗ[R] Q)
    ((LinearEquiv.congrRight (rightCancelEquiv Q e) :
          (a : P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        ((LinearMap.rTensorHom N : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] M ⊗[R] N)
          ((LinearMap.rTensorHom M : (a : P →ₗ[R] Q) → P ⊗[R] M →ₗ[R] Q ⊗[R] M) x)) :
      P ⊗[R] M ⊗[R] N →ₗ[R] Q)
    ((LinearEquiv.symm (LinearEquiv.congrLeft Q R (rightCancelEquiv P e)) : (a : P →ₗ[R] Q) → P ⊗[R] M ⊗[R] N →ₗ[R] Q)
        x :
      P ⊗[R] M ⊗[R] N →ₗ[R] Q)

Tactic:
ext