awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M_2 : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M_2
inst_10 : Module R M_2
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M_2
inst_14 : Module.Invertible R N
M : (Skeleton (SemimoduleCat R))ˣ
this : {M N : Skeleton (SemimoduleCat R)} → M = N → (↑(Quotient.out M) : Type u) ≃ₗ[R] (↑(Quotient.out N) : Type u)
⊢ (↑((Equiv.symm (equivShrink (Skeleton (SemimoduleCat R))ˣ) :
            (a : Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ) → (Skeleton (SemimoduleCat R))ˣ)
          (id
              ((equivShrink (Skeleton (SemimoduleCat R))ˣ :
                  (a : (Skeleton (SemimoduleCat R))ˣ) → Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ)
                M) :
            Pic R)) :
      Skeleton (SemimoduleCat R)) =
    (↑M : Skeleton (SemimoduleCat R))

Tactic:
simp
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
rw :
  Eq (α := Skeleton (SemimoduleCat R))
    (toSkeleton
      (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Dual R M'))
        (SemimoduleCat.of R M')))
    1
⊢ HMul.hMul (α := Skeleton (SemimoduleCat R)) ⟦SemimoduleCat.of R M'⟧ ⟦SemimoduleCat.of R (Dual R M')⟧ = 1

Tactic:
rw [← toSkeleton, ← toSkeleton, mul_comm, ← Skeleton.toSkeleton_tensorObj]

Premises used: CategoryTheory.toSkeleton, CategoryTheory.Skeleton.toSkeleton_tensorObj, mul_comm
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ Eq (α := Skeleton (SemimoduleCat R))
    (toSkeleton
      (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Dual R M'))
        (SemimoduleCat.of R M')))
    1

Tactic:
Quotient.sound ⟨(Invertible.linearEquiv R _).toModuleIsoₛ⟩

Premises used: Nonempty.intro, CategoryTheory.InducedCategory, LinearEquiv.toModuleIsoₛ, Quotient.sound, Module.Invertible.linearEquiv, CategoryTheory.Skeleton
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ Eq (α := Skeleton (SemimoduleCat R))
    (toSkeleton
      (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Dual R M'))
        (SemimoduleCat.of R M')))
    1

Tactic:
exact Quotient.sound ⟨(Invertible.linearEquiv R _).toModuleIsoₛ⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
⊢ Pic.mk R M.AsModule = M

Tactic:
mk_eq_iff.mpr ⟨.refl ..⟩

Premises used: Iff.mpr, CommRing.Pic.mk_eq_iff, Nonempty.intro, LinearEquiv.refl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M N : Pic R
rw : M = N ↔ Pic.mk R M.AsModule = N
rw₁ rw₂ : M = N ↔ M = N
⊢ M = N ↔ Nonempty.{u + 1} (M.AsModule ≃ₗ[R] N.AsModule)

Tactic:
rw [← mk_eq_iff, mk_eq_self]

Premises used: CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
⊢ Eq (α := Pic R) (Pic.mk R M) (Pic.mk R N) ↔ Nonempty (M ≃ₗ[R] N)

Tactic:
let eN := mk.linearEquiv R N
  mk_eq_iff.trans ⟨fun ⟨e⟩ ↦ ⟨e ≪≫ₗ eN⟩, fun ⟨e⟩ ↦ ⟨e ≪≫ₗ eN.symm⟩⟩

Premises used: LinearEquiv.symm, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk.linearEquiv, _private.0.CommRing.Pic.mk_eq_mk_iff.match_2, Nonempty.intro, CommRing.Pic.AsModule, LinearEquiv, Iff.intro, Iff.trans, Nonempty, RingHom.id, LinearEquiv.trans, _private.0.CommRing.Pic.mk_eq_mk_iff.match_1, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Pic R) (Pic.mk R R) 1

Tactic:
congr_arg (equivShrink _) <| Units.ext <| Quotient.sound ⟨(Finite.reprEquivₛ R R).toModuleIsoₛ⟩

Premises used: Module.Finite.reprEquivₛ, Units.ext, Nonempty.intro, congr_arg, CommRing.Pic, LinearEquiv.toModuleIsoₛ, Quotient.sound, equivShrink, DFunLike.coe, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
rw : Eq (α := Pic R) (Pic.mk R M) (Pic.mk R R) ↔ Nonempty (M ≃ₗ[R] R)
rw₁ rw₂ : Nonempty (M ≃ₗ[R] R) ↔ Nonempty (M ≃ₗ[R] R)
⊢ Eq (α := Pic R) (Pic.mk R M) 1 ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
rw [← mk_self, mk_eq_mk_iff]

Premises used: CommRing.Pic.mk_eq_mk_iff, CommRing.Pic.mk_self
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
⊢ Eq (α := Pic R) (Pic.mk R M) 1 ↔ Free R M

Tactic:
mk_eq_one_iff.trans Invertible.free_iff_linearEquiv.symm

Premises used: Module.Invertible.free_iff_linearEquiv, CommRing.Pic.mk_eq_one_iff, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
inst_4 : Free R M
⊢ Eq (α := Pic R) (Pic.mk R M) 1

Tactic:
mk_eq_one_iff_free.mpr ‹_›

Premises used: Iff.mpr, CommRing.Pic.mk_eq_one_iff_free
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
⊢ Free R (AsModule (R := R) 1)

Tactic:
mk_eq_one_iff_free.mp mk_eq_self

Premises used: CommRing.Pic.mk_eq_self, CommRing.Pic.mk_eq_one_iff_free, Iff.mp
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
simp_rw :
  (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) :
      Skeleton (SemimoduleCat R)) =
    (↑(HMul.hMul (α := (Skeleton (SemimoduleCat R))ˣ)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
            ⋯)) :
      Skeleton (SemimoduleCat R))
⊢ (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) :
      Skeleton (SemimoduleCat R)) =
    (↑(HMul.hMul (α := (Skeleton (SemimoduleCat R))ˣ) (β := (Skeleton (SemimoduleCat R))ˣ)
          ((Equiv.symm (equivShrink (Skeleton (SemimoduleCat R))ˣ) :
                (a : Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ) → (Skeleton (SemimoduleCat R))ˣ)
              (Pic.mk R M) :
            (Skeleton (SemimoduleCat R))ˣ)
          ((Equiv.symm (equivShrink (Skeleton (SemimoduleCat R))ˣ) :
                (a : Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ) → (Skeleton (SemimoduleCat R))ˣ)
              (Pic.mk R N) :
            (Skeleton (SemimoduleCat R))ˣ)) :
      Skeleton (SemimoduleCat R))

Tactic:
simp_rw [Pic.mk, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
⊢ (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) :
      Skeleton (SemimoduleCat R)) =
    (↑(HMul.hMul (α := (Skeleton (SemimoduleCat R))ˣ)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
            ⋯)) :
      Skeleton (SemimoduleCat R))

Tactic:
(Quotient.sound ?_).trans (Skeleton.toSkeleton_tensorObj ..)

Premises used: CategoryTheory.Skeleton.toSkeleton_tensorObj, CategoryTheory.InducedCategory, Quotient.sound, Eq.trans, CategoryTheory.Skeleton
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
refine :
  HasEquiv.Equiv (α := SemimoduleCat R) (SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N)))
    (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Finite.reprₛ R M))
      (SemimoduleCat.of R (Finite.reprₛ R N)))
