awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
h : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) x y
of :
  ∀ (x y : ⨂[R] (x : ι), M) (h : Rel R ι M x y),
    (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
refl :
  ∀ (x : ⨂[R] (x : ι), M), (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • x)
symm :
  ∀ {x y : ⨂[R] (x : ι), M},
    AddConGen.Rel (Rel R ι M) x y →
      (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y) →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • x)
trans :
  ∀ {x y z : ⨂[R] (x : ι), M},
    AddConGen.Rel (Rel R ι M) x y →
      AddConGen.Rel (Rel R ι M) y z →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y) →
          (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • z) →
            (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have add : ∀ {w x y z : ⨂[R] (x : ι), M},
  AddConGen.Rel (Rel R ι M) w x →
    AddConGen.Rel (Rel R ι M) y z →
      (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x) →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • z) →
          (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • (w + y)) (r • (x + z))
Tactic: induction h with
  | of x y h => cases h with
    | perm e f =>
      apply isEmpty_or_nonempty ι |>.elim <;> intro h
      · convert! addConGen (Rel R ι M) |>.refl _
      · let i := Nonempty.some h
        classical
        convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl
  | refl => exact AddCon.refl _ _
  | symm => apply AddCon.symm; assumption
  | trans => apply AddCon.trans <;> assumption
  | add => rw [smul_add, smul_add]; apply AddCon.add <;> assumption
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw : Eq (α := Submodule R Sym[R] ι M)
  (Submodule.span R
    (Set.range (ι := (i : ι) → M)
      (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
            (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
        (a : (i : ι) → M) → Sym[R] ι M)))
  ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₁ : Eq (α := Submodule R Sym[R] ι M)
  (Submodule.span R
    (Set.range (ι := (i : ι) → M)
      (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
  ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₂ : Eq (α := Submodule R Sym[R] ι M)
  (Submodule.span R
    (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
      (Set.range (ι := (i : ι) → M)
        (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
  ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₂ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₃ : Eq (α := Submodule R Sym[R] ι M)
  (Submodule.map (mk R ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
  ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₂ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₃ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.map (mk R ι M)
      (Submodule.span R
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₄ : Eq (α := Submodule R Sym[R] ι M) (Submodule.map (mk R ι M) ⊤) ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₂ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₃ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.map (mk R ι M)
      (Submodule.span R
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₄ : Eq (α := Submodule R Sym[R] ι M) (Submodule.map (mk R ι M) ⊤) ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₅ : Eq (α := Submodule R Sym[R] ι M) (LinearMap.range (mk R ι M)) ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₂ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₃ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.map (mk R ι M)
      (Submodule.span R
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₄ : Eq (α := Submodule R Sym[R] ι M) (Submodule.map (mk R ι M) ⊤) ⊤
rw₅ : Eq (α := Submodule R Sym[R] ι M) (LinearMap.range (mk R ι M)) ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤
have rw₆ : Eq (α := Submodule R Sym[R] ι M) ⊤ ⊤
Tactic: rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_11
inst_3 : Semiring S
inst_4 : Algebra R S
m : R ⊗[R] M
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] (TensorProduct.lid R M : (a : R ⊗[R] M) → M) m : S ⊗[R] M)
    ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) m : S ⊗[R] M)
have suffices : ∀ (m : M),
  Eq (α := S ⊗[R] M)
    ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) ∘ₗ
            (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M) :
          (a : M) → S ⊗[R] M)
        m :
      S ⊗[R] M)
    (1 ⊗ₜ[R] m : S ⊗[R] M)
Tactic: suffices ∀ m, (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap).comp
    (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
    simp [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
⊢ Eq (α := M →ₗ[R] R →ₗ[R] M ⊗[R] R)
    (LinearMap.compr₂ₛₗ (mk R M R)
      ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 ∘ₗ lift (LinearMap.flip (LinearMap.lsmul R M))))
    (LinearMap.compr₂ₛₗ (mk R M R) LinearMap.id)
have h : ∀ (x : M),
  Eq (α := M ⊗[R] R)
    ((((LinearMap.compr₂ₛₗ (mk R M R)
                ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 ∘ₗ
                  lift (LinearMap.flip (LinearMap.lsmul R M))) :
              (a : M) → R →ₗ[R] M ⊗[R] R)
            x :
          R →ₗ[R] M ⊗[R] R) :
        (a : R) → M ⊗[R] R)
      1)
    ((((LinearMap.compr₂ₛₗ (mk R M R) LinearMap.id : (a : M) → R →ₗ[R] M ⊗[R] R) x : R →ₗ[R] M ⊗[R] R) :
        (a : R) → M ⊗[R] R)
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M →ₗ[R] R →ₗ[R] M)
    (LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) : M ⊗[R] R →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M))
have h : ∀ (x : M),
  Eq.{u_5 + 1} (α := M)
    ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) : M ⊗[R] R →ₗ[R] M) :
                (a : M) → R →ₗ[R] M)
              x :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) : (a : M) → R →ₗ[R] M) x :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := LinearMap.{u_1, u_1, u_1, u_5} (RingHom.id R) R (M →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) : R ⊗[R] M →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M))
