awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
rw : Eq (α := A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] ↥(↑I : Submodule R A)) (lTensor A (g ∘ₗ f)) LinearMap.id
rw₁ : Eq (α := A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] ↥(↑I : Submodule R A)) (lTensor A LinearMap.id) LinearMap.id
rw₂ rw₃ : Eq.{u_4 + 1} (α := A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] ↥(↑I : Submodule R A)) LinearMap.id LinearMap.id
⊢ Eq (α := A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] ↥(↑I : Submodule R A)) (lTensor A g ∘ₗ lTensor A f) LinearMap.id

Tactic:
rw [← lTensor_comp, hgf, lTensor_id]

Premises used: LinearMap.lTensor_id, LinearMap.lTensor_comp
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A ⊗[R] (↥S → R))
      (⇑(piScalarRight R R A ↥S : A ⊗[R] (↥S → R) ≃ₗ[R] ↥S → A) : (a : A ⊗[R] (↥S → R)) → ↥S → A)
      (⇑(lTensor A f) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A ⊗[R] (↥S → R)))

Tactic:
have := (piScalarRight R R A S).injective.comp <| injective_of_comp_eq_id
    (f.lTensor A) (g.lTensor A) <| by rw [← lTensor_comp, hgf, lTensor_id]
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
this :
  Function.Injective.{u_4 + 1, u_4 + 1} (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A ⊗[R] (↥S → R))
      (⇑(piScalarRight R R A ↥S : A ⊗[R] (↥S → R) ≃ₗ[R] ↥S → A) : (a : A ⊗[R] (↥S → R)) → ↥S → A)
      (⇑(lTensor A f) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A ⊗[R] (↥S → R)))
⊢ Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A)
      (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
        (a : A) → (i : ↥S) → A)
      (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A))

Tactic:
rw [← LinearEquiv.coe_toLinearMap, ← coe_comp, eq, coe_comp] at this

Premises used: LinearMap.coe_comp, LinearEquiv.coe_toLinearMap
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
this :
  Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A)
      (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
        (a : A) → (i : ↥S) → A)
      (⇑m : (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) (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩

Premises used: LinearMap.range_eq_top, And.intro, Iff.mp, Module.Projective.of_split, Function.Injective.of_comp
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
this :
  Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A)
      (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
        (a : A) → (i : ↥S) → A)
      (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A))
