awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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.{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)
Tactic: rw [← LinearMap.lTensor_inj_iff_rTensor_inj, lTensor_injective_iff]
-- 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.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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, LinearMap.lTensor_surjective _⟩
-- 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.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)
have 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)
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.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)
have 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)
Tactic: rw [← LinearMap.lTensor_surj_iff_rTensor_surj, lTensor_surjective_iff]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← LinearMap.lTensor_surj_iff_rTensor_surj, lTensor_surjective_iff]
-- 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.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)
have 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)
Tactic: simp_rw [Function.Bijective, lTensor_injective_iff, lTensor_surjective_iff]
-- 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
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)
⊢ 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)
have 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)
Tactic: simp_rw [Function.Bijective, lTensor_injective_iff, lTensor_surjective_iff]
-- 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.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)
have 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)
Tactic: simp_rw [Function.Bijective, rTensor_injective_iff, rTensor_surjective_iff]
-- 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
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)
⊢ 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)
have 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)
Tactic: simp_rw [Function.Bijective, rTensor_injective_iff, rTensor_surjective_iff]
-- 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
⊢ Free R M ↔ Nonempty (M ≃ₗ[R] R)
have refine : Free R M → Nonempty (M ≃ₗ[R] R)
Tactic: refine ⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩
-- 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
h : Free R M
⊢ Nonempty (M ≃ₗ[R] R)
have a : Nontrivial R
Tactic: nontriviality R
-- 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
h : Free R M
h_1 : Nontrivial R
⊢ Nonempty (M ≃ₗ[R] R)
have have : ∀ (e : M ≃ₗ[R] Finsupp.{v, u} (Free.ChooseBasisIndex R M) R), Nonempty (M ≃ₗ[R] R)
Tactic: have e := (Free.chooseBasis R M).repr
-- 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
h : Free R M
h_1 : Nontrivial R
e : M ≃ₗ[R] Finsupp.{v, u} (Free.ChooseBasisIndex R M) R
⊢ Nonempty (M ≃ₗ[R] R)
have this : 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)
-- 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
h : Free R M
h_1 : Nontrivial R
e : M ≃ₗ[R] Finsupp.{v, u} (Free.ChooseBasisIndex R M) R
this : Fintype.card.{v} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
⊢ Nonempty (M ≃ₗ[R] R)
have have : ∀ (this : Unique (Free.ChooseBasisIndex R M)), Nonempty (M ≃ₗ[R] R)
Tactic: have : Unique (Free.ChooseBasisIndex R M) :=
    (Fintype.card_eq_one_iff_nonempty_unique.mp (by simpa using this)).some
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
⊢ finrank R M = 1
have inl : Subsingleton R → finrank R M = 1
Tactic: cases subsingleton_or_nontrivial R
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
inl : Subsingleton R → finrank R M = 1
⊢ finrank R M = 1
have inr : Nontrivial R → finrank R M = 1
Tactic: cases subsingleton_or_nontrivial R
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Subsingleton R
⊢ finrank R M = 1
have inl : Module.rank R M = 1
Tactic: rw [← rank_eq_one_iff_finrank_eq_one, rank_subsingleton]
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Subsingleton R
inl : Module.rank R M = 1
⊢ finrank R M = 1
have inl₁ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
Tactic: rw [← rank_eq_one_iff_finrank_eq_one, rank_subsingleton]
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Nontrivial R
⊢ finrank R M = 1
have inr : finrank R R = 1
Tactic: rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, finrank_self]
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Nontrivial R
inr : finrank R R = 1
⊢ finrank R M = 1
have inr₁ : Eq (α := ℕ) 1 1
Tactic: rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, finrank_self]
-- 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
⊢ Eq (α := (a : R) → End R M) (⇑(toModuleEnd R M) : (a : R) → End R M)
    (Function.comp (β := End R (R ⊗[R] M)) (⇑(LinearEquiv.conj (lid R M)) : (a : End R (R ⊗[R] M)) → End R M)
      (Function.comp (β := R →ₗ[R] R)
        (⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) :
          (a : R →ₗ[R] R) → R ⊗[R] M →ₗ[R] R ⊗[R] M)
        (Function.comp (β := Rᵐᵒᵖ) (⇑(RingEquiv.moduleEndSelf R) : (a : Rᵐᵒᵖ) → End R R)
          (⇑MulOpposite.opEquiv : (a : R) → Rᵐᵒᵖ))))
have h : ∀ (x : R) (x_1 : M),
  Eq (α := M) ((((toModuleEnd R M : (a : R) → End R M) x : End R M) : (a : M) → M) x_1 : M)
    ((Function.comp (β := End R (R ⊗[R] M)) (⇑(LinearEquiv.conj (lid R M)) : (a : End R (R ⊗[R] M)) → End R M)
            (Function.comp (β := R →ₗ[R] R)
              (⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) :
                (a : R →ₗ[R] R) → R ⊗[R] M →ₗ[R] R ⊗[R] M)
              (Function.comp (β := Rᵐᵒᵖ) (⇑(RingEquiv.moduleEndSelf R) : (a : Rᵐᵒᵖ) → End R R)
                (⇑MulOpposite.opEquiv : (a : R) → Rᵐᵒᵖ)))
            x :
          (a : M) → M)
        x_1 :
      M)
Tactic: ext
-- 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
⊢ Function.Bijective.{u + 1, v + 1} (α := R) (β := End R M) (⇑(toModuleEnd R M) : (a : R) → End R M)
have this : Eq (α := (a : R) → End R M) (⇑(toModuleEnd R M) : (a : R) → End R M)
  (Function.comp (β := End R (R ⊗[R] M)) (⇑(LinearEquiv.conj (lid R M)) : (a : End R (R ⊗[R] M)) → End R M)
    (Function.comp (β := R →ₗ[R] R)
      (⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) :
        (a : R →ₗ[R] R) → R ⊗[R] M →ₗ[R] R ⊗[R] M)
      (Function.comp (β := Rᵐᵒᵖ) (⇑(RingEquiv.moduleEndSelf R) : (a : Rᵐᵒᵖ) → End R R)
        (⇑MulOpposite.opEquiv : (a : R) → Rᵐᵒᵖ))))
Tactic: have : toModuleEnd R (S := R) M = (lid R M).conj ∘ rTensorEquiv R R
      (comm .. ≪≫ₗ linearEquiv R M) ∘ RingEquiv.moduleEndSelf R ∘ MulOpposite.opEquiv := by
    ext; simp [LinearEquiv.conj, liftAux]
-- 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
m : M
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ m) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ m)
have obtain : ∀ (r : R),
  Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
