awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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))ˣ) (β := (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))
have simp_rw : (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ sorry) :
    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))⟧ sorry)
        (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
          sorry)) :
    Skeleton (SemimoduleCat R))
Tactic: simp_rw [Pic.mk, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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))
have 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)))
Tactic: refine (Quotient.sound ?_).trans (Skeleton.toSkeleton_tensorObj ..)
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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))
    (↑((Equiv.symm (equivShrink (Skeleton (SemimoduleCat R))ˣ) :
              (a : Shrink.{u, u + 1} (Skeleton (SemimoduleCat R))ˣ) → (Skeleton (SemimoduleCat R))ˣ)
            (Pic.mk R M))⁻¹ :
      Skeleton (SemimoduleCat R))
have 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)))⟧ sorry) :
    Skeleton (SemimoduleCat R))
  (↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧ sorry)⁻¹ :
    Skeleton (SemimoduleCat R))
Tactic: rw [Pic.mk, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
⊢ M⁻¹ = Pic.mk R (Dual R M.AsModule)
have rw : M⁻¹ = (Pic.mk R M.AsModule)⁻¹
Tactic: rw [mk_dual, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Pic R
rw : M⁻¹ = (Pic.mk R M.AsModule)⁻¹
⊢ M⁻¹ = Pic.mk R (Dual R M.AsModule)
have rw₁ : M⁻¹ = M⁻¹
Tactic: rw [mk_dual, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : Pic R
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)
have rw : M * N = HMul.hMul (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R N.AsModule)
Tactic: rw [mk_tensor, mk_eq_self, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)
have rw₁ : M * N = M * Pic.mk R N.AsModule
Tactic: rw [mk_tensor, mk_eq_self, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)
have rw₂ : M * N = M * N
Tactic: rw [mk_tensor, mk_eq_self, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ M = N
have rw : Pic.mk R M.AsModule = N
Tactic: rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ M = N
have rw₁ : Eq (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R N.AsModule)
Tactic: rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ M = N
have rw₂ : Eq (α := Pic R) 1 (Pic.mk R N.AsModule)
Tactic: rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ M = N
have rw₃ : Eq.{u + 1} (α := Pic R) 1 1
Tactic: rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ 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))
have rw : Nonempty (A ⊗[R] (x * x_1).AsModule ≃ₗ[A] A ⊗[R] x.AsModule ⊗[A] (A ⊗[R] x_1.AsModule))
Tactic: rw [← mk_tensor, mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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))
have refine : Pic.mk R (x.AsModule ⊗[R] x_1.AsModule) = x * x_1
Tactic: refine ⟨congr (.refl ..) (.symm (mk_eq_iff.mp ?_).some) ≪≫ₗ distribBaseChange R A ..⟩
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Pic.mk R (x.AsModule ⊗[R] x_1.AsModule) = x * x_1
have simp_rw : HMul.hMul (α := Pic R) (Pic.mk R x.AsModule) (Pic.mk R x_1.AsModule) = x * x_1
Tactic: simp_rw [mk_tensor, mk_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Eq (α := MonoidHom.{u, u_8} (Pic R) (Pic B)) (MonoidHom.comp (N := Pic A) (mapAlgebra A B) (mapAlgebra R A))
    (mapAlgebra R B)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ 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)
have 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)
Tactic: rw [MonoidHom.comp_apply, mapAlgebra_mapAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ 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)
have 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)
Tactic: rw [MonoidHom.comp_apply, mapAlgebra_mapAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Pic R →* Pic R) (mapAlgebra R R) (MonoidHom.id (Pic R))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_7
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapRingHom (algebraMap R A)) (mapAlgebra R A)
have rw : Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapAlgebra R A) (mapAlgebra R A)
Tactic: rw [mapRingHom, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapRingHom (algebraMap R A)) (mapAlgebra R A)
have rw₁ : Eq (α := MonoidHom.{u, u_7} (Pic R) (Pic A)) (mapAlgebra R A) (mapAlgebra R A)
Tactic: rw [mapRingHom, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Pic R →* Pic R) (mapRingHom (RingHom.id R)) (MonoidHom.id (Pic R))
have rw : Eq (α := Pic R →* Pic R) (mapAlgebra R R) (MonoidHom.id (Pic R))
Tactic: rw [mapRingHom, mapAlgebra_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Pic R →* Pic R) (mapAlgebra R R) (MonoidHom.id (Pic R))
⊢ Eq (α := Pic R →* Pic R) (mapRingHom (RingHom.id R)) (MonoidHom.id (Pic R))
have rw₁ : Eq.{u + 1} (α := Pic R →* Pic R) (MonoidHom.id (Pic R)) (MonoidHom.id (Pic R))
Tactic: rw [mapRingHom, mapAlgebra_self]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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))
have refine_1 : ∀ (P : Ideal R) (x : P.IsMaximal),
  Eq (α :=
    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)
        (↑(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)
    ((↑(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) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
Tactic: refine LinearEquiv.toLinearMap_injective <| LinearMap.eq_of_localization_maximal _ ff _ ff _ _
    fun P _ ↦ .trans (b := (TensorProduct.comm ..).toLinearMap) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
refine_1 :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    Eq (α :=
      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)
          (↑(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)
      ((↑(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) :
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
⊢ Eq (α := M ⊗[R] M ≃ₗ[R] M ⊗[R] M) (TensorProduct.comm R M M) (LinearEquiv.refl R (M ⊗[R] M))
have refine_2 : ∀ (P : Ideal R) (x : P.IsMaximal),
  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: refine LinearEquiv.toLinearMap_injective <| LinearMap.eq_of_localization_maximal _ ff _ ff _ _
    fun P _ ↦ .trans (b := (TensorProduct.comm ..).toLinearMap) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ 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))
have 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))
Tactic: have ⟨e⟩ := free_iff_linearEquiv.mp (inferInstance : Free Rp (LocalizedModule P.primeCompl M))