have h : ∀ (x : M),
  Eq (α := M)
    (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) : R ⊗[R] M →ₗ[R] M) :
              (a : R) → M →ₗ[R] M)
            1 :
          (a : M) → M)
        x :
      M)
    (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) : (a : R) → M →ₗ[R] M) 1 :
          (a : M) → M)
        x :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
A : Type u_11
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A M
inst_8 : IsScalarTower R A M
inst_9 : Module A N
inst_10 : IsScalarTower R A N
h : Function.Surjective.{u_1 + 1, u_11 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n))
have obtain : ∀ (r : R),
  Eq (α := M ⊗[R] N) (HSMul.hSMul.{u_11, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) m ⊗ₜ[R] n)
    (m ⊗ₜ[R] HSMul.hSMul.{u_11, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) n)
Tactic: obtain ⟨r, rfl⟩ := h a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] M ⊗[R] (N ⊗[R] P))
    (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
      lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)))
    LinearMap.id
have H : ∀ (x : M) (x_1 : N) (x_2 : P),
  Eq (α := M ⊗[R] (N ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                        (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
                          lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P))) :
                      (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
              x_1 :
            P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
          (a : P) → M ⊗[R] (N ⊗[R] P))
        x_2 :
      M ⊗[R] (N ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P)) LinearMap.id : (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) x) :
                (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
              x_1 :
            P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
          (a : P) → M ⊗[R] (N ⊗[R] P))
        x_2 :
      M ⊗[R] (N ⊗[R] P))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
⊢ Eq (α := M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
    (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
      lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))
    LinearMap.id
have H : ∀ (x : M) (x_1 : N) (x_2 : P),
  Eq (α := M ⊗[R] N ⊗[R] P)
    ((((((compr₂ₛₗ (mk R M N)
                        (compr₂ₛₗ (mk R (M ⊗[R] N) P)
                          (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
                            lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))) :
                      (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                    x :
                  N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
              x_1 :
            P →ₗ[R] M ⊗[R] N ⊗[R] P) :
          (a : P) → M ⊗[R] N ⊗[R] P)
        x_2 :
      M ⊗[R] N ⊗[R] P)
    ((((((compr₂ₛₗ (mk R M N) (compr₂ₛₗ (mk R (M ⊗[R] N) P) LinearMap.id) : (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                    x :
                  N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
              x_1 :
            P →ₗ[R] M ⊗[R] N ⊗[R] P) :
          (a : P) → M ⊗[R] N ⊗[R] P)
        x_2 :
      M ⊗[R] N ⊗[R] P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) ≃ₗ[R] N ⊗[R] (M ⊗[R] P)) (leftComm R M N P)
    (LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
      TensorProduct.assoc R N M P)
have a : Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
  (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
        TensorProduct.assoc R N M P) :
    M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
Tactic: apply LinearEquiv.toLinearMap_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Associator (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
    (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
          TensorProduct.assoc R N M P) :
      M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
have a : ∀ (x : M) (x_1 : N) (x_2 : P),
  Eq (α := N ⊗[R] (M ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                      (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
              x_1 :
            P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
          (a : P) → N ⊗[R] (M ⊗[R] P))
        x_2 :
      N ⊗[R] (M ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                        (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ
                                congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
                              TensorProduct.assoc R N M P) :
                          M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                      (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
              x_1 :
            P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
          (a : P) → N ⊗[R] (M ⊗[R] P))
        x_2 :
      N ⊗[R] (M ⊗[R] P))
Tactic: ext