Tactic: obtain ⟨r, rfl⟩ := hf m
Cleared hypotheses: 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
r : R
simp_rw simp_rw₁ : HSMul.hSMul (β := M) r₁ ((f : (a : R) → M) r : M) = HSMul.hSMul (β := M) r₂ ((f : (a : R) → M) r : M)
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
have simp_rw₂ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ • r) : M) ((f : (a : R) → M) (r₂ • r) : M)
Tactic: simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]
-- 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
r : R
simp_rw simp_rw₁ : HSMul.hSMul (β := M) r₁ ((f : (a : R) → M) r : M) = HSMul.hSMul (β := M) r₂ ((f : (a : R) → M) r : M)
simp_rw₂ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ • r) : M) ((f : (a : R) → M) (r₂ • r) : M)
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
have simp_rw₃ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ * r) : M) ((f : (a : R) → M) (r₂ * r) : M)
Tactic: simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]
-- 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
r : R
simp_rw simp_rw₁ : HSMul.hSMul (β := M) r₁ ((f : (a : R) → M) r : M) = HSMul.hSMul (β := M) r₂ ((f : (a : R) → M) r : M)
simp_rw₂ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ • r) : M) ((f : (a : R) → M) (r₂ • r) : M)
simp_rw₃ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ * r) : M) ((f : (a : R) → M) (r₂ * r) : M)
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
have simp_rw₄ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r * r₁) : M) ((f : (a : R) → M) (r * r₂) : M)
Tactic: simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]
-- 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
r : R
simp_rw simp_rw₁ : HSMul.hSMul (β := M) r₁ ((f : (a : R) → M) r : M) = HSMul.hSMul (β := M) r₂ ((f : (a : R) → M) r : M)
simp_rw₂ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ • r) : M) ((f : (a : R) → M) (r₂ • r) : M)
simp_rw₃ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ * r) : M) ((f : (a : R) → M) (r₂ * r) : M)
simp_rw₄ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r * r₁) : M) ((f : (a : R) → M) (r * r₂) : M)
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
have simp_rw₅ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r • r₁) : M) ((f : (a : R) → M) (r • r₂) : M)
Tactic: simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]
-- 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
f : R →ₗ[R] M
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
r₁ r₂ : R
eq : Eq.{v + 1} (α := M) ((f : (a : R) → M) r₁ : M) ((f : (a : R) → M) r₂ : M)
r : R
simp_rw simp_rw₁ : HSMul.hSMul (β := M) r₁ ((f : (a : R) → M) r : M) = HSMul.hSMul (β := M) r₂ ((f : (a : R) → M) r : M)
simp_rw₂ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ • r) : M) ((f : (a : R) → M) (r₂ • r) : M)
simp_rw₃ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r₁ * r) : M) ((f : (a : R) → M) (r₂ * r) : M)
simp_rw₄ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r * r₁) : M) ((f : (a : R) → M) (r * r₂) : M)
simp_rw₅ : Eq.{v + 1} (α := M) ((f : (a : R) → M) (r • r₁) : M) ((f : (a : R) → M) (r • r₂) : M)
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ ((f : (a : R) → M) r))
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ ((f : (a : R) → M) r))
have simp_rw₆ : HSMul.hSMul (β := M) r ((f : (a : R) → M) r₁ : M) = HSMul.hSMul (β := M) r ((f : (a : R) → M) r₂ : M)
Tactic: simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]
-- 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 : 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
M' : Type u := Finite.reprₛ R M
⊢ HMul.hMul (α := Skeleton (SemimoduleCat R)) ⟦SemimoduleCat.of R M'⟧ ⟦SemimoduleCat.of R (Dual R M')⟧ = 1
have rw : Eq (α := Skeleton (SemimoduleCat R))
  (toSkeleton
    (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R) (SemimoduleCat.of R (Dual R M'))
      (SemimoduleCat.of R M')))
  1
Tactic: rw [← toSkeleton, ← toSkeleton, mul_comm, ← Skeleton.toSkeleton_tensorObj]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : Pic R
⊢ M = N ↔ Nonempty.{u + 1} (M.AsModule ≃ₗ[R] N.AsModule)
have rw : M = N ↔ Pic.mk R M.AsModule = N
Tactic: rw [← mk_eq_iff, 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 ↔ Pic.mk R M.AsModule = N
⊢ M = N ↔ Nonempty.{u + 1} (M.AsModule ≃ₗ[R] N.AsModule)
have rw₁ : M = N ↔ M = N
Tactic: rw [← mk_eq_iff, mk_eq_self]
-- 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 (α := Pic R) (Pic.mk R M) 1 ↔ Nonempty (M ≃ₗ[R] R)
have rw : Eq (α := Pic R) (Pic.mk R M) (Pic.mk R R) ↔ Nonempty (M ≃ₗ[R] R)
Tactic: rw [← mk_self, mk_eq_mk_iff]
-- 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
rw : Eq (α := Pic R) (Pic.mk R M) (Pic.mk R R) ↔ Nonempty (M ≃ₗ[R] R)
⊢ Eq (α := Pic R) (Pic.mk R M) 1 ↔ Nonempty (M ≃ₗ[R] R)
have rw₁ : Nonempty (M ≃ₗ[R] R) ↔ Nonempty (M ≃ₗ[R] R)
Tactic: rw [← mk_self, mk_eq_mk_iff]