awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]

Premises used: LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv, LinearEquiv.congrLeft
-- 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
⊢ Function.Injective (α := P ⊗[R] M →ₗ[R] Q ⊗[R] M) (β := P →ₗ[R] Q)
    (⇑(rTensorInv P Q e) : (a : P ⊗[R] M →ₗ[R] Q ⊗[R] M) → P →ₗ[R] Q)

Tactic:
simpa [rTensorInv] using (rTensorInv_leftInverse _ _ <| TensorProduct.comm R N M ≪≫ₗ e).injective

Premises used: Function.LeftInverse.injective, TensorProduct.comm, Module.Invertible.rTensorInv, Module.Invertible.rTensorInv_leftInverse, LinearEquiv.trans
-- Module: Mathlib.RingTheory.PicardGroup
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [LinearMap.toFun_eq_coe, rTensorInv_leftInverse]

Premises used: LinearMap.toFun_eq_coe, Module.Invertible.rTensorInv_leftInverse
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ 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:
rw [← LinearEquiv.toLinearMap_symm_comp_eq]

Premises used: LinearEquiv.toLinearMap_symm_comp_eq
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ (↑(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:
ext
-- Module: Mathlib.RingTheory.PicardGroup
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
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:
simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]

Premises used: LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv, LinearEquiv.congrLeft
-- Module: Mathlib.RingTheory.PicardGroup
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)

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]
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ Function.Bijective (α := M) (β := N →ₗ[R] R) (⇑(curry (↑e : M ⊗[R] N →ₗ[R] R)) : (a : M) → N →ₗ[R] R)

Tactic:
simpa [this] using (rTensorEquiv R M <| TensorProduct.comm R N M ≪≫ₗ e).bijective

Premises used: TensorProduct.comm, LinearEquiv.bijective, Module.Invertible.rTensorEquiv, LinearEquiv.trans
-- Module: Mathlib.RingTheory.PicardGroup
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
rw :
  contractLeft R N ∘ₗ (↑(LinearEquiv.rTensor N (linearEquivDual e)) : M ⊗[R] N →ₗ[R] Dual R N ⊗[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)

Tactic:
rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]

Premises used: LinearEquiv.eq_comp_toLinearMap_symm, LinearEquiv.coe_trans
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ contractLeft R N ∘ₗ (↑(LinearEquiv.rTensor N (linearEquivDual e)) : M ⊗[R] N →ₗ[R] Dual R N ⊗[R] N) =
    (↑e : M ⊗[R] N →ₗ[R] R)

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
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
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:
rfl
-- Module: Mathlib.RingTheory.PicardGroup
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 (α := Dual R N ⊗[R] N) (β := R)
    (⇑(↑(LinearEquiv.symm (LinearEquiv.rTensor N (linearEquivDual e)) ≪≫ₗ e) : Dual R N ⊗[R] N →ₗ[R] R) :
      (a : Dual R N ⊗[R] N) → R)

Tactic:
apply LinearEquiv.bijective

Premises used: LinearEquiv.bijective
-- Module: Mathlib.RingTheory.PicardGroup
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
⊢ Module.Invertible R M

Tactic:
.right (TensorProduct.comm R N M ≪≫ₗ e)

Premises used: TensorProduct.comm, LinearEquiv.trans, Module.Invertible.right
-- Module: Mathlib.RingTheory.PicardGroup
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
⊢ Module.Invertible R R

Tactic:
.left (TensorProduct.lid R R)

Premises used: TensorProduct.lid, Module.Invertible.left
-- Module: Mathlib.RingTheory.PicardGroup
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
inst_5 : Module.Invertible R M
e : M ≃ₗ[R] N
⊢ Module.Invertible R N

Tactic:
.right (e.symm.lTensor _ ≪≫ₗ linearEquiv R M)

Premises used: LinearEquiv.symm, LinearEquiv.lTensor, LinearEquiv.trans, Module.Invertible.linearEquiv, Module.Invertible.right
-- Module: Mathlib.RingTheory.PicardGroup
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
inst_9 : Module.Invertible R M
⊢ Module.Invertible R (Dual R M)

