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
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 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
h :
  Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
    (⇑((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
    (⇑((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
          LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
      (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
⊢ Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
    (Function.comp (β := ↥(I * submoduleAlgebra e))
      (⇑(I * submoduleAlgebra e).subtype : (a : ↥(I * submoduleAlgebra e)) → A)
      (⇑(I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → ↥(I * submoduleAlgebra e)))
    (Function.comp (β := A ⊗[R] ↥(submoduleAlgebra e))
      (⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
      (⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
        (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A ⊗[R] ↥(submoduleAlgebra e)))

Tactic:
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]

Premises used: LinearMap.coe_comp, LinearEquiv.coe_toLinearMap
-- 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 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
h :
  (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
    (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype
⊢ Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
    (⇑((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
    (⇑((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
          LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
      (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)

Tactic:
congr 1
-- 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 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
h :
  ∀ (x : ↥I) (x_1 : ↥(submoduleAlgebra e)),
    Eq (α := A)
      (((((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) :
                    ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                  (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
                x :
              ↥(submoduleAlgebra e) →ₗ[R] A) :
            (a : ↥(submoduleAlgebra e)) → A)
          x_1 :
        A)
      (((((AlgebraTensorModule.curry
                      ((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
                          A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
                        LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
                    ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                  (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
                x :
              ↥(submoduleAlgebra e) →ₗ[R] A) :
            (a : ↥(submoduleAlgebra e)) → A)
          x_1 :
        A)
⊢ (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
    (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype

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
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 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
x : ↥I
x_1 : ↥(submoduleAlgebra e)
⊢ Eq (α := A)
    (((((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) :
                  ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
                        A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
                      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
                  ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
h :
  ∀ (M : Pic R),
    Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M ↔
      Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
⊢ Eq (α := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) (relPic R A)

Tactic:
ext M
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h :
  Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M →
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
h₁ :
  Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M →
    Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M ↔
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M

Tactic:
constructor
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
h₁ :
  ∀ (I : (Submodule R A)ˣ),
    Membership.mem (α := Pic R) (γ := Subgroup (Pic R)) (relPic R A)
      (((unitsToPic R A : MonoidHom.{u_4, u} (Submodule R A)ˣ (Pic R)) : (a : (Submodule R A)ˣ) → Pic R) I : Pic R)
⊢ Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M

Tactic:
obtain ⟨I, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ Membership.mem (α := Pic R) (γ := Subgroup (Pic R)) (relPic R A)
    (((unitsToPic R A : MonoidHom.{u_4, u} (Submodule R A)ˣ (Pic R)) : (a : (Submodule R A)ˣ) → Pic R) I : Pic R)

Tactic:
mk_eq_one_iff.mpr ⟨AlgebraTensorModule.congr (.refl ..) (unitsToPicEquiv I) ≪≫ₗ
      .ofBijective ((Algebra.TensorProduct.lmul'' R).toLinearMap ∘ₗ AlgebraTensorModule.lTensor A A
        I.1.subtype) (projective_units_and_mul'_comp_lTensor_bijective I).2⟩

Premises used: Iff.mpr, AlgHom.toLinearMap, Units.val, Set.Mem, setOf, CommRing.Pic.mk_eq_one_iff, _private.0.Submodule.projective_units_and_mul'_comp_lTensor_bijective, Nonempty.intro, TensorProduct.AlgebraTensorModule.congr, LinearMap.comp, Submodule.unitsToPicEquiv, And.right, Set.preimage, Algebra.TensorProduct.lmul'', Set.singleton, Submodule.subtype, LinearEquiv.refl, LinearEquiv.trans, DFunLike.coe, LinearEquiv.ofBijective, CommRing.Pic.mk, TensorProduct.AlgebraTensorModule.lTensor
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ Membership.mem (α := Pic R) (γ := Subgroup (Pic R)) (relPic R A)
    (((unitsToPic R A : MonoidHom.{u_4, u} (Submodule R A)ˣ (Pic R)) : (a : (Submodule R A)ˣ) → Pic R) I : Pic R)

Tactic:
exact mk_eq_one_iff.mpr ⟨AlgebraTensorModule.congr (.refl ..) (unitsToPicEquiv I) ≪≫ₗ
      .ofBijective ((Algebra.TensorProduct.lmul'' R).toLinearMap ∘ₗ AlgebraTensorModule.lTensor A A
        I.1.subtype) (projective_units_and_mul'_comp_lTensor_bijective I).2⟩

Premises used: Iff.mpr, AlgHom.toLinearMap, Units.val, CommRing.Pic.mk_eq_one_iff, _private.0.Submodule.projective_units_and_mul'_comp_lTensor_bijective, Nonempty.intro, TensorProduct.AlgebraTensorModule.congr, LinearMap.comp, Submodule.unitsToPicEquiv, And.right, Algebra.TensorProduct.lmul'', Submodule.subtype, LinearEquiv.refl, LinearEquiv.trans, DFunLike.coe, LinearEquiv.ofBijective, TensorProduct.AlgebraTensorModule.lTensor
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
h₁ :
  ∀ (f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A),
    Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M

Tactic:
have f := (mk_eq_one_iff.mp (inv_mem h)).some
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M

Tactic:
⟨(isUnit_of_mul_isUnit_left (x := submoduleAlgebra e) (y := submoduleAlgebra f) ?_).unit,
    mk_eq_iff.mpr ⟨submoduleAlgebraEquiv e⟩⟩

Premises used: Iff.mpr, Set.Mem, setOf, CommRing.Pic.mk_eq_iff, Module.Flat.submoduleAlgebraEquiv, isUnit_of_mul_isUnit_left, Nonempty.intro, Exists.intro, IsUnit.unit, Set.range
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
h₁ : IsUnit (submoduleAlgebra e * submoduleAlgebra f)
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M

Tactic:
refine ⟨(isUnit_of_mul_isUnit_left (x := submoduleAlgebra e) (y := submoduleAlgebra f) ?_).unit,
    mk_eq_iff.mpr ⟨submoduleAlgebraEquiv e⟩⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
simp_rw : HMul.hMul (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R M⁻¹.AsModule) = 1
simp_rw₁ : M * M⁻¹ = 1
⊢ Eq (α := Pic R) (Pic.mk R (M.AsModule ⊗[R] M⁻¹.AsModule)) 1

Tactic:
simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]

Premises used: CommRing.Pic.mk_tensor, CommRing.Pic.mk_eq_self, mul_inv_cancel
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A)

Tactic:
have := eq_span_singleton_of_surjective <| LinearEquiv.surjective <|
    (congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ
    (mk_eq_one_iff.mp <| by simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]).some).symm ≪≫ₗ
    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A)
h₁ :
  IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A)
⊢ ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))

Tactic:
apply_fun (⊤ * ·) at this

Premises used: HMul.hMul, Top.top
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
⊢ ⊤ =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))

Tactic:
simp_rw [← mul_assoc, top_mul_submoduleAlgebra] at this

Premises used: mul_assoc, Module.Flat.top_mul_submoduleAlgebra
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
h₁ :
  ∀ (a : A)
    (eq :
      a *
          (↑(((↑(LinearEquiv.symm
                          (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                        tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                    R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                  (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
                1) :
            A) =
        1),
    IsUnit (M := Submodule R A)
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))

Tactic:
obtain ⟨a, -, eq⟩ := mem_mul_span_singleton.mp (this ▸ mem_top (x := 1))

Premises used: Submodule.mem_mul_span_singleton, Iff.mp
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
a : A
eq :
  a *
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A) =
    1
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))

Tactic:
.map (spanSingleton R).toMonoidHom (.of_mul_eq_one_right _ eq)

Premises used: Set.Mem, setOf, Submodule.spanSingleton, IsUnit.of_mul_eq_one_right, MonoidWithZeroHom.toMonoidHom, Set.singleton, Submodule.span, IsUnit.map
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
a : A
eq :
  a *
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A) =
    1
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))

Tactic:
exact .map (spanSingleton R).toMonoidHom (.of_mul_eq_one_right _ eq)
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ Function.MulExact.{u_4, u, u_4} (M := (Submodule R A)ˣ) (N := Pic R) (P := Pic A)
    (⇑(unitsToPic R A) : (a : (Submodule R A)ˣ) → Pic R) (⇑(mapAlgebra R A) : (a : Pic R) → Pic A)

Tactic:
MonoidHom.mulExact_iff.mpr (range_unitsToPic R A).symm

Premises used: Iff.mpr, Submodule.range_unitsToPic, Eq.symm, MonoidHom.mulExact_iff
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M
inst_6 : Module R_1 N
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
inst_9 : CommSemiring A
inst_10 : Algebra R_1 A
inst_11 : FaithfulSMul R_1 A
R : Type u_5
inst_12 : CommRing R
inst_13 : IsDomain R
inst_14 : Nonempty.{u_5 + 1} (NormalizedGCDMonoid R)
⊢ Subsingleton.{u_5 + 1} (Pic R)

Tactic:
Equiv.subsingleton (ClassGroup.equivPic R).toEquiv.symm

Premises used: MulEquiv.toEquiv, ClassGroup.equivPic, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Invertible R M
inst_4 : Subsingleton.{u_5 + 1} (Pic (FractionRing R))
⊢ ∃ (I : Ideal R), Nonempty (M ≃ₗ[R] ↥I)

Tactic:
have : Pic.mk R M ∈ relPic R (FractionRing R) := Subsingleton.elim ..
  have ⟨I, eq⟩ := Submodule.range_unitsToPic R (FractionRing R) ▸ this
  have ⟨e⟩ := mk_eq_mk_iff.mp eq.symm
  ⟨_, ⟨e ≪≫ₗ FractionalIdeal.equivNumOfIsLocalization
    ⟨_, I.submodule_isFractional (S := nonZeroDivisors R)⟩⟩⟩

Premises used: FractionRing, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, CommRing.Pic.mk, CommRing.Pic.mapAlgebra