awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
have rw : 1 ∈ f.range
Tactic: rw [← LinearMap.range_eq_top, Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ 1 ∈ f.range
have h : Eq.{u + 1} (α := R)
  ((f : (a : ↥S →₀ N) → R)
      ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2) :
    R)
  (1 : R)
Tactic: use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Eq.{u + 1} (α := R)
    ((f : (a : ↥S →₀ N) → R)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2) :
      R)
    (1 : R)
have h : Eq.{u + 1} (α := R)
  (Finsupp.sum (M := N) ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2)
    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) : (a : N) → R))
  1
Tactic: simp_rw [f, Finsupp.coe_lsum]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Eq.{u + 1} (α := R)
    (Finsupp.sum (M := N) ((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2)
      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) :
        (a : N) → R))
    1
have h : Eq.{u + 1} (α := R)
  (∑ i : ↥S,
    ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
      (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N) i :
        N))
  1
Tactic: rw [Finsupp.sum_fintype _ _ fun _ ↦ map_zero _]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
have h : ∀ (hS : Eq.{u + 1} (α := R) (1 : R) ((e : (a : M ⊗[R] N) → R) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) : R)),
  Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
Tactic: rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
Cleared hypotheses: hS, f
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
h :
  ∀ (hS : Eq.{u + 1} (α := R) (1 : R) ((e : (a : M ⊗[R] N) → R) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) : R)),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
⊢ Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
have h₁ : ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ x ∈ S, (e : (a : M ⊗[R] N) → R) (x.1 ⊗ₜ[R] x.2))),
  Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
Tactic: rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
Cleared hypotheses: hS, f
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
h :
  ∀ (hS : Eq.{u + 1} (α := R) (1 : R) ((e : (a : M ⊗[R] N) → R) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) : R)),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₁ :
  ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ x ∈ S, (e : (a : M ⊗[R] N) → R) (x.1 ⊗ₜ[R] x.2))),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
⊢ Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
have h₂ : ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ i : ↥S, (e : (a : M ⊗[R] N) → R) ((↑i : M × N).1 ⊗ₜ[R] (↑i : M × N).2))),
  Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
Tactic: rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
Cleared hypotheses: hS, f
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
h :
  ∀ (hS : Eq.{u + 1} (α := R) (1 : R) ((e : (a : M ⊗[R] N) → R) (∑ i ∈ S, i.1 ⊗ₜ[R] i.2) : R)),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₁ :
  ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ x ∈ S, (e : (a : M ⊗[R] N) → R) (x.1 ⊗ₜ[R] x.2))),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
h₂ :
  ∀ (hS : Eq.{u + 1} (α := R) 1 (∑ i : ↥S, (e : (a : M ⊗[R] N) → R) ((↑i : M × N).1 ⊗ₜ[R] (↑i : M × N).2))),
    Eq.{u + 1} (α := R)
      (∑ i : ↥S,
        ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
          (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
              i :
            N))
      1
⊢ Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
have h₃ : ∀ (hS : Eq.{u + 1} (α := R) (∑ i : ↥S, (e : (a : M ⊗[R] N) → R) ((↑i : M × N).1 ⊗ₜ[R] (↑i : M × N).2)) 1),
  Eq.{u + 1} (α := R)
    (∑ i : ↥S,
      ((↑e : M ⊗[R] N →ₗ[R] R) ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (↑i : M × N).1 : (a : N) → R)
        (((Equiv.symm Finsupp.equivFunOnFinite : (a : ↥S → N) → ↥S →₀ N) fun (i : ↥S) ↦ (↑i : M × N).2 : (a : ↥S) → N)
            i :
          N))
    1
Tactic: rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
Cleared hypotheses: hS, f
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
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
⊢ Module.Finite R M ∧ Projective R M
have this : Function.Surjective (α := ↥S →₀ N) (β := R) (⇑f : (a : ↥S →₀ N) → R)
Tactic: have : Function.Surjective f := by
    rw [← LinearMap.range_eq_top, Ideal.eq_top_iff_one]
    use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2
    simp_rw [f, Finsupp.coe_lsum]
    rw [Finsupp.sum_fintype _ _ fun _ ↦ map_zero _]
    rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
⊢ Module.Finite R M ∧ Projective R M
have have : ∀ (g : R →ₗ[R] ↥S →₀ N) (hg : f ∘ₗ g = LinearMap.id), Module.Finite R M ∧ Projective R M
Tactic: have ⟨g, hg⟩ := projective_lifting_property f .id this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
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)
⊢ Module.Finite R M ∧ Projective R M
have this₁ : Function.Surjective (α := ↥S →₀ R) (β := M) (⇑f' : (a : ↥S →₀ R) → M)
Tactic: have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
have refine : ∀ (m : M), Eq (α := M) ((f' ∘ₗ g' : (a : M) → M) m : M) ((LinearMap.id : (a : M) → M) m : M)
Tactic: refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Module.Finite R M ∧ Projective R M
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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
⊢ Module.Finite R M ∧ Projective R M
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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) (⇑f : (a : N) → P)
have 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)
Tactic: rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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 (α := 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)
have 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)
Tactic: rw [← LinearMap.lTensor_inj_iff_rTensor_inj, lTensor_injective_iff]