awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
  (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R)
f' : (↥S →₀ R) →ₗ[R] M :=
  (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
    LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N))
g' : M →ₗ[R] ↥S →₀ R :=
  (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
    LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
⊢ Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)

Tactic:
simpa [f'] using LinearMap.lTensor_surjective _ this

Premises used: LinearMap.lTensor_surjective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
  (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R)
f' : (↥S →₀ R) →ₗ[R] M :=
  (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
    LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N))
g' : M →ₗ[R] ↥S →₀ R :=
  (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
    LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
⊢ Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)

Tactic:
have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this_1 : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
  (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R)
f' : (↥S →₀ R) →ₗ[R] M :=
  (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
    LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N))
g' : M →ₗ[R] ↥S →₀ R :=
  (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
    LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
this : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)
⊢ Module.Finite R M ∧ Projective R M

Tactic:
⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩

Premises used: Module.Finite.of_surjective, LinearMap.ext, And.intro, Module.Projective.of_split
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this_1 : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
  (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R)
f' : (↥S →₀ R) →ₗ[R] M :=
  (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
    LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N))
g' : M →ₗ[R] ↥S →₀ R :=
  (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
    LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
this : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)
refine : ∀ (m : M), Eq (α := M) ((f' ∘ₗ g' : (a : M) → M) m : M) ((LinearMap.id : (a : M) → M) m : M)
⊢ Module.Finite R M ∧ Projective R M

Tactic:
refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this_1 : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
  (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R)
f' : (↥S →₀ R) →ₗ[R] M :=
  (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
    LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N))
g' : M →ₗ[R] ↥S →₀ R :=
  (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
    LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
this : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)
m : M
⊢ Eq (α := M) ((f' ∘ₗ g' : (a : M) → M) m : M) ((LinearMap.id : (a : M) → M) m : M)

Tactic:
simp [f', g', show f (g 1) = 1 from DFunLike.congr_fun hg 1]

Premises used: DFunLike.congr_fun, OfNat.ofNat
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : Eq (α := M ⊗[R] N) ((e.symm : (a : R) → M ⊗[R] N) 1) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2)
f : (↥S →₀ N) →ₗ[R] R :=
  (Finsupp.lsum R : (a : ↥S → N →ₗ[R] R) → (↥S →₀ N) →ₗ[R] R) fun (i : ↥S) ↦
    (↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1
this : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
let let₁ let₂ let₃ let₄ : Module.Finite R M ∧ Projective R M
let₅ :
  let aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
    (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
      (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R);
  let f' :=
    (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
      LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N));
  ∀ (this : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)), Module.Finite R M ∧ Projective R M
let₆ :
  let aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R :=
    (finsuppRight R R M N ↥S : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ M ⊗[R] N) ≪≫ₗ
      (Finsupp.mapRange.linearEquiv e : (↥S →₀ M ⊗[R] N) ≃ₗ[R] ↥S →₀ R);
  let f' :=
    (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) ∘ₗ
      LinearMap.lTensor M f ∘ₗ (↑aux.symm : (↥S →₀ R) →ₗ[R] M ⊗[R] (↥S →₀ N));
  let g' :=
    (↑aux : M ⊗[R] (↥S →₀ N) →ₗ[R] ↥S →₀ R) ∘ₗ
      LinearMap.lTensor M g ∘ₗ (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R);
  ∀ (this : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)) (m : M),
    Eq (α := M) ((f' ∘ₗ g' : (a : M) → M) m : M) ((LinearMap.id : (a : M) → M) m : M)
⊢ Module.Finite R M ∧ Projective R M

Tactic:
classical
  let aux := finsuppRight R _ M N S ≪≫ₗ Finsupp.mapRange.linearEquiv e
  let f' : (S →₀ R) →ₗ[R] M := TensorProduct.rid R M ∘ₗ f.lTensor M ∘ₗ aux.symm
  let g' : M →ₗ[R] S →₀ R := aux ∘ₗ g.lTensor M ∘ₗ (TensorProduct.rid R M).symm
  have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
  refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
  simp [f', g', show f (g 1) = 1 from DFunLike.congr_fun hg 1]

Premises used: DFunLike.congr_fun, OfNat.ofNat
-- 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 : Module.Invertible R M
⊢ Module.Finite R M

Tactic:
(finite_projective R M).1

Premises used: And.left, _private.0.Module.Invertible.finite_projective
-- 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 : Module.Invertible R M
⊢ Projective R M

Tactic:
(finite_projective R M).2

