awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
B : Type u_8
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
M : Pic R
⊢ Eq.{u_8 + 1} (α := Pic B)
    (((mapAlgebra A B : MonoidHom.{u_7, u_8} (Pic A) (Pic B)) : (a : Pic A) → Pic B)
        (((mapAlgebra R A : MonoidHom.{u, u_7} (Pic R) (Pic A)) : (a : Pic R) → Pic A) M) :
      Pic B)
    (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) M : Pic B)

Tactic:
mk_eq_mk_iff.mpr ⟨AlgebraTensorModule.congr (.refl ..) (mk.linearEquiv ..) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange ..⟩

Premises used: Iff.mpr, TensorProduct.AlgebraTensorModule.cancelBaseChange, CommRing.Pic.mk_eq_mk_iff, CommRing.Pic.mk.linearEquiv, Nonempty.intro, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, LinearEquiv.trans, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
B : Type u_8
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
h :
  ∀ (x : Pic R),
    Eq.{u_8 + 1} (α := Pic B)
      (((MonoidHom.comp (N := Pic A) (mapAlgebra A B) (mapAlgebra R A) : MonoidHom.{u, u_8} (Pic R) (Pic B)) :
            (a : Pic R) → Pic B)
          x :
        Pic B)
      (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) x : Pic B)
⊢ Eq (α := MonoidHom.{u, u_8} (Pic R) (Pic B)) (MonoidHom.comp (N := Pic A) (mapAlgebra A B) (mapAlgebra R A))
    (mapAlgebra R B)

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
B : Type u_8
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : Pic R
h :
  Eq.{u_8 + 1} (α := Pic B)
    (((mapAlgebra A B : MonoidHom.{u_7, u_8} (Pic A) (Pic B)) : (a : Pic A) → Pic B)
        (((mapAlgebra R A : MonoidHom.{u, u_7} (Pic R) (Pic A)) : (a : Pic R) → Pic A) x) :
      Pic B)
    (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) x : Pic B)
h₁ h₂ :
  Eq.{u_8 + 1} (α := Pic B) (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) x : Pic B)
    (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) x : Pic B)
⊢ Eq.{u_8 + 1} (α := Pic B)
    (((MonoidHom.comp (N := Pic A) (mapAlgebra A B) (mapAlgebra R A) : MonoidHom.{u, u_8} (Pic R) (Pic B)) :
          (a : Pic R) → Pic B)
        x :
      Pic B)
    (((mapAlgebra R B : MonoidHom.{u, u_8} (Pic R) (Pic B)) : (a : Pic R) → Pic B) x : Pic B)

Tactic:
rw [MonoidHom.comp_apply, mapAlgebra_mapAlgebra]

Premises used: CommRing.Pic.mapAlgebra_mapAlgebra, MonoidHom.comp_apply
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
⊢ (mapAlgebra R R : (a : Pic R) → Pic R) M = M

Tactic:
mk_eq_iff.mpr ⟨TensorProduct.lid ..⟩

Premises used: Iff.mpr, CommRing.Pic.mk_eq_iff, Nonempty.intro, TensorProduct.lid, CommRing.Pic.mk
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
h :
  ∀ (x : Pic R),
    Eq (α := Pic R) ((mapAlgebra R R : (a : Pic R) → Pic R) x : Pic R)
      ((MonoidHom.id (Pic R) : (a : Pic R) → Pic R) x : Pic R)
⊢ Eq (α := Pic R →* Pic R) (mapAlgebra R R) (MonoidHom.id (Pic R))

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
x : Pic R
⊢ Eq (α := Pic R) ((mapAlgebra R R : (a : Pic R) → Pic R) x : Pic R)
    ((MonoidHom.id (Pic R) : (a : Pic R) → Pic R) x : Pic R)

Tactic:
mapAlgebra_self_apply

Premises used: CommRing.Pic.mapAlgebra_self_apply
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
x : Pic R
⊢ Eq (α := Pic R) ((mapAlgebra R R : (a : Pic R) → Pic R) x : Pic R)
    ((MonoidHom.id (Pic R) : (a : Pic R) → Pic R) x : Pic R)

Tactic:
exact mapAlgebra_self_apply

Premises used: CommRing.Pic.mapAlgebra_self_apply
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
inst_1 : CommSemiring A
inst_2 : Algebra R A
rw : Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapAlgebra R A) (mapAlgebra R A)
rw₁ rw₂ : Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapAlgebra R A) (mapAlgebra R A)
⊢ Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapRingHom (algebraMap R A)) (mapAlgebra R A)

Tactic:
rw [mapRingHom, toAlgebra_algebraMap]

Premises used: CommRing.Pic.mapRingHom, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
S : Type u_9
T : Type u_10
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : R →+* S
g : S →+* T
M : Pic R
⊢ Eq.{u_10 + 1} (α := Pic T) ((mapRingHom g : (a : Pic S) → Pic T) ((mapRingHom f : (a : Pic R) → Pic S) M) : Pic T)
    ((mapRingHom (g.comp f) : (a : Pic R) → Pic T) M : Pic T)

Tactic:
congr($mapRingHom_comp_mapRingHom M)

Premises used: congrArg, id, CommRing.Pic.mapRingHom_comp_mapRingHom, DFunLike.coe
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Pic R →* Pic R) (mapAlgebra R R) (MonoidHom.id (Pic R))
rw₁ rw₂ : Eq.{u + 1} (α := Pic R →* Pic R) (MonoidHom.id (Pic R)) (MonoidHom.id (Pic R))
⊢ Eq (α := Pic R →* Pic R) (mapRingHom (RingHom.id R)) (MonoidHom.id (Pic R))

