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
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x_1 : A ⊗[R] ↥(submoduleAlgebra e)
a : A
x : ↥(submoduleAlgebra e)
⊢ Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] x) :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] x) :
      A)
have h : ∀ (m : M),
  Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] ((submoduleAlgebraEquiv e).symm : (a : M) → ↥(submoduleAlgebra e)) m : A ⊗[R] ↥(submoduleAlgebra e)) :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] ((submoduleAlgebraEquiv e).symm : (a : M) → ↥(submoduleAlgebra e)) m : A ⊗[R] ↥(submoduleAlgebra e)) :
      A)
Tactic: obtain ⟨m, rfl⟩ := (submoduleAlgebraEquiv e).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] ((submoduleAlgebraEquiv e).symm : (a : M) → ↥(submoduleAlgebra e)) m : A ⊗[R] ↥(submoduleAlgebra e)) :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (a ⊗ₜ[R] ((submoduleAlgebraEquiv e).symm : (a : M) → ↥(submoduleAlgebra e)) m : A ⊗[R] ↥(submoduleAlgebra e)) :
      A)
have h : HMul.hMul (β := A) a ((toAlgebra e : (a : M) → A) m : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
Tactic: suffices a * toAlgebra e m = e (a ⊗ₜ[R] m) by simpa using this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ HMul.hMul (β := A) a ((toAlgebra e : (a : M) → A) m : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
  (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
Tactic: dsimp [toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h₁ : HSMul.hSMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₁ : HSMul.hSMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h₂ : Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m)) : A)
  ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₁ : HSMul.hSMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₂ :
  Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m)) : A)
    ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h₃ : Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : A)
  ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₁ : HSMul.hSMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₂ :
  Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m)) : A)
    ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
h₃ :
  Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : A)
    ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h₄ : Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) ((a * 1) ⊗ₜ[R] m) : A) ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
h : HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₁ : HSMul.hSMul (β := A) a ((e : (a : A ⊗[R] M) → A) (1 ⊗ₜ[R] m) : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
h₂ :
  Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m)) : A)
    ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
h₃ :
  Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : A)
    ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
h₄ : Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) ((a * 1) ⊗ₜ[R] m) : A) ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
⊢ HMul.hMul (β := A) a ((e : (a : A ⊗[R] M) → A) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
have h₅ : Eq.{u_4 + 1} (α := A) ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A) ((e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m) : A)
Tactic: rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_5 : Flat R M
inst_6 : FaithfulSMul R A
⊢ ⊤ * submoduleAlgebra e = ⊤
have rw : LinearMap.range (M := ↥⊤ ⊗[R] ↥(submoduleAlgebra e)) (Submodule.mulMap ⊤ (submoduleAlgebra e)) = ⊤
Tactic: rw [← Submodule.mulMap_range]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_5 : Flat R M
inst_6 : FaithfulSMul R A
⊢ LinearMap.range (M := ↥⊤ ⊗[R] ↥(submoduleAlgebra e)) (Submodule.mulMap ⊤ (submoduleAlgebra e)) = ⊤
have h : Submodule.mulMap ⊤ (submoduleAlgebra e) =
  (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
        LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
    ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A)
Tactic: convert!
    (Submodule.topEquiv.rTensor _ ≪≫ₗ (tensorSubmoduleAlgebraEquiv e).restrictScalars R).range
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_5 : Flat R M
inst_6 : FaithfulSMul R A
⊢ Submodule.mulMap ⊤ (submoduleAlgebra e) =
    (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
          LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
      ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A)
have h : ∀ (x : ↥⊤) (x_1 : ↥(submoduleAlgebra e)),
  Eq (α := A)
    (((((AlgebraTensorModule.curry (Submodule.mulMap ⊤ (submoduleAlgebra e)) : ↥⊤ →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥⊤) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)
    (((((AlgebraTensorModule.curry
                    (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
                          LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
                      ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                  ↥⊤ →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥⊤) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
⊢ ↥I ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[R] ↥(I * submoduleAlgebra e)
have refine : Function.Injective (α := ↥I ⊗[R] ↥(submoduleAlgebra e)) (β := A)
  (Function.comp (β := ↥(I * submoduleAlgebra e))
    (⇑(I * submoduleAlgebra e).subtype : (a : ↥(I * submoduleAlgebra e)) → A)
    (⇑(I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → ↥(I * submoduleAlgebra e)))
Tactic: refine .ofBijective _ ⟨.of_comp (f := Submodule.subtype _) ?_, Submodule.mulMap'_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
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
⊢ Function.Injective (α := ↥I ⊗[R] ↥(submoduleAlgebra e)) (β := A)
    (Function.comp (β := ↥(I * submoduleAlgebra e))
      (⇑(I * submoduleAlgebra e).subtype : (a : ↥(I * submoduleAlgebra e)) → A)
      (⇑(I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → ↥(I * submoduleAlgebra e)))
have h : Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
  (Function.comp (β := ↥(I * submoduleAlgebra e))
    (⇑(I * submoduleAlgebra e).subtype : (a : ↥(I * submoduleAlgebra e)) → A)
    (⇑(I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → ↥(I * submoduleAlgebra e)))
  (Function.comp (β := A ⊗[R] ↥(submoduleAlgebra e))
    (⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
    (⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
      (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A ⊗[R] ↥(submoduleAlgebra e)))
Tactic: convert!
    ((tensorSubmoduleAlgebraEquiv e).restrictScalars R).injective.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.subtype_injective)
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
⊢ Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
    (Function.comp (β := ↥(I * submoduleAlgebra e))
      (⇑(I * submoduleAlgebra e).subtype : (a : ↥(I * submoduleAlgebra e)) → A)
      (⇑(I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → ↥(I * submoduleAlgebra e)))
    (Function.comp (β := A ⊗[R] ↥(submoduleAlgebra e))
      (⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
      (⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
        (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A ⊗[R] ↥(submoduleAlgebra e)))
have h : Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
  (⇑((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
  (⇑((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
        LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
    (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
Tactic: simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
⊢ Eq (α := ↥I ⊗[R] ↥(submoduleAlgebra e) → A)
    (⇑((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) : (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
    (⇑((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
          LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
      (a : ↥I ⊗[R] ↥(submoduleAlgebra e)) → A)
have h : (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
  (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
    LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype
Tactic: congr 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
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
I : Submodule R A
⊢ (I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e) =
    (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) : A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype
have h : ∀ (x : ↥I) (x_1 : ↥(submoduleAlgebra e)),
  Eq (α := A)
    (((((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) :
                  ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
                        A ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A) ∘ₗ
                      LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype) :
                  ↥I →ₗ[R] ↥(submoduleAlgebra e) →ₗ[R] A) :
                (a : ↥I) → ↥(submoduleAlgebra e) →ₗ[R] A)
              x :
            ↥(submoduleAlgebra e) →ₗ[R] A) :
          (a : ↥(submoduleAlgebra e)) → A)
        x_1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ Eq (α := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) (relPic R A)
have h : ∀ (M : Pic R),
  Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M ↔
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
Tactic: ext M
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M ↔
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
have h : Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M →
  Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h :
  Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M →
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M ↔
    Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
have h₁ : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M →
  Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
⊢ Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
have h₁ : ∀ (I : (Submodule R A)ˣ),
  Membership.mem (α := Pic R) (γ := Subgroup (Pic R)) (relPic R A)
    (((unitsToPic R A : MonoidHom.{u_4, u} (Submodule R A)ˣ (Pic R)) : (a : (Submodule R A)ˣ) → Pic R) I : Pic R)
Tactic: obtain ⟨I, rfl⟩ := h
Cleared hypotheses: M, h
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
have h₁ : ∀ (f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A),
  Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
Tactic: have f := (mk_eq_one_iff.mp (inv_mem h)).some
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ Membership.mem (γ := Subgroup (Pic R)) (MonoidHom.range (G := (Submodule R A)ˣ) (unitsToPic R A)) M
have h₁ : IsUnit (submoduleAlgebra e * submoduleAlgebra f)
Tactic: refine ⟨(isUnit_of_mul_isUnit_left (x := submoduleAlgebra e) (y := submoduleAlgebra f) ?_).unit,
    mk_eq_iff.mpr ⟨submoduleAlgebraEquiv e⟩⟩