Premises used: And.right, _private.0.Module.Invertible.finite_projective
-- 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 : Module.Invertible R M
⊢ IsReflexive R M

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Iff.intro
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
refine :
  ∀ (h : Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)),
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
refine ⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
rw :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P)
    (⇑((↑(leftCancelEquiv P (linearEquiv R M)) : Dual R M ⊗[R] (M ⊗[R] P) →ₗ[R] P) ∘ₗ
          LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ
            (↑(LinearEquiv.symm (leftCancelEquiv N (linearEquiv R M))) : N →ₗ[R] Dual R M ⊗[R] (M ⊗[R] N))) :
      (a : N) → P)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]

Premises used: Module.Invertible.linearEquiv, Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P)
    (⇑((↑(leftCancelEquiv P (linearEquiv R M)) : Dual R M ⊗[R] (M ⊗[R] P) →ₗ[R] P) ∘ₗ
          LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ
            (↑(LinearEquiv.symm (leftCancelEquiv N (linearEquiv R M))) : N →ₗ[R] Dual R M ⊗[R] (M ⊗[R] N))) :
      (a : N) → P)

Tactic:
simpa using Flat.lTensor_preserves_injective_linearMap _ h

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
rw :
  Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
rw₁ rw₂ :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
rw [← LinearMap.lTensor_inj_iff_rTensor_inj, lTensor_injective_iff]

Premises used: Module.Invertible.lTensor_injective_iff, LinearMap.lTensor_inj_iff_rTensor_inj
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
⟨fun h ↦ ?_, LinearMap.lTensor_surjective _⟩

Premises used: LinearMap.lTensor_surjective, Iff.intro
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
refine :
  ∀ (h : Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
refine ⟨fun h ↦ ?_, LinearMap.lTensor_surjective _⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
rw :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P)
    (⇑((↑(leftCancelEquiv P (linearEquiv R M)) : Dual R M ⊗[R] (M ⊗[R] P) →ₗ[R] P) ∘ₗ
          LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ
            (↑(LinearEquiv.symm (leftCancelEquiv N (linearEquiv R M))) : N →ₗ[R] Dual R M ⊗[R] (M ⊗[R] N))) :
      (a : N) → P)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]

Premises used: Module.Invertible.linearEquiv, Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P)
    (⇑((↑(leftCancelEquiv P (linearEquiv R M)) : Dual R M ⊗[R] (M ⊗[R] P) →ₗ[R] P) ∘ₗ
          LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ
            (↑(LinearEquiv.symm (leftCancelEquiv N (linearEquiv R M))) : N →ₗ[R] Dual R M ⊗[R] (M ⊗[R] N))) :
      (a : N) → P)

Tactic:
simpa using LinearMap.lTensor_surjective _ h

Premises used: LinearMap.lTensor_surjective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
rw :
  Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
rw₁ rw₂ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Surjective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
rw [← LinearMap.lTensor_surj_iff_rTensor_surj, lTensor_surjective_iff]

Premises used: LinearMap.lTensor_surj_iff_rTensor_surj, Module.Invertible.lTensor_surjective_iff
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
simp_rw :
  Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ∧
      Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
simp_rw₁ :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Bijective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
simp_rw [Function.Bijective, lTensor_injective_iff, lTensor_surjective_iff]

Premises used: Module.Invertible.lTensor_injective_iff, Function.Bijective, Module.Invertible.lTensor_surjective_iff
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Invertible R M
f : N →ₗ[R] P
simp_rw :
  Function.Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ∧
      Function.Surjective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
simp_rw₁ :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P) ∧
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Function.Bijective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(LinearMap.rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Function.Bijective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)

Tactic:
simp_rw [Function.Bijective, rTensor_injective_iff, rTensor_surjective_iff]

Premises used: Module.Invertible.rTensor_injective_iff, Module.Invertible.rTensor_surjective_iff, Function.Bijective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
⊢ Free R M ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩

Premises used: LinearEquiv.symm, _private.0.Module.Invertible.free_iff_linearEquiv.match_1, Module.Free, Module.Free.of_equiv, Iff.intro
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
refine : Free R M → Nonempty (M ≃ₗ[R] R)
⊢ Free R M ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
h : Free R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
h : Free R M
h_1 : Nontrivial R
have : ∀ (e : M ≃ₗ[R] Finsupp.{v, u} (Free.ChooseBasisIndex R M) R), Nonempty (M ≃ₗ[R] R)
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
have e := (Free.chooseBasis R M).repr
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Invertible R M
h : Free R M
h_1 : Nontrivial R
e : M ≃ₗ[R] Finsupp.{v, u} (Free.ChooseBasisIndex R M) R
⊢ Fintype.card.{v} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit

Tactic:
have := card_eq_of_linearEquiv R <|
    (finsuppTensorFinsupp' .. ≪≫ₗ linearEquivFunOnFinite R R _).symm ≪≫ₗ TensorProduct.congr
      (linearEquivFunOnFinite R R _ ≪≫ₗ llift R R R _ ≪≫ₗ e.dualMap)
      e.symm ≪≫ₗ linearEquiv R M ≪≫ₗ (.symm <| .funUnique Unit R R)