Tactic:
rw [mapRingHom, mapAlgebra_self]

Premises used: CommRing.Pic.mapAlgebra_self, CommRing.Pic.mapRingHom
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
⊢ (mapRingHom (RingHom.id R) : (a : Pic R) → Pic R) M = M

Tactic:
congr($mapRingHom_id M)

Premises used: congrArg, id, CommRing.Pic.mapRingHom_id, DFunLike.coe
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Subsingleton.{u_7 + 1} (Pic A)
⊢ Eq (α := Subgroup (Pic R)) (relPic R A) ⊤

Tactic:
top_unique fun _ _ ↦ Subsingleton.elim ..

Premises used: top_unique, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, CommRing.Pic.mapAlgebra
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
⊢ Eq (α := M ⊗[R] M ≃ₗ[R] M ⊗[R] M) (TensorProduct.comm R M M) (LinearEquiv.refl R (M ⊗[R] M))

Tactic:
LinearEquiv.toLinearMap_injective <| LinearMap.eq_of_localization_maximal _ ff _ ff _ _
    fun P _ ↦ .trans (b := (TensorProduct.comm ..).toLinearMap) ?_ ?_

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.eq_of_localization_maximal, Eq.trans
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
x x_1 : M
⊢ Eq (α := LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (((((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
                  (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
                    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
                      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
                (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
                  LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
                    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
              (↑(TensorProduct.comm R M M) : M ⊗[R] M →ₗ[R] M ⊗[R] M) :
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
          (a : LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) →
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
        (((ff P : M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
            (a : M ⊗[R] M) → LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
          (x ⊗ₜ[R] x_1)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    ((TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M) :
          (a : LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) →
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
        (((ff P : M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
            (a : M ⊗[R] M) → LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
          (x ⊗ₜ[R] x_1)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)

Tactic:
apply IsLocalizedModule.map_apply

Premises used: IsLocalizedModule.map_apply
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
refine_2 :
  ∀ (e : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp),
    Eq (α :=
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
            (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
                LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
          (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
        (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))
⊢ Eq (α :=
    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
          (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
        (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))

Tactic:
have ⟨e⟩ := free_iff_linearEquiv.mp (inferInstance : Free Rp (LocalizedModule P.primeCompl M))
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
refine_2 :
  ∀ (e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp),
    Eq (α :=
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
            (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
                LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
          (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
        (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))
⊢ Eq (α :=
    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
          (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
        (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))

Tactic:
have e := e.restrictScalars R
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e_1 : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
rw :
  ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
    Rp ⊗[Rp] Rp)
| ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
    Rp ⊗[Rp] Rp)

Tactic:
rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul, mul_comm, smul_eq_mul, mul_one, DFunLike.coe
-- 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
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e_1 : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
conv_lhs :
  Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
refine_2 :
  Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
⊢ Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)

Tactic:
conv_lhs => rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul, mul_comm, smul_eq_mul, mul_one, DFunLike.coe
-- 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
m₁ m₂ : M
⊢ Eq (α := M ⊗[R] M) (m₁ ⊗ₜ[R] m₂) (m₂ ⊗ₜ[R] m₁)

Tactic:
DFunLike.congr_fun (tensorProductComm_eq_refl ..) (m₂ ⊗ₜ m₁)

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, Module.Invertible.tensorProductComm_eq_refl, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
obtain :
  ∀ (T T' : Finset A) (hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A))
    (hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A))
    (one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
    Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
      (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.inv_mul ▸ one_le.mp le_rfl)

Premises used: Submodule.mem_span_mul_finite_of_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
⊢ ∃ (f : A → R),
    Function.support f ⊆ (↑(Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T') : Set A) ∧
      Eq (α := A) (∑ a ∈ Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T', f a • a) 1

Tactic:
rw [← Set.image2_mul, ← Finset.coe_image₂, mem_span_finset] at one_mem

Premises used: Submodule.mem_span_finset, Set.image2_mul, Finset.coe_image₂
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
one_mem :
  ∃ (f : A → R),
    Function.support f ⊆ (↑(Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T') : Set A) ∧
      Eq (α := A) (∑ a ∈ Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T', f a • a) 1
⊢ let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∃ (f : A → R), Function.support f ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, f a • a) 1

Tactic:
set S := T.image₂ (· * ·) T'

Premises used: HMul.hMul, Finset.image₂
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T'
one_mem : ∃ (f : A → R), Function.support f ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, f a • a) 1
obtain :
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
    Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
      (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
obtain ⟨r, hr⟩ := one_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1
choose :
  ∀ (a : (i : ↥S) → A) (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T')
    (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
    Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
      (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
choose a ha b hb eq using fun i : S ↦ Finset.mem_image₂.mp i.2

Premises used: Finset.mem_image₂, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1
a : (i : ↥S) → A
ha : ∀ (i : ↥S), a i ∈ T
b : (i : ↥S) → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = (↑i : A)
i : ↥S
x : A
hx : x ∈ (↑I : Submodule R A)
rw :
  Membership.mem (α := A) ((↑I : Submodule R A) * (↑I⁻¹ : Submodule R A))
    ((LinearMap.mulRight R (r (↑i : A) • a i) : (a : A) → A) x : A)
⊢ Membership.mem (α := A) (γ := Submodule R A) (range (Algebra.linearMap R A))
    ((LinearMap.mulRight R (r (↑i : A) • a i) : (a : A) → A) x : A)

Tactic:
rw [← one_eq_range, ← I.mul_inv]

Premises used: Units.mul_inv, Submodule.one_eq_range