awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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) := ⋯
⊢ ∀ (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)
have rw : LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
Tactic: rw [LinearMap.map_mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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) := ⋯
⊢ LinearMap.compr₂ (LinearMap.mul R (⨂[R] (x : ι), R)) toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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) := ⋯
⊢ 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)
have 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)
Tactic: change toFun (tprod R _ * tprod R _) = toFun (tprod R _) * toFun (tprod R _)
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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) := ⋯
⊢ (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)
have H : (toFun : (a : ⨂[R] (i : ι), R) → R)
    ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R)
        (HMul.hMul (α := (i : ι) → R) (fun (x : ι) ↦ 1) fun (x : ι) ↦ 1) :
      ⨂[R] (i : ι), R) =
  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)
Tactic: simp_rw [tprod_mul_tprod, toFun, lift.tprod, MultilinearMap.mkPiAlgebra_apply,
          Pi.mul_apply, Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (↑(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
have 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)
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (↑(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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (↑(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
have 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)
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (↑(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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (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
have 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
Tactic: simp_rw [rTensorInv, LinearEquiv.coe_trans, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ (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
have 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)
Tactic: rw [← LinearEquiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
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] M →ₗ[R] Q ⊗[R] M
⊢ Eq (α := P →ₗ[R] Q)
    ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q)
        (AddHom.toFun (LinearMap.toAddHom (LinearMap.rTensorHom M))
          ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x)) :
      P →ₗ[R] Q)
    ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
have rw : Eq (α := P →ₗ[R] Q)
  ((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)
        ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x)) :
    P →ₗ[R] Q)
  ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
Tactic: rw [LinearMap.toFun_eq_coe, rTensorInv_leftInverse]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
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] M →ₗ[R] Q ⊗[R] M
rw :
  Eq (α := P →ₗ[R] Q)
    ((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)
          ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x)) :
      P →ₗ[R] Q)
    ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
⊢ Eq (α := P →ₗ[R] Q)
    ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q)
        (AddHom.toFun (LinearMap.toAddHom (LinearMap.rTensorHom M))
          ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x)) :
      P →ₗ[R] Q)
    ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
have rw₁ : Eq (α := P →ₗ[R] Q) ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
  ((rTensorInv P Q e : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q) x : P →ₗ[R] Q)
Tactic: rw [LinearMap.toFun_eq_coe, rTensorInv_leftInverse]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ curry (↑e : M ⊗[R] N →ₗ[R] R) =
    (↑(LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight) :
        (R ⊗[R] N →ₗ[R] M ⊗[R] N) →ₗ[R] N →ₗ[R] R) ∘ₗ
      rTensorHom N ∘ₗ (↑(LinearEquiv.symm (ringLmapEquivSelf R R M)) : M →ₗ[R] R →ₗ[R] M)
have rw : (↑(LinearEquiv.symm (LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight)) :
      (N →ₗ[R] R) →ₗ[R] R ⊗[R] N →ₗ[R] M ⊗[R] N) ∘ₗ
    curry (↑e : M ⊗[R] N →ₗ[R] R) =
  rTensorHom N ∘ₗ (↑(LinearEquiv.symm (ringLmapEquivSelf R R M)) : M →ₗ[R] R →ₗ[R] M)
Tactic: rw [← LinearEquiv.toLinearMap_symm_comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ (↑(LinearEquiv.symm (LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight)) :
        (N →ₗ[R] R) →ₗ[R] R ⊗[R] N →ₗ[R] M ⊗[R] N) ∘ₗ
      curry (↑e : M ⊗[R] N →ₗ[R] R) =
    rTensorHom N ∘ₗ (↑(LinearEquiv.symm (ringLmapEquivSelf R R M)) : M →ₗ[R] R →ₗ[R] M)
have h : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R] N)
    ((((AlgebraTensorModule.curry
                  (((↑(LinearEquiv.symm (LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight)) :
                          (N →ₗ[R] R) →ₗ[R] R ⊗[R] N →ₗ[R] M ⊗[R] N) ∘ₗ
                        curry (↑e : M ⊗[R] N →ₗ[R] R) :
                      (a : M) → R ⊗[R] N →ₗ[R] M ⊗[R] N)
                    x) :
                R →ₗ[R] N →ₗ[R] M ⊗[R] N) :
              (a : R) → N →ₗ[R] M ⊗[R] N)
            1 :
          (a : N) → M ⊗[R] N)
        x_1 :
      M ⊗[R] N)
    ((((AlgebraTensorModule.curry
                  ((rTensorHom N ∘ₗ (↑(LinearEquiv.symm (ringLmapEquivSelf R R M)) : M →ₗ[R] R →ₗ[R] M) :
                      (a : M) → R ⊗[R] N →ₗ[R] M ⊗[R] N)
                    x) :
                R →ₗ[R] N →ₗ[R] M ⊗[R] N) :
              (a : R) → N →ₗ[R] M ⊗[R] N)
            1 :
          (a : N) → M ⊗[R] N)
        x_1 :
      M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ Function.Bijective (α := M) (β := N →ₗ[R] R) (⇑(curry (↑e : M ⊗[R] N →ₗ[R] R)) : (a : M) → N →ₗ[R] R)
have this : curry (↑e : M ⊗[R] N →ₗ[R] R) =
  (↑(LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight) :
      (R ⊗[R] N →ₗ[R] M ⊗[R] N) →ₗ[R] N →ₗ[R] R) ∘ₗ
    rTensorHom N ∘ₗ (↑(LinearEquiv.symm (ringLmapEquivSelf R R M)) : M →ₗ[R] R →ₗ[R] M)
Tactic: have : curry e.toLinearMap = ((TensorProduct.lid R N).congrLeft _ R ≪≫ₗ e.congrRight) ∘ₗ
      rTensorHom N ∘ₗ (ringLmapEquivSelf R R M).symm.toLinearMap := by
    rw [← LinearEquiv.toLinearMap_symm_comp_eq]; ext
    simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N = (↑(LinearEquiv.symm (LinearEquiv.rTensor N (linearEquivDual e)) ≪≫ₗ e) : Dual R N ⊗[R] N →ₗ[R] R)
have rw : contractLeft R N ∘ₗ (↑(LinearEquiv.rTensor N (linearEquivDual e)) : M ⊗[R] N →ₗ[R] Dual R N ⊗[R] N) =
  (↑e : M ⊗[R] N →ₗ[R] R)
Tactic: rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N ∘ₗ (↑(LinearEquiv.rTensor N (linearEquivDual e)) : M ⊗[R] N →ₗ[R] Dual R N ⊗[R] N) =
    (↑e : M ⊗[R] N →ₗ[R] R)
have a : ∀ (x : M) (x_1 : N),
  Eq.{u + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (contractLeft R N ∘ₗ
                      (↑(LinearEquiv.rTensor N (linearEquivDual e)) : M ⊗[R] N →ₗ[R] Dual R N ⊗[R] N)) :
                  M →ₗ[R] N →ₗ[R] R) :
                (a : M) → N →ₗ[R] R)
              x :
            N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)
    (((((AlgebraTensorModule.curry (↑e : M ⊗[R] N →ₗ[R] R) : M →ₗ[R] N →ₗ[R] R) : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
⊢ Module.Finite R M ∧ Projective R M
have have : ∀ (S : Finset (M × N)) (hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)),
  Module.Finite R M ∧ Projective R M
Tactic: have ⟨S, hS⟩ := TensorProduct.exists_finset (e.symm 1)