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
x : N
motive : N → Prop
zero : motive 0
tmul : ∀ (m : M), motive ((f : (a : M) → N) m)
smul : ∀ (s : S) (n : N), motive n → motive (s • n)
add : ∀ (n₁ n₂ : N), motive n₁ → motive n₂ → motive (n₁ + n₂)
⊢ motive x

Tactic:
h.inductionOn x zero (fun _ _ => smul _ _ (tmul _)) add

Premises used: IsTensorProduct.inductionOn
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
h₁ : ∀ (x : N), Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
⊢ g₁ = g₂

Tactic:
ext x
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)

Tactic:
h.inductionOn x _ ?_ ?_ ?_ ?_

Premises used: IsBaseChange.inductionOn, Eq, DFunLike.coe
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
h₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
h₂ :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
h₃ :
  ∀ (s : S) (n : N),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q) →
      Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
h₄ :
  ∀ (n₁ n₂ : N),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n₁ : Q) ((g₂ : (a : N) → Q) n₁ : Q) →
      Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n₂ : Q) ((g₂ : (a : N) → Q) n₂ : Q) →
        Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (n₁ + n₂) : Q) ((g₂ : (a : N) → Q) (n₁ + n₂) : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)

Tactic:
refine h.inductionOn x _ ?_ ?_ ?_ ?_
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
h₁ : Eq.{u_3 + 1} (α := Q) (0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
h₂ h₃ : Eq.{u_3 + 1} (α := Q) 0 0
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
⊢ ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)

Tactic:
assumption
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
s : S
n : N
e' : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q)
h₁ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = (g₂ : (a : N) → Q) (s • n)
h₂ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q)
h₃ h₄ : HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q) = HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)

Tactic:
rw [g₁.map_smul, g₂.map_smul, e']

Premises used: LinearMap.map_smul
-- 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x_1 x y : N
e₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
e₂ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) y : Q) ((g₂ : (a : N) → Q) y : Q)
h₁ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) = (g₂ : (a : N) → Q) (x + y)
h₂ :
  HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
h₃ :
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
h₄ h₅ :
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (x + y) : Q) ((g₂ : (a : N) → Q) (x + y) : Q)

Tactic:
rw [map_add, map_add, e₁, e₂]

Premises used: map_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
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g₁ g₂ : N →ₗ[S] Q
e :
  Eq (α := M →ₗ[R] Q)
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g₁ ∘ₗ
      f)
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g₂ ∘ₗ
      f)
⊢ g₁ = g₂

Tactic:
h.algHom_ext g₁ g₂ (LinearMap.congr_fun e)

Premises used: IsBaseChange.algHom_ext, LinearMap.congr_fun
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
⊢ IsTensorProduct (M := S ⊗[R] M) (mk R S M)

Tactic:
TensorProduct.isTensorProduct R S M

Premises used: TensorProduct.isTensorProduct
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
h :
  Eq (α := S →ₗ[R] M →ₗ[R] S ⊗[R] M)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₃)} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : 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] S ⊗[R] M))) :
            (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
          (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
        ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))
    (mk R S M)
⊢ IsTensorProduct (M₁ := S) (M₂ := M) (M := S ⊗[R] M)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₃)} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : 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] S ⊗[R] M))) :
            (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
          (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
        ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))

Tactic:
convert! TensorProduct.isTensorProduct R S M using 1

Premises used: TensorProduct.isTensorProduct
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
h :
  ∀ (s : S) (x : M),
    Eq (α := S ⊗[R] M)
      (((((↑R :
                      {S M : Type v₃} →
                        {M₂ : Type (max v₁ v₃)} →
                          [inst : Semiring R] →
                            [inst_5 : Semiring S] →
                              [inst_6 : AddCommMonoid M] →
                                [inst_7 : AddCommMonoid M₂] →
                                  [inst_8 : Module R M] →
                                    [inst_9 : Module R M₂] →
                                      [inst_10 : Module S M] →
                                        [inst_11 : 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] S ⊗[R] M))) :
                          (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
                        (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
                      ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
                  (a : S) → M →ₗ[R] S ⊗[R] M)
                s :
              M →ₗ[R] S ⊗[R] M) :
            (a : M) → S ⊗[R] M)
          x :
        S ⊗[R] M)
      ((((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) s : M →ₗ[R] S ⊗[R] M) : (a : M) → S ⊗[R] M) x : S ⊗[R] M)
⊢ Eq (α := S →ₗ[R] M →ₗ[R] S ⊗[R] M)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₃)} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : 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] S ⊗[R] M))) :
            (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
          (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
        ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))
    (mk R S M)

Tactic:
ext s x
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
h : Eq (α := S ⊗[R] M) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] x) (s ⊗ₜ[R] x)
⊢ HSMul.hSMul (β := S ⊗[R] M) s (1 ⊗ₜ[R] x) = s ⊗ₜ[R] x

Tactic:
rw [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
h : HSMul.hSMul (β := S) s 1 = s
⊢ Eq (α := S ⊗[R] M) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] x) (s ⊗ₜ[R] x)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
⊢ HSMul.hSMul (β := S) s 1 = s

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
⊢ HSMul.hSMul (β := S) s 1 = s

Tactic:
exact mul_one _

Premises used: mul_one
-- 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
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
r : S
x : S ⊗[R] M
change :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
⊢ (↑(IsTensorProduct.equiv h) : S ⊗[R] M →ₗ[R] N).toFun (r • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) ((↑(IsTensorProduct.equiv h) : S ⊗[R] M →ₗ[R] N).toFun x)

Tactic:
change h.equiv (r • x) = r • h.equiv x

Premises used: HSMul.hSMul, DFunLike.coe, 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
h : IsBaseChange S f
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
r : S
x : S ⊗[R] M
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- 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
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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
refine_2 :
  ∀ (x : S) (y : M),
    (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r (x ⊗ₜ[R] y)) =
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
refine_3 :
  ∀ (x y : S ⊗[R] M),
    (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
        HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) →
      (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
          HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N) →
        (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
          HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
refine_1₁ : 0 = HSMul.hSMul (β := N) r 0
refine_1₂ refine_1₃ : Eq.{v₂ + 1} (α := N) 0 0
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)

Tactic:
rw [smul_zero, map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- 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
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
r : S
x_1 : S ⊗[R] M
x : S
y : M
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r (x ⊗ₜ[R] y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)

Tactic:
simp [smul_tmul', Algebra.linearMap_apply, smul_comm r x]

Premises used: Algebra.linearMap_apply, TensorProduct.smul_tmul', SMulCommClass.smul_comm
-- 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
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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₁ :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₂ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₃ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₄ :
  HAdd.hAdd (β := N) (HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N))
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₅ refine_3₆ :
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)

Tactic:
rw [map_add, smul_add, map_add, smul_add, hx, hy]

Premises used: map_add, smul_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
f : M →ₗ[R] N
h : IsBaseChange S f
s : S
m : M
⊢ (h.equiv : (a : S ⊗[R] M) → N) (s ⊗ₜ[R] m) = HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl