awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
rw : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((h.equiv : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] m) : N)
rw₁ : (f : (a : M) → N) m = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) m : N)
rw₂ rw₃ : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) m : N)
⊢ Eq (α := S ⊗[R] M) ((h.equiv.symm : (a : N) → S ⊗[R] M) ((f : (a : M) → N) m) : S ⊗[R] M) (1 ⊗ₜ[R] m : S ⊗[R] M)

Tactic:
rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]

Premises used: LinearEquiv.symm_apply_eq, one_smul, IsBaseChange.equiv_tmul, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), Eq.{v₂ + 1} (α := N) ((e : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N) ((f : (a : M) → N) x : N)
apply :
  ∀ (x : S) (y : M),
    Eq.{v₂ + 1} (α := N) ((LinearEquiv.restrictScalars R e : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
      (((((↑R :
                      {S M : Type v₃} →
                        {M₂ : Type (max v₁ v₂)} →
                          [inst : Semiring R] →
                            [inst_9 : Semiring S] →
                              [inst_10 : AddCommMonoid M] →
                                [inst_11 : AddCommMonoid M₂] →
                                  [inst_12 : Module R M] →
                                    [inst_13 : Module R M₂] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (S := S)
                    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                          (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                        (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                      f) :
                  (a : S) → M →ₗ[R] N)
                x :
              M →ₗ[R] N) :
            (a : M) → N)
          y :
        N)
⊢ IsBaseChange S f

Tactic:
apply IsTensorProduct.of_equiv (e.restrictScalars R)

Premises used: LinearEquiv.restrictScalars, IsTensorProduct.of_equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), Eq.{v₂ + 1} (α := N) ((e : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N) ((f : (a : M) → N) x : N)
x : S
y : M
⊢ x ⊗ₜ[R] y = HSMul.hSMul (β := S ⊗[R] M) x (1 ⊗ₜ[R] y)

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), Eq.{v₂ + 1} (α := N) ((e : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N) ((f : (a : M) → N) x : N)
x : S
y : M
⊢ Eq.{v₂ + 1} (α := N) ((LinearEquiv.restrictScalars R e : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
    (((((↑R :
                    {S M : Type v₃} →
                      {M₂ : Type (max v₁ v₂)} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := S)
                  (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                        (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                      (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                    f) :
                (a : S) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)

Tactic:
simp [show x ⊗ₜ[R] y = x • (1 ⊗ₜ[R] y) by simp [smul_tmul'], he]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
⊢ Eq.{v₃ + 1} (α := S) (((AlgebraTensorModule.rid R S S : S ⊗[R] R ≃ₗ[S] S) : (a : S ⊗[R] R) → S) (1 ⊗ₜ[R] x) : S)
    ((Algebra.linearMap R S : (a : R) → S) x : S)

Tactic:
simpa using (Algebra.algebraMap_eq_smul_one x).symm

Premises used: Algebra.algebraMap_eq_smul_one, Eq.symm
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
⊢ ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
      ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)

Tactic:
have (m : M) : f' (eM m) = eN (f m) := LinearMap.congr_fun comm m
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
this :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
      ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
⊢ IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max v₁ v₂)} →
              [inst : Semiring R] →
                [inst_15 : Semiring S] →
                  [inst_16 : AddCommMonoid M] →
                    [inst_17 : AddCommMonoid M₂] →
                      [inst_18 : Module R M] →
                        [inst_19 : Module R M₂] →
                          [inst_20 : Module S M] →
                            [inst_21 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := S)
        (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
            (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
          f)) ↔
    IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_15 : Semiring S] →
                  [inst_16 : AddCommMonoid M] →
                    [inst_17 : AddCommMonoid M₂] →
                      [inst_18 : Module R M] →
                        [inst_19 : Module R M₂] →
                          [inst_20 : Module S M] →
                            [inst_21 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := S)
        (((LinearMap.flip (Algebra.linearMap S (Module.End S (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
            (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
          f'))

Tactic:
⟨fun ist ↦ ?_, fun ist ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
this :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
      ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
ist :
  IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₂)} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S)
      (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
⊢ IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S)
    (LinearMap.compr₂
      (LinearMap.compl₂ (σ₂₃ := RingHom.id R)
        ((↑R :
            {S M : Type v₃} →
              {M₂ : Type (max v₁ v₂)} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
              (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
            f))
        (↑eM.symm : P →ₗ[R] M))
      (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q))

Tactic:
(ist.compl₂_linearEquiv eM.symm).compr₂_linearEquiv (eN.restrictScalars R)

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, IsTensorProduct.compl₂_linearEquiv, IsTensorProduct.compr₂_linearEquiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
this :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
      ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
ist :
  IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max u_2 u_3)} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S)
      (((LinearMap.flip (Algebra.linearMap S (Module.End S (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
          (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
        f'))
⊢ IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S)
    (LinearMap.compr₂
      (LinearMap.compl₂ (σ₂₃ := RingHom.id R)
        ((↑R :
            {S M : Type v₃} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
              (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
            f'))
        (↑eM : M →ₗ[R] P))
      (↑(LinearEquiv.restrictScalars R eN.symm) : Q →ₗ[R] N))

Tactic:
(ist.compl₂_linearEquiv eM).compr₂_linearEquiv (eN.symm.restrictScalars R)

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, IsTensorProduct.compl₂_linearEquiv, IsTensorProduct.compr₂_linearEquiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
e : M ≃ₗ[R] P
f : P →ₗ[R] N
isb : IsBaseChange S f
y : M
⊢ Eq.{v₂ + 1} (α := N) ((f ∘ₗ (↑e : M →ₗ[R] P) : (a : M) → N) y : N)
    (((↑(LinearEquiv.restrictScalars R (LinearEquiv.refl S N)) : N →ₗ[R] N) ∘ₗ f ∘ₗ (↑e : M →ₗ[R] P) : (a : M) → N) y :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
⊢ IsBaseChange (M := M ⊗[R] P) (N := N ⊗[R] P) A (AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P)

Tactic:
IsBaseChange.of_equiv e (fun x ↦ ?_)

Premises used: IsBaseChange.of_equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
refine :
  ∀ (x : M ⊗[R] P),
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
⊢ IsBaseChange (M := M ⊗[R] P) (N := N ⊗[R] P) A (AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P)

Tactic:
refine IsBaseChange.of_equiv e (fun x ↦ ?_)

Premises used: IsBaseChange.of_equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] 0) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) 0 : N ⊗[R] P)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x : M
y : P
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x ⊗ₜ[R] y)) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x ⊗ₜ[R] y) :
      N ⊗[R] P)

Tactic:
simp [e, IsBaseChange.equiv_tmul]

Premises used: IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x y : M ⊗[R] P
h1 :
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)
h2 :
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] y) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) y : N ⊗[R] P)
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x + y)) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x + y) :
      N ⊗[R] P)

Tactic:
simp [tmul_add, h1, h2]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
P : Type u_2
inst_9 : AddCommMonoid P
inst_10 : Module R P
A : Type u_4
inst_11 : CommSemiring A
inst_12 : Algebra R A
inst_13 : Algebra S A
inst_14 : IsScalarTower R S A
inst_15 : Module S M
inst_16 : IsScalarTower R S M
inst_17 : Module A N
inst_18 : IsScalarTower S A N
inst_19 : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (LinearEquiv.symm (AlgebraTensorModule.assoc R S A A M P) : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] A ⊗[S] M ⊗[R] P) ≪≫ₗ
    (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P) : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P)
x : M ⊗[R] P
zero :
  Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] 0) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) 0 : N ⊗[R] P)
tmul :
  ∀ (x : M) (y : P),
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x ⊗ₜ[R] y)) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x ⊗ₜ[R] y) :
        N ⊗[R] P)
add :
  ∀ (x y : M ⊗[R] P)
    (h1 :
      Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
        (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P))
    (h2 :
      Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] y) : N ⊗[R] P)
        (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) y :
          N ⊗[R] P)),
    Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] (x + y)) : N ⊗[R] P)
      (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) (x + y) :
        N ⊗[R] P)
⊢ Eq (α := N ⊗[R] P) ((e : (a : A ⊗[S] (M ⊗[R] P)) → N ⊗[R] P) (1 ⊗ₜ[S] x) : N ⊗[R] P)
    (((AlgebraTensorModule.map f LinearMap.id : M ⊗[R] P →ₗ[S] N ⊗[R] P) : (a : M ⊗[R] P) → N ⊗[R] P) x : N ⊗[R] P)

Tactic:
induction x with
  | zero => simp
  | tmul => simp [e, IsBaseChange.equiv_tmul]
  | add _ _ h1 h2 => simp [tmul_add, h1, h2]

Premises used: TensorProduct.tmul_add, IsBaseChange.equiv_tmul, TensorProduct.tmul