awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
h :
  ∀ (x : A ⊗[R] ↥(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)
          x :
        A)
      (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
              A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
            (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
          x :
        A)
⊢ Eq (α := A ⊗[R] ↥(submoduleAlgebra e) → 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)
    (⇑(AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
          A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
      (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)

Tactic:
ext x
-- 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 : 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)
⊢ 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)
        0 :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        0 :
      A)

Tactic:
simp
-- 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 : 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)
⊢ ∀ (x y : A ⊗[R] ↥(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)
            x :
          A)
        (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
                A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
              (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
            x :
          A) →
      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)
              y :
            A)
          (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
                  A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
                (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
              y :
            A) →
        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)
              (x + y) :
            A)
          (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
                  A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
                (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
              (x + y) :
            A)

Tactic:
simp +contextual
-- 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 : 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)
h :
  ∀ (x : A) (y : ↥(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)
          (x ⊗ₜ[R] y) :
        A)
      (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
              A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
            (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
          (x ⊗ₜ[R] y) :
        A)
⊢ 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)
        x :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        x :
      A)

Tactic:
refine x.induction_on (by simp) ?_ (by simp +contextual)
-- 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 : 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)
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)
⊢ 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)

Tactic:
obtain ⟨m, rfl⟩ := (submoduleAlgebraEquiv e).symm.surjective x

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Module.Flat.submoduleAlgebraEquiv, 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 : 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
this : HMul.hMul (β := A) a ((toAlgebra e : (a : M) → A) m : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] 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:
simpa using this
-- 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 : 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 ((toAlgebra e : (a : M) → A) m : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] 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:
suffices a * toAlgebra e m = e (a ⊗ₜ[R] m) by simpa using this
-- 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 : 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) ((algebraMap R A : (a : R) → A) 1 ⊗ₜ[R] m : A ⊗[R] M) : A) =
    (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)
⊢ HMul.hMul (β := A) a ((toAlgebra e : (a : M) → A) m : A) = (e : (a : A ⊗[R] M) → A) (a ⊗ₜ[R] m)

Tactic:
dsimp [toAlgebra]

Premises used: Module.Flat.toAlgebra
-- 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 : 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)
h₅ 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)
⊢ 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:
rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul', map_one, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.RingTheory.PicardGroup
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
rw : LinearMap.range (M := ↥⊤ ⊗[R] ↥(submoduleAlgebra e)) (Submodule.mulMap ⊤ (submoduleAlgebra e)) = ⊤
⊢ ⊤ * submoduleAlgebra e = ⊤

Tactic:
rw [← Submodule.mulMap_range]

Premises used: Submodule.mulMap_range
-- Module: Mathlib.RingTheory.PicardGroup
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
⊢ Eq (α := Submodule R A)
    (LinearMap.range
      (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
            LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
        ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A))
    ⊤

Tactic:
(Submodule.topEquiv.rTensor _ ≪≫ₗ (tensorSubmoduleAlgebraEquiv e).restrictScalars R).range

Premises used: Submodule.topEquiv, LinearEquiv.restrictScalars, LinearEquiv.rTensor, LinearEquiv.trans, Module.Flat.tensorSubmoduleAlgebraEquiv, LinearEquiv.range
-- Module: Mathlib.RingTheory.PicardGroup
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
h :
  Submodule.mulMap ⊤ (submoduleAlgebra e) =
    (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
          LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
      ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A)
⊢ LinearMap.range (M := ↥⊤ ⊗[R] ↥(submoduleAlgebra e)) (Submodule.mulMap ⊤ (submoduleAlgebra e)) = ⊤

Tactic:
convert!
    (Submodule.topEquiv.rTensor _ ≪≫ₗ (tensorSubmoduleAlgebraEquiv e).restrictScalars R).range

Premises used: Submodule.topEquiv, LinearEquiv.restrictScalars, LinearEquiv.rTensor, LinearEquiv.trans, Module.Flat.tensorSubmoduleAlgebraEquiv, LinearEquiv.range
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ Submodule.mulMap ⊤ (submoduleAlgebra e) =
    (↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
          LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) :
      ↥⊤ ⊗[R] ↥(submoduleAlgebra e) →ₗ[R] A)

Tactic:
ext
-- Module: Mathlib.RingTheory.PicardGroup
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
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:
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 : 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
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)))
⊢ ↥I ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[R] ↥(I * submoduleAlgebra e)

Tactic:
refine .ofBijective _ ⟨.of_comp (f := Submodule.subtype _) ?_, Submodule.mulMap'_surjective _ _⟩
-- 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 : 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 (β := 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:
((tensorSubmoduleAlgebraEquiv e).restrictScalars R).injective.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.subtype_injective)

Premises used: LinearEquiv.restrictScalars, Function.Injective.comp, LinearEquiv.injective, Submodule.subtype_injective, Module.Flat.tensorSubmoduleAlgebraEquiv, Module.Flat.rTensor_preserves_injective_linearMap
-- 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 : 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
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)))
⊢ 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:
convert!
    ((tensorSubmoduleAlgebraEquiv e).restrictScalars R).injective.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.subtype_injective)

Premises used: LinearEquiv.restrictScalars, Function.Injective.comp, LinearEquiv.injective, Submodule.subtype_injective, Module.Flat.tensorSubmoduleAlgebraEquiv, Module.Flat.rTensor_preserves_injective_linearMap