refine : m.range = ⊤
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
    Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A) (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
refine ⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩
-- 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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype
eq :
  ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
      (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
    (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m
this :
  Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
    (Function.comp (β := A)
      (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
        (a : A) → (i : ↥S) → A)
      (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A))
x : A
x_1 : ↥(↑I : Submodule R A)
⊢ Eq (α := A)
    (((((AlgebraTensorModule.curry m : A →ₗ[R] ↥(↑I : Submodule R A) →ₗ[R] A) : (a : A) → ↥(↑I : Submodule R A) →ₗ[R] A)
              x :
            ↥(↑I : Submodule R A) →ₗ[R] A) :
          (a : ↥(↑I : Submodule R A)) → A)
        x_1 :
      A)
    (((((AlgebraTensorModule.curry
                    (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
                      (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
                        A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) :
                  A →ₗ[R] ↥(↑I : Submodule R A) →ₗ[R] A) :
                (a : A) → ↥(↑I : Submodule R A) →ₗ[R] A)
              x :
            ↥(↑I : Submodule R A) →ₗ[R] A) :
          (a : ↥(↑I : Submodule R A)) → A)
        x_1 :
      A)

Tactic:
rfl
-- 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
inst_11 : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A)

Tactic:
(projective_units_and_mul'_comp_lTensor_bijective I).1

Premises used: _private.0.Submodule.projective_units_and_mul'_comp_lTensor_bijective, And.left
-- 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
hI : IsUnit I
⊢ Projective.{u, u_4} R ↥I

Tactic:
projective_units hI.unit

Premises used: Set.Mem, Submodule.projective_units, IsUnit.unit
-- 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
inst_11 : FaithfulSMul R A
I J : (Submodule R A)ˣ
refine :
  Function.Injective (α := ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) (β := A)
    (Function.comp (β := ↥(↑(I * J) : Submodule R A))
      (⇑(↑(I * J) : Submodule R A).subtype : (a : ↥(↑(I * J) : Submodule R A)) → A)
      (⇑((↑I : Submodule R A).mulMap' (↑J : Submodule R A)) :
        (a : ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) → ↥(↑(I * J) : Submodule R A)))
⊢ ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A) ≃ₗ[R] ↥(↑(I * J) : Submodule R A)

Tactic:
refine .ofBijective _ ⟨.of_comp (f := Submodule.subtype _) ?_, mulMap'_surjective _ _⟩
-- 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
inst_11 : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ Function.Injective (α := ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) (β := A)
    (Function.comp (β := ↥(↑(I * J) : Submodule R A))
      (⇑(↑(I * J) : Submodule R A).subtype : (a : ↥(↑(I * J) : Submodule R A)) → A)
      (⇑((↑I : Submodule R A).mulMap' (↑J : Submodule R A)) :
        (a : ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) → ↥(↑(I * J) : Submodule R A)))

Tactic:
convert!
    (projective_units_and_mul'_comp_lTensor_bijective J).2.1.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.1.subtype_injective)

Premises used: Units.val, _private.0.Submodule.projective_units_and_mul'_comp_lTensor_bijective, And.right, Function.Injective.comp, And.left, Submodule.subtype_injective, Module.Flat.rTensor_preserves_injective_linearMap
-- 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
inst_11 : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ Module.Invertible.{u, u_4} R ↥(↑I : Submodule R A)

Tactic:
.left (tensorInvEquiv I)

Premises used: Submodule.tensorInvEquiv, Module.Invertible.left
-- 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
inst_11 : FaithfulSMul R A
I_1 J_1 I J : (Submodule R A)ˣ
rw : Nonempty.{u_4 + 1} (↥(↑(I * J) : Submodule R A) ≃ₗ[R] ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A))
⊢ Pic.mk.{u, u_4} R ↥(↑(I * J) : Submodule R A) =
    HMul.hMul (α := Pic R) (Pic.mk.{u, u_4} R ↥(↑I : Submodule R A)) (Pic.mk.{u, u_4} R ↥(↑J : Submodule R A))

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 : 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
inst_11 : FaithfulSMul R A
I_1 J_1 I J : (Submodule R A)ˣ
⊢ Nonempty.{u_4 + 1} (↥(↑(I * J) : Submodule R A) ≃ₗ[R] ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A))

Tactic:
⟨(tensorEquivMul I J).symm⟩

Premises used: LinearEquiv.symm, Submodule.tensorEquivMul, Nonempty.intro
-- 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
inst_11 : FaithfulSMul R A
I_1 J_1 I J : (Submodule R A)ˣ
⊢ Nonempty.{u_4 + 1} (↥(↑(I * J) : Submodule R A) ≃ₗ[R] ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A))

Tactic:
exact ⟨(tensorEquivMul I J).symm⟩
-- 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
h :
  ∀ (I : (Submodule R A)ˣ),
    Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I ↔
      Membership.mem (γ := Subgroup (Submodule R A)ˣ)
        (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
⊢ Eq (α := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A))
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A)))

Tactic:
ext I
-- 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)ˣ
h :
  Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I →
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
h₁ :
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I →
    Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I ↔
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I

Tactic:
constructor
-- 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)ˣ
h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
h₁ :
  ∀ (e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)),
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I

Tactic:
have e := (mk_eq_one_iff.mp h).some.symm
-- 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)ˣ
h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
h₁ :
  ∀ (e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)),
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I

Tactic:
have e' := (mk_eq_one_iff.mp (inv_mem h)).some.symm