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
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
⊢ Fintype.card.{v} (Free.ChooseBasisIndex R M) = 1

Tactic:
simpa using 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
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
have : ∀ (this : Unique (Free.ChooseBasisIndex R M)), Nonempty (M ≃ₗ[R] R)
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
have : Unique (Free.ChooseBasisIndex R M) :=
    (Fintype.card_eq_one_iff_nonempty_unique.mp (by simpa using this)).some
-- 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
this_1 : Fintype.card.{v} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
this : Unique (Free.ChooseBasisIndex R M)
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
⟨e ≪≫ₗ uniqueLinearEquiv R R default⟩

Premises used: Inhabited.default, Finsupp.uniqueLinearEquiv, Nonempty.intro, LinearEquiv.trans
-- 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
this_1 : Fintype.card.{v} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
this : Unique (Free.ChooseBasisIndex R M)
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
exact ⟨e ≪≫ₗ uniqueLinearEquiv R R default⟩
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
inl : Subsingleton R → finrank R M = 1
inr : Nontrivial R → finrank R M = 1
⊢ finrank R M = 1

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Subsingleton R
inl : Module.rank R M = 1
inl₁ inl₂ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
⊢ finrank R M = 1

Tactic:
rw [← rank_eq_one_iff_finrank_eq_one, rank_subsingleton]

Premises used: Module.rank_eq_one_iff_finrank_eq_one, rank_subsingleton
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
h : Nontrivial R
inr : finrank R R = 1
inr₁ inr₂ : Eq (α := ℕ) 1 1
⊢ finrank R M = 1

Tactic:
rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, finrank_self]

Premises used: Module.Invertible.free_iff_linearEquiv, Nonempty.some, LinearEquiv.finrank_eq, Iff.mp, Module.finrank_self
-- 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
inst_4 : StrongRankCondition R
inst_5 : Free R M
⊢ Module.rank R M = 1

Tactic:
rank_eq_one_iff_finrank_eq_one.mpr (Invertible.finrank_eq_one R M)

Premises used: Iff.mpr, Module.Invertible.finrank_eq_one, Module.rank_eq_one_iff_finrank_eq_one
-- 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 :
  ∀ (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)
⊢ 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:
ext
-- 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
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:
simp [LinearEquiv.conj, liftAux]

Premises used: TensorProduct.liftAux, LinearEquiv.conj
-- 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
⊢ 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]
-- 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
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ᵐᵒᵖ))))
⊢ Function.Bijective.{u + 1, v + 1} (α := R) (β := End R M) (⇑(toModuleEnd R M) : (a : R) → End R M)

Tactic:
simpa [this] using MulOpposite.opEquiv.bijective

Premises used: MulOpposite.opEquiv, Equiv.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
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
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))
⊢ Eq.{v + 1} (α := M) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₁ m) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ m)

Tactic:
obtain ⟨r, rfl⟩ := hf m

Premises used: rfl
-- 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
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)
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))

Tactic:
simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]

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

Tactic:
simpa [lTensor_surjective_iff] using hf

Premises used: Module.Invertible.lTensor_surjective_iff
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Bijective.{v + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
simpa [lTensor_bijective_iff] using bijective_self_of_surjective
    (f.lTensor _ ∘ₗ (linearEquiv R M).symm.toLinearMap) (by simpa [lTensor_surjective_iff] using hf)

Premises used: LinearEquiv.symm, LinearMap.lTensor, _private.0.Module.Invertible.bijective_self_of_surjective, LinearMap.comp, LinearEquiv.toLinearMap, Module.Invertible.lTensor_bijective_iff, Module.Invertible.linearEquiv
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.LeftInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
⊢ Function.RightInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)

Tactic:
Function.rightInverse_of_injective_of_leftInverse
    (bijective_of_surjective hfg.surjective).injective hfg

Premises used: Function.rightInverse_of_injective_of_leftInverse, Module.Invertible.bijective_of_surjective, Function.Bijective.injective, Function.LeftInverse.surjective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.RightInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
⊢ Function.LeftInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)