Tactic:
.left (linearEquiv R M)

Premises used: Module.Invertible.left, Module.Invertible.linearEquiv
-- Module: Mathlib.RingTheory.PicardGroup
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
inst_9 : Module.Invertible R M
inst_10 : Module.Invertible R N
⊢ Module.Invertible R (M ⊗[R] N)

Tactic:
.right (M := Dual R M ⊗[R] Dual R N) <| tensorTensorTensorComm .. ≪≫ₗ
    congr (linearEquiv R M) (linearEquiv R N) ≪≫ₗ TensorProduct.lid R R

Premises used: TensorProduct.congr, TensorProduct.tensorTensorTensorComm, TensorProduct.lid, LinearEquiv.trans, Module.Invertible.linearEquiv, Module.Invertible.right
-- Module: Mathlib.RingTheory.PicardGroup
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
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
⊢ Module.Finite R M ∧ Projective R M

Tactic:
have ⟨S, hS⟩ := TensorProduct.exists_finset (e.symm 1)
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
rw : 1 ∈ f.range
⊢ Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)

Tactic:
rw [← LinearMap.range_eq_top, Ideal.eq_top_iff_one]

Premises used: LinearMap.range_eq_top, Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
h :
  Eq.{u + 1} (α := R)
    ((f : (a : ↥S →₀ N) → R)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2) :
      R)
    (1 : R)
⊢ 1 ∈ f.range

Tactic:
use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2

Premises used: Finsupp.equivFunOnFinite, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
h :
  Eq.{u + 1} (α := R)
    (Finsupp.sum (M := N) ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2)
      fun (i : ↥S) ↦
      (⇑((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1) :
        (a : N) → R))
    1
⊢ Eq.{u + 1} (α := R)
    ((f : (a : ↥S →₀ N) → R)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2) :
      R)
    (1 : R)

Tactic:
simp_rw [f, Finsupp.coe_lsum]

Premises used: Finsupp.coe_lsum
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
h :
  Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
⊢ Eq.{u + 1} (α := R)
    (Finsupp.sum (M := N) ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2)
      fun (i : ↥S) ↦
      (⇑((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1) :
        (a : N) → R))
    1

Tactic:
rw [Finsupp.sum_fintype _ _ fun _ ↦ map_zero _]

Premises used: Finsupp.sum_fintype, map_zero
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
h :
  ∀ (hS : Eq.{u + 1} (α := R) (1 : R) ((e : (a : M ⊗[R] N) → R) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) : R)),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₁ :
  ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ x ∈ S, (e : (a : M ⊗[R] N) → R) (x.1 ⊗ₜ[R] x.2))),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₂ :
  ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ i : ↥S, (e : (a : M ⊗[R] N) → R) ((↑i : M × N).1 ⊗ₜ[R] (↑i : M × N).2))),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₃ h₄ h₅ h₆ :
  ∀ (hS : Eq.{u + 1} (α := R) (∑ i : ↥S, (e : (a : M ⊗[R] N) → R) ((↑i : M × N).1 ⊗ₜ[R] (↑i : M × N).2)) 1),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
⊢ Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1

Tactic:
rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS

Premises used: LinearEquiv.symm_apply_eq, map_sum, eq_comm, Finset.sum_coe_sort
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
⊢ Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)

Tactic:
have : Function.Surjective f := by
    rw [← LinearMap.range_eq_top, Ideal.eq_top_iff_one]
    use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2
    simp_rw [f, Finsupp.coe_lsum]
    rw [Finsupp.sum_fintype _ _ fun _ ↦ map_zero _]
    rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
-- Module: Mathlib.RingTheory.PicardGroup
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
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
have : ∀ (g : R →ₗ[R] ↥S →₀ N) (hg : f ∘ₗ g = LinearMap.id), Module.Finite R M ∧ Projective R M
⊢ Module.Finite R M ∧ Projective R M

Tactic:
have ⟨g, hg⟩ := projective_lifting_property f .id this