⊢ (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) :
      Skeleton (SemimoduleCat R)) =
    (↑(HMul.hMul (α := (Skeleton (SemimoduleCat R))ˣ)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)
          (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
            ⋯)) :
      Skeleton (SemimoduleCat R))

Tactic:
refine (Quotient.sound ?_).trans (Skeleton.toSkeleton_tensorObj ..)

Premises used: CategoryTheory.Skeleton.toSkeleton_tensorObj, Quotient.sound, Eq.trans
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
⊢ HasEquiv.Equiv (α := SemimoduleCat R) (SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N)))
    (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Finite.reprₛ R M))
      (SemimoduleCat.of R (Finite.reprₛ R N)))

Tactic:
⟨(Finite.reprEquivₛ R _ ≪≫ₗ TensorProduct.congr
      (Finite.reprEquivₛ R M).symm (Finite.reprEquivₛ R N).symm).toModuleIsoₛ⟩

Premises used: LinearEquiv.symm, Module.Finite.reprEquivₛ, CategoryTheory.IsIsomorphic, TensorProduct.congr, Nonempty.intro, LinearEquiv.toModuleIsoₛ, LinearEquiv.trans
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
⊢ HasEquiv.Equiv (α := SemimoduleCat R) (SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N)))
    (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Finite.reprₛ R M))
      (SemimoduleCat.of R (Finite.reprₛ R N)))

Tactic:
exact ⟨(Finite.reprEquivₛ R _ ≪≫ₗ TensorProduct.congr
      (Finite.reprEquivₛ R M).symm (Finite.reprEquivₛ R N).symm).toModuleIsoₛ⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
rw :
  Eq (α := Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) :
      Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)⁻¹ :
      Skeleton (SemimoduleCat R))
⊢ Eq (α := Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) :
      Skeleton (SemimoduleCat R))
    (↑((Equiv.symm (equivShrink (Skeleton (SemimoduleCat R))ˣ) :
              (a : Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ) → (Skeleton (SemimoduleCat R))ˣ)
            (Pic.mk R M))⁻¹ :
      Skeleton (SemimoduleCat R))

Tactic:
rw [Pic.mk, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
⊢ Eq (α := Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) :
      Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)⁻¹ :
      Skeleton (SemimoduleCat R))

Tactic:
Quotient.sound ⟨(Finite.reprEquivₛ R _ ≪≫ₗ (Finite.reprEquivₛ R _).dualMap).toModuleIsoₛ⟩

Premises used: Module.Finite.reprEquivₛ, Nonempty.intro, CategoryTheory.InducedCategory, LinearEquiv.dualMap, LinearEquiv.toModuleIsoₛ, Quotient.sound, LinearEquiv.trans, CategoryTheory.Skeleton
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
⊢ Eq (α := Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
          ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) :
      Skeleton (SemimoduleCat R))
    (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
            ⋯)⁻¹ :
      Skeleton (SemimoduleCat R))

Tactic:
exact Quotient.sound ⟨(Finite.reprEquivₛ R _ ≪≫ₗ (Finite.reprEquivₛ R _).dualMap).toModuleIsoₛ⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
rw : M⁻¹ = (Pic.mk R M.AsModule)⁻¹
rw₁ rw₂ : M⁻¹ = M⁻¹
⊢ M⁻¹ = Pic.mk R (Dual R M.AsModule)

Tactic:
rw [mk_dual, mk_eq_self]

Premises used: CommRing.Pic.mk_dual, CommRing.Pic.mk_eq_self
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M N : Pic R
rw : M * N = HMul.hMul (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R N.AsModule)
rw₁ : M * N = M * Pic.mk R N.AsModule
rw₂ rw₃ : M * N = M * N
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)

Tactic:
rw [mk_tensor, mk_eq_self, mk_eq_self]

Premises used: CommRing.Pic.mk_tensor, CommRing.Pic.mk_eq_self
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
h : ∀ (a : Type u) (b : AddCommMonoid a) (c : Module R a) (d : Module.Invertible R a), Eq (α := Pic R) (Pic.mk R a) 1
M N : Pic R
rw : Pic.mk R M.AsModule = N
rw₁ : Eq (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R N.AsModule)
rw₂ : Eq (α := Pic R) 1 (Pic.mk R N.AsModule)
rw₃ rw₄ : Eq.{u + 1} (α := Pic R) 1 1
⊢ M = N

Tactic:
rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]

Premises used: CommRing.Pic.mk_eq_self
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommRing R
⊢ Subsingleton.{u + 1} (Pic R) ↔
    ∀ (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M], Module.Invertible R M → Free R M

Tactic:
subsingleton_iffₛ.trans
    ⟨fun h M ↦ h M, fun h M ↦ let _ := @Module.addCommMonoidToAddCommGroup R; h M⟩

Premises used: Module.addCommMonoidToAddCommGroup, Iff.intro, Iff.trans, CommRing.Pic.subsingleton_iffₛ
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
inst_15 : Subsingleton.{u + 1} (Pic R)
⊢ Free R M

Tactic:
have := subsingleton_iffₛ.mp ‹_› (Finite.reprₛ R M) inferInstance
  .of_equiv (Finite.reprEquivₛ R M)

Premises used: Module.Finite.reprEquivₛ, inferInstance, Module.Free.of_equiv, Iff.mp, CommRing.Pic.subsingleton_iffₛ, Module.Finite.reprₛ
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M_1
inst_6 : Module R_1 N_1
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R_1 M
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N
inst_13 : Module.Invertible R_1 M
inst_14 : Module.Invertible R_1 N
R : Type u_7
inst_15 : CommRing R
inst_16 : IsLocalRing R
⊢ Subsingleton.{u_7 + 1} (Pic R)

Tactic:
subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_isLocalRing

Premises used: Iff.mpr, CommRing.Pic.subsingleton_iff, Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M_1
inst_6 : Module R_1 N_1
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R_1 M
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N
inst_13 : Module.Invertible R_1 M
inst_14 : Module.Invertible R_1 N
R : Type u_7
inst_15 : CommRing R
inst_16 : Finite.{u_7 + 1} (MaximalSpectrum R)
⊢ Subsingleton.{u_7 + 1} (Pic R)

Tactic:
subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_finrank_eq _ _ 1
    fun _ ↦ let _ := @Ideal.Quotient.field; Invertible.finrank_eq_one ..

Premises used: MaximalSpectrum.asIdeal, Iff.mpr, Module.free_of_flat_of_finrank_eq, CommRing.Pic.subsingleton_iff, Ideal.Quotient.field, HasQuotient.Quotient, Module.Invertible.finrank_eq_one, TensorProduct, OfNat.ofNat
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A_1 : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
A : Type u_7
B : Type u_8
inst_15 : CommSemiring A
inst_16 : CommSemiring B
inst_17 : Algebra R A
x x_1 : Pic R
rw : Nonempty (A ⊗[R] (x * x_1).AsModule ≃ₗ[A] A ⊗[R] x.AsModule ⊗[A] (A ⊗[R] x_1.AsModule))
⊢ Pic.mk A (A ⊗[R] (x * x_1).AsModule) =
    HMul.hMul (α := Pic A) (Pic.mk A (A ⊗[R] x.AsModule)) (Pic.mk A (A ⊗[R] x_1.AsModule))

Tactic:
rw [← mk_tensor, mk_eq_mk_iff]

Premises used: CommRing.Pic.mk_eq_mk_iff, CommRing.Pic.mk_tensor
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A_1 : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
A : Type u_7
B : Type u_8
inst_15 : CommSemiring A
inst_16 : CommSemiring B
inst_17 : Algebra R A
x x_1 : Pic R
⊢ Nonempty (A ⊗[R] (x * x_1).AsModule ≃ₗ[A] A ⊗[R] x.AsModule ⊗[A] (A ⊗[R] x_1.AsModule))

Tactic:
⟨congr (.refl ..) (.symm (mk_eq_iff.mp ?_).some) ≪≫ₗ distribBaseChange R A ..⟩

Premises used: LinearEquiv.symm, TensorProduct.AlgebraTensorModule.distribBaseChange, CommRing.Pic.mk_eq_iff, Nonempty.some, Nonempty.intro, TensorProduct.AlgebraTensorModule.congr, Iff.mp, LinearEquiv.refl, LinearEquiv.trans
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A_1 : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
A : Type u_7
B : Type u_8
inst_15 : CommSemiring A
inst_16 : CommSemiring B
inst_17 : Algebra R A
x x_1 : Pic R
refine : Pic.mk R (x.AsModule ⊗[R] x_1.AsModule) = x * x_1
⊢ Nonempty (A ⊗[R] (x * x_1).AsModule ≃ₗ[A] A ⊗[R] x.AsModule ⊗[A] (A ⊗[R] x_1.AsModule))

Tactic:
refine ⟨congr (.refl ..) (.symm (mk_eq_iff.mp ?_).some) ≪≫ₗ distribBaseChange R A ..⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A_1 : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N_1
inst_7 : Module R P
inst_8 : Module R Q
M : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M
inst_10 : Module R M
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M
inst_14 : Module.Invertible R N
A : Type u_7
B : Type u_8
inst_15 : CommSemiring A
inst_16 : CommSemiring B
inst_17 : Algebra R A
x x_1 : Pic R
simp_rw : HMul.hMul (α := Pic R) (Pic.mk R x.AsModule) (Pic.mk R x_1.AsModule) = x * x_1
⊢ Pic.mk R (x.AsModule ⊗[R] x_1.AsModule) = x * x_1

Tactic:
simp_rw [mk_tensor, mk_eq_self]

Premises used: CommRing.Pic.mk_tensor, CommRing.Pic.mk_eq_self