Tactic:
rightInverse_of_leftInverse hfg

Premises used: Function.RightInverse, Module.Invertible.rightInverse_of_leftInverse
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ Function.LeftInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M) ↔
    Function.RightInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)

Tactic:
⟨rightInverse_of_leftInverse, leftInverse_of_rightInverse⟩

Premises used: Iff.intro, Module.Invertible.leftInverse_of_rightInverse, Module.Invertible.rightInverse_of_leftInverse
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.LeftInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
x : M
⊢ Eq.{u_1 + 1} (α := N) ((linearEquivOfLeftInverse hfg : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.LeftInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
x : N
⊢ Eq.{v + 1} (α := M) (((linearEquivOfLeftInverse hfg).symm : (a : N) → M) x : M) ((g : (a : N) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.RightInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
x : M
⊢ Eq.{u_1 + 1} (α := N) ((linearEquivOfRightInverse hfg : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : Module.Invertible R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hfg : Function.RightInverse.{u_1 + 1, v + 1} (α := N) (β := M) (⇑f : (a : M) → N) (⇑g : (a : N) → M)
x : N
⊢ Eq.{v + 1} (α := M) (((linearEquivOfRightInverse hfg).symm : (a : N) → M) x : M) ((g : (a : N) → M) x : M)

Tactic:
rfl

Premises used: 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 : Module.Invertible R M
inst_10 : Semiring A
inst_11 : Algebra R A
inst_12 : Module.Invertible R A
inv : A →ₗ[R] R :=
  (↑(linearEquiv R A) : Dual R A ⊗[R] A →ₗ[R] R) ∘ₗ
    LinearMap.lTensor (Dual R A) (LinearMap.mul' R A) ∘ₗ
      (↑(LinearEquiv.symm (leftCancelEquiv A (linearEquiv R A))) : A →ₗ[R] Dual R A ⊗[R] (A ⊗[R] A))
s : Finset (Dual R A × A)
hs :
  Eq (α := Dual R A ⊗[R] A) ((LinearEquiv.symm (linearEquiv R A) : (a : R) → Dual R A ⊗[R] A) 1)
    (∑ i ∈ s, i.1 ⊗ₜ[R] i.2)
⊢ Eq (α := R) ((inv ∘ₗ Algebra.linearMap R A : (a : R) → R) 1 : R) ((LinearMap.id : (a : R) → R) 1 : R)

Tactic:
simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]

Premises used: LinearEquiv.symm_apply_eq, map_sum, TensorProduct.sum_tmul, Iff.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 : Module.Invertible R A
x : R
⊢ Eq.{u_4 + 1} (α := A) ((algEquivOfRing R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
rfl

Premises used: 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 : Module.Invertible R M
inst_10 : CommSemiring A
inst_11 : Algebra R A
⊢ Module.Invertible A (A ⊗[R] M)

Tactic:
.right (M := A ⊗[R] Dual R M) <| (AlgebraTensorModule.distribBaseChange ..).symm ≪≫ₗ
    AlgebraTensorModule.congr (.refl A A) (linearEquiv R M) ≪≫ₗ AlgebraTensorModule.rid ..

Premises used: LinearEquiv.symm, TensorProduct.AlgebraTensorModule.distribBaseChange, TensorProduct.AlgebraTensorModule.congr, TensorProduct.AlgebraTensorModule.rid, LinearEquiv.refl, LinearEquiv.trans, Module.Invertible.linearEquiv, Module.Invertible.right
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
N : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Module.Invertible R M
inst_6 : CommSemiring A
inst_7 : Algebra R A
S : Submonoid R
inst_8 : IsLocalization S A
f : M →ₗ[R] N
inst_9 : IsLocalizedModule S f
inst_10 : Module A N
inst_11 : IsScalarTower R A N
⊢ Module.Invertible A N

Tactic:
.congr (IsLocalizedModule.isBaseChange S A f).equiv

Premises used: IsLocalizedModule.isBaseChange, Module.Invertible.congr, IsBaseChange.equiv
-- 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
inst_10 : CommSemiring A
inst_11 : Algebra R A
S : Submonoid R
⊢ Module.Invertible (Localization (M := R) S) (LocalizedModule S M)

Tactic:
of_isLocalization S (LocalizedModule.mkLinearMap S M)

Premises used: Module.Invertible.of_isLocalization, LocalizedModule.mkLinearMap
-- 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
inst_10 : CommSemiring A
inst_11 : Algebra R A
L : Type u_5
inst_12 : AddCommMonoid L
inst_13 : Module R L
inst_14 : Module A L
inst_15 : IsScalarTower R A L
inst_16 : Module.Invertible A L
⊢ Module.Invertible A (L ⊗[R] M)

Tactic:
.congr (AlgebraTensorModule.cancelBaseChange R A A L M)

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, Module.Invertible.congr
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M_1 : 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_1
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
M : (Skeleton (SemimoduleCat R))ˣ
⊢ Module.Invertible R (↑(Quotient.out (↑M : Skeleton (SemimoduleCat R))) : Type u)

Tactic:
.right (Quotient.eq.mp M.inv_mul).some.toLinearEquivₛ

Premises used: CategoryTheory.Iso.toLinearEquivₛ, Units.inv_mul, Nonempty.some, Iff.mp, Quotient.eq, Module.Invertible.right
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M_1 : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M_1
inst_6 : Module R_1 N
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
R : Type u
inst_9 : CommRing R
M : (Skeleton (ModuleCat R))ˣ
⊢ Module.Invertible R (↑(Quotient.out (↑M : Skeleton (ModuleCat R))) : Type u)

Tactic:
.right (Quotient.eq.mp M.inv_mul).some.toLinearEquiv

Premises used: Units.inv_mul, CategoryTheory.Iso.toLinearEquiv, Nonempty.some, Iff.mp, Quotient.eq, Module.Invertible.right
-- 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
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ : sf
⊢ ModuleCon.Quotient (Fin (c₁.fst (β := fun (n : ℕ) ↦ ModuleCon R (Fin n → R))) → R)
      (c₁.snd (β := fun (n : ℕ) ↦ ModuleCon R (Fin n → R))) ≃ₗ[R]
    ModuleCon.Quotient (Fin (c₁.fst (β := fun (n : ℕ) ↦ ModuleCon R (Fin n → R))) → R)
      (c₁.snd (β := fun (n : ℕ) ↦ ModuleCon R (Fin n → R)))

Tactic:
exact .refl ..
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M
inst_6 : Module R_1 N
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
R : Type u
inst_9 : CommRing R
⊢ Small.{u, u + 1} (Skeleton (ModuleCat R))ˣ

Tactic:
small_map (Units.mapEquiv <| Skeleton.mulEquiv ModuleCat.equivalenceSemimoduleCat).toEquiv

Premises used: CategoryTheory.Skeleton.mulEquiv, MulEquiv.toEquiv, Units.mapEquiv, ModuleCat.equivalenceSemimoduleCat, small_map
-- Module: Mathlib.RingTheory.PicardGroup
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
⊢ Module.Invertible R (Finite.reprₛ R M)

Tactic:
.congr (Finite.reprEquivₛ R M).symm

Premises used: LinearEquiv.symm, Module.Finite.reprEquivₛ, Module.Invertible.congr
-- Module: Mathlib.RingTheory.PicardGroup
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_2 : Type u_5
N : Type u_6
inst_9 : AddCommMonoid M_2
inst_10 : Module R M_2
inst_11 : AddCommMonoid N
inst_12 : Module R N
inst_13 : Module.Invertible R M_2
inst_14 : Module.Invertible R N
M_3 : (Skeleton (SemimoduleCat R))ˣ
M : Skeleton (SemimoduleCat R)
⊢ (↑(Quotient.out M) : Type u) ≃ₗ[R] (↑(Quotient.out M) : Type u)

Tactic:
exact .refl ..