awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f_3 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf_2 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_3)
g_3 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_2 : IsTensorProduct g_3
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
⊢ ∀ (c : S) (m : M₁) (n : M₂),
    (fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m (c • n) =
      HSMul.hSMul (β := M₁₂) c
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m n)

Tactic:
simp [h₂]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
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 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
T : Type u_16
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Module T M₁
inst_24 : IsScalarTower R T M₁
inst_25 : Module T M₁₂
inst_26 : SMulCommClass S T M₁₂
inst_27 : IsScalarTower R T M₁₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁ ⊗[R] M₂₃)
    (((assocOfMapSMul f hf g hg h₁ h₂ : M₁₂ ⊗[S] M₃ ≃ₗ[T] M₁ ⊗[R] M₂₃) : (a : M₁₂ ⊗[S] M₃) → M₁ ⊗[R] M₂₃)
        ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x₁ : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) x₂ ⊗ₜ[S] x₃) :
      M₁ ⊗[R] M₂₃)
    (x₁ ⊗ₜ[R] (((g : (a : M₂) → M₃ →ₗ[S] M₂₃) x₂ : M₃ →ₗ[S] M₂₃) : (a : M₃) → M₂₃) x₃ : M₁ ⊗[R] M₂₃)

Tactic:
IsTensorProduct.assoc_tmul ..

Premises used: IsTensorProduct.assoc_tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
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 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
T : Type u_16
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Module T M₁
inst_24 : IsScalarTower R T M₁
inst_25 : Module T M₁₂
inst_26 : SMulCommClass S T M₁₂
inst_27 : IsScalarTower R T M₁₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁₂ ⊗[S] M₃)
    (((LinearEquiv.symm (assocOfMapSMul f hf g hg h₁ h₂) : M₁ ⊗[R] M₂₃ ≃ₗ[T] M₁₂ ⊗[S] M₃) :
          (a : M₁ ⊗[R] M₂₃) → M₁₂ ⊗[S] M₃)
        (x₁ ⊗ₜ[R] (((g : (a : M₂) → M₃ →ₗ[S] M₂₃) x₂ : M₃ →ₗ[S] M₂₃) : (a : M₃) → M₂₃) x₃) :
      M₁₂ ⊗[S] M₃)
    ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x₁ : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) x₂ ⊗ₜ[S] x₃ : M₁₂ ⊗[S] M₃)

Tactic:
IsTensorProduct.assoc_symm_tmul ..

Premises used: IsTensorProduct.assoc_symm_tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M
inst_8 : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e : M ≃ₗ[R] M'
rw :
  Function.Bijective (α := M₁ ⊗[R] M₂) (β := M') (⇑((↑e : M →ₗ[R] M') ∘ₗ TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M')
⊢ Function.Bijective (α := M₁ ⊗[R] M₂) (β := M')
    (⇑(TensorProduct.lift (f.compr₂ (↑e : M →ₗ[R] M'))) : (a : M₁ ⊗[R] M₂) → M')

Tactic:
rw [TensorProduct.lift_compr₂]

Premises used: TensorProduct.lift_compr₂
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M
inst_8 : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e : M ≃ₗ[R] M'
⊢ Function.Bijective (α := M₁ ⊗[R] M₂) (β := M') (⇑((↑e : M →ₗ[R] M') ∘ₗ TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M')

Tactic:
e.bijective.comp ist

Premises used: LinearEquiv.bijective, Function.Bijective.comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M
inst_8 : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e : M ≃ₗ[R] M'
⊢ Function.Bijective (α := M₁ ⊗[R] M₂) (β := M') (⇑((↑e : M →ₗ[R] M') ∘ₗ TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M')

Tactic:
exact e.bijective.comp ist

Premises used: LinearEquiv.bijective, Function.Bijective.comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : Module R N₁
inst_10 : Module R N₂
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
rw :
  Function.Bijective (α := N₁ ⊗[R] N₂) (β := M)
    (⇑(TensorProduct.lift f ∘ₗ LinearMap.rTensor M₂ (↑e₁ : N₁ →ₗ[R] M₁) ∘ₗ LinearMap.lTensor N₁ (↑e₂ : N₂ →ₗ[R] M₂)) :
      (a : N₁ ⊗[R] N₂) → M)
⊢ Function.Bijective (α := N₁ ⊗[R] N₂) (β := M)
    (⇑(TensorProduct.lift ((f ∘ₗ (↑e₁ : N₁ →ₗ[R] M₁)).compl₂ (↑e₂ : N₂ →ₗ[R] M₂))) : (a : N₁ ⊗[R] N₂) → M)

Tactic:
rw [← TensorProduct.lift_comp_map, ← LinearMap.rTensor_comp_lTensor]

Premises used: LinearMap.rTensor_comp_lTensor, TensorProduct.lift_comp_map
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : Module R N₁
inst_10 : Module R N₂
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective (α := N₁ ⊗[R] N₂) (β := M)
    (⇑(TensorProduct.lift f ∘ₗ LinearMap.rTensor M₂ (↑e₁ : N₁ →ₗ[R] M₁) ∘ₗ LinearMap.lTensor N₁ (↑e₂ : N₂ →ₗ[R] M₂)) :
      (a : N₁ ⊗[R] N₂) → M)

Tactic:
ist.comp ((e₁.rTensor M₂).bijective.comp (e₂.lTensor N₁).bijective)

Premises used: LinearEquiv.bijective, Quotient.liftOn', AddCon.liftOn, LinearEquiv.rTensor, LinearEquiv.lTensor, Function.Bijective.comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : Module R N₁
inst_10 : Module R N₂
ist : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M) (⇑(TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective (α := N₁ ⊗[R] N₂) (β := M)
    (⇑(TensorProduct.lift f ∘ₗ LinearMap.rTensor M₂ (↑e₁ : N₁ →ₗ[R] M₁) ∘ₗ LinearMap.lTensor N₁ (↑e₂ : N₂ →ₗ[R] M₂)) :
      (a : N₁ ⊗[R] N₂) → M)

Tactic:
exact ist.comp ((e₁.rTensor M₂).bijective.comp (e₂.lTensor N₁).bijective)

Premises used: LinearEquiv.bijective, LinearEquiv.rTensor, LinearEquiv.lTensor, Function.Bijective.comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
inst_7 : AddCommMonoid N₁
inst_8 : Module R N₁
ist : IsTensorProduct f
e₁ : N₁ ≃ₗ[R] M₁
⊢ IsTensorProduct (f ∘ₗ (↑e₁ : N₁ →ₗ[R] M₁))

Tactic:
ist.compl₂_comp_linearEquiv e₁ (LinearEquiv.refl R M₂)

Premises used: IsTensorProduct.compl₂_comp_linearEquiv, LinearEquiv.refl, LinearMap.compl₂
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₂ : Type u_7
inst_7 : AddCommMonoid N₂
inst_8 : Module R N₂
ist : IsTensorProduct f
e₂ : N₂ ≃ₗ[R] M₂
⊢ IsTensorProduct (f.compl₂ (↑e₂ : N₂ →ₗ[R] M₂))

Tactic:
ist.compl₂_comp_linearEquiv (LinearEquiv.refl R M₁) e₂

Premises used: IsTensorProduct.compl₂_comp_linearEquiv, LinearEquiv.refl
-- 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
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 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] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
⊢ ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)

Tactic:
have hF : ∀ (s : S) (m : M), h.lift F (s • f m) = s • g m := h.lift_eq F
-- 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
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 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] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
zero :
  (IsTensorProduct.lift h F : (a : N) → Q) 0 = HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)
zero₁ : 0 = HSMul.hSMul (β := Q) r 0
zero₂ zero₃ : Eq.{u_3 + 1} (α := Q) 0 0
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) r 0) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)

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
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 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] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
s : S
m : M
tmul :
  (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) (r * s) ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
tmul₁ :
  HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
tmul₂ : HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) = r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
tmul₃ tmul₄ :
  r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q) = r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)

Tactic:
rw [← mul_smul, hF, hF, mul_smul]

Premises used: SemigroupAction.mul_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
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
⊢ ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)

Tactic:
have hF : ∀ (s : S) (m : M), h.lift g (s • f m) = s • g m := h.lift_eq _
-- 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 : M →ₗ[R] Q
x : M
hF :
  ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
⊢ (h.lift g : (a : N) → Q) (HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)) =
    HSMul.hSMul.{v₃, u_3, u_3} (α := S) (β := Q) 1 ((g : (a : M) → Q) x : Q)

Tactic:
hF 1 x

Premises used: OfNat.ofNat
-- 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 : M →ₗ[R] Q
x : M
hF :
  ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
h₁ : (f : (a : M) → N) x = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)
h₂ : (g : (a : M) → Q) x = HSMul.hSMul.{v₃, u_3, u_3} (α := S) (β := Q) 1 ((g : (a : M) → Q) x : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((h.lift g : (a : N) → Q) ((f : (a : M) → N) x : N) : Q) ((g : (a : M) → Q) x : Q)

Tactic:
convert! hF 1 x

Premises used: OfNat.ofNat
-- 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 : M →ₗ[R] Q
x : M
hF :
  ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
h₁ h₂ : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ (f : (a : M) → N) x = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)

Tactic:
rw [one_smul]

Premises used: one_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
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF :
  ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
h₁ h₂ : Eq.{u_3 + 1} (α := Q) ((g : (a : M) → Q) x : Q) ((g : (a : M) → Q) x : Q)
⊢ (g : (a : M) → Q) x = HSMul.hSMul.{v₃, u_3, u_3} (α := S) (β := Q) 1 ((g : (a : M) → Q) x : Q)

Tactic:
rw [one_smul]

Premises used: one_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
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g : 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₂)
        (h.lift g) ∘ₗ
      f =
    g

Tactic:
LinearMap.ext (h.lift_eq g)

Premises used: LinearMap.ext, IsBaseChange.lift_eq