awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁
z : M₂
this :
  HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z : M₁₂) =
    (((f : (a : M₁) → M₂ →ₗ[S] M₁₂) (t • x) : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁ ⊗[R] M₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁ ⊗[R] M₂
tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁ ⊗[R] M₂
tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
tmul₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂ ⊗[S] M₃
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have zero : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y =>
    obtain ⟨x, rfl⟩ := hf.equiv.surjective x
    induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂ ⊗[S] M₃
zero : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have add : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y =>
    obtain ⟨x, rfl⟩ := hf.equiv.surjective x
    induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂ ⊗[S] M₃
zero : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
add : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y =>
    obtain ⟨x, rfl⟩ := hf.equiv.surjective x
    induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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')
    (⇑(TensorProduct.lift (f.compr₂ (↑e : M →ₗ[R] M'))) : (a : M₁ ⊗[R] M₂) → M')
have rw : Function.Bijective (α := M₁ ⊗[R] M₂) (β := M') (⇑((↑e : M →ₗ[R] M') ∘ₗ TensorProduct.lift f) : (a : M₁ ⊗[R] M₂) → M')
Tactic: rw [TensorProduct.lift_compr₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 ∘ₗ (↑e₁ : N₁ →ₗ[R] M₁)).compl₂ (↑e₂ : N₂ →ₗ[R] M₂))) : (a : N₁ ⊗[R] N₂) → M)
have 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)
Tactic: rw [← TensorProduct.lift_comp_map, ← LinearMap.rTensor_comp_lTensor]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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)
⊢ (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)
have zero : (IsTensorProduct.lift h F : (a : N) → Q) 0 = HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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)
⊢ (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)
have zero₁ : 0 = HSMul.hSMul (β := Q) r 0
Tactic: rw [smul_zero, map_zero, smul_zero]