awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have refine_1 : ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
        ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
      (a : ↥⊥ ⊗[R] ↥A) → ↥A)
    (HMul.hMul (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥) y ⊗ₜ[R] (a * b)) =
  HMul.hMul (α := ↥A) (β := ↥A)
    (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥⊥ ⊗[R] ↥A) → ↥A)
        ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' ⊗ₜ[R] a) :
      ↥A)
    (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥⊥ ⊗[R] ↥A) → ↥A)
        (y ⊗ₜ[R] b) :
      ↥A)
Tactic: rw [← hx, ← hy, ← map_mul, (toSubmodule A).lTensorOne_tmul x' a,
      (toSubmodule A).lTensorOne_tmul y' b, (toSubmodule A).lTensorOne_tmul (x' * y') (a * b),
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
⊢ ↥A ⊗[R] ↥⊥ ≃ₐ[R] ↥A
have refine_1 : ∀ (a₁ a₂ : ↥A) (b₁ b₂ : ↥⊥),
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a₁ ⊗ₜ[R] b₁) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a₂ ⊗ₜ[R] b₂) :
        ↥A)
Tactic: refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).rTensorOne ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
refine_1 :
  ∀ (a₁ a₂ : ↥A) (b₁ b₂ : ↥⊥),
    ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥A ⊗[R] ↥⊥) → ↥A)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := ↥A) (β := ↥A)
        (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥A ⊗[R] ↥⊥) → ↥A)
            (a₁ ⊗ₜ[R] b₁) :
          ↥A)
        (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥A ⊗[R] ↥⊥) → ↥A)
            (a₂ ⊗ₜ[R] b₂) :
          ↥A)
⊢ ↥A ⊗[R] ↥⊥ ≃ₐ[R] ↥A
have refine_2 : Eq.{u_2 + 1} (α := ↥A)
  (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      (1 ⊗ₜ[R] 1) :
    ↥A)
  (1 : ↥A)
Tactic: refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).rTensorOne ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
have refine_1 : ∀ (x' : R) (hx : (algebraMap R S : (a : R) → S) x' = (↑x : S)),
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
Tactic: obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R S : (a : R) → S) x' = (↑x : S)
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
have hx₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
Tactic: replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
have refine_1 : ∀ (y' : R) (hy : (algebraMap R S : (a : R) → S) y' = (↑y : S)),
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
Tactic: obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R S : (a : R) → S) y' = (↑y : S)
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
have hy₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
Tactic: replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
have refine_1 : ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
      (a : ↥A ⊗[R] ↥⊥) → ↥A)
    ((a * b) ⊗ₜ[R] HMul.hMul (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥) y) =
  HMul.hMul (α := ↥A) (β := ↥A)
    (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥A ⊗[R] ↥⊥) → ↥A)
        (a ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x') :
      ↥A)
    (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥A ⊗[R] ↥⊥) → ↥A)
        (b ⊗ₜ[R] y) :
      ↥A)
Tactic: rw [← hx, ← hy, ← map_mul, (toSubmodule A).rTensorOne_tmul x' a,
      (toSubmodule A).rTensorOne_tmul y' b, (toSubmodule A).rTensorOne_tmul (x' * y') (a * b),
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
⊢ Eq (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    (((_root_.TensorProduct.map (LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft))
              (LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight)) :
            S ⊗[R] T →ₗ[R] ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight)) :
          (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range)
        (HMul.hMul (α := S ⊗[R] T)
          (↑(Subtype.mk (p := fun (x : S ⊗[R] T) ↦
                Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeLeft) x) (x ⊗ₜ[R] 1) ⋯) :
            S ⊗[R] T)
          (↑(Subtype.mk (p := fun (x : S ⊗[R] T) ↦
                Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeRight) x) (1 ⊗ₜ[R] y) ⋯) :
            S ⊗[R] T)) :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    (Subtype.mk (p := fun (x : S ⊗[R] T) ↦ Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeLeft) x)
          (x ⊗ₜ[R] 1) ⋯ ⊗ₜ[R]
        Subtype.mk (p := fun (x : S ⊗[R] T) ↦
          Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeRight) x) (1 ⊗ₜ[R] y) ⋯ :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
have rw : Eq (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
  (((LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft) :
            S →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeLeft))) :
          (a : S) → ↥includeLeft.range)
        x ⊗ₜ[R]
      ((LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight) :
            T →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeRight))) :
          (a : T) → ↥includeRight.range)
        y :
    ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
  (Subtype.mk (p := fun (x : S ⊗[R] T) ↦ Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeLeft) x)
        (x ⊗ₜ[R] 1) sorry ⊗ₜ[R]
      Subtype.mk (p := fun (x : S ⊗[R] T) ↦ Membership.mem (γ := Subalgebra R (S ⊗[R] T)) (AlgHom.range includeRight) x)
        (1 ⊗ₜ[R] y) sorry :
    ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
Tactic: rw [tmul_mul_tmul, mul_one, one_mul, _root_.TensorProduct.map_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
⊢ Eq (α := S ⊗[R] T)
    (((Submodule.mulMap (LinearMap.range (AlgHom.toLinearMap includeLeft))
                (LinearMap.range (AlgHom.toLinearMap includeRight)) :
              ↥(LinearMap.range (AlgHom.toLinearMap includeLeft)) ⊗[R]
                  ↥(LinearMap.range (AlgHom.toLinearMap includeRight)) →ₗ[R]
                S ⊗[R] T) ∘ₗ
            _root_.TensorProduct.map (LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft))
              (LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight)) :
          (a : S ⊗[R] T) → S ⊗[R] T)
        (x ⊗ₜ[R] y) :
      S ⊗[R] T)
    ((LinearMap.id : (a : S ⊗[R] T) → S ⊗[R] T) (x ⊗ₜ[R] y) : S ⊗[R] T)
have rw : Eq (α := S ⊗[R] T)
  (((Submodule.mulMap (LinearMap.range (AlgHom.toLinearMap includeLeft))
            (LinearMap.range (AlgHom.toLinearMap includeRight)) :
          ↥(LinearMap.range (AlgHom.toLinearMap includeLeft)) ⊗[R]
              ↥(LinearMap.range (AlgHom.toLinearMap includeRight)) →ₗ[R]
            S ⊗[R] T) :
        (a : ↥includeLeft.range ⊗[R] ↥includeRight.range) → S ⊗[R] T)
      (((LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft) :
              S →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeLeft))) :
            (a : S) → ↥includeLeft.range)
          x ⊗ₜ[R]
        ((LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight) :
              T →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeRight))) :
            (a : T) → ↥includeRight.range)
          y) :
    S ⊗[R] T)
  (x ⊗ₜ[R] y : S ⊗[R] T)
Tactic: rw [LinearMap.comp_apply, LinearMap.id_apply, _root_.TensorProduct.map_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
⊢ HMul.hMul (α := S ⊗[R] T) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y
have rw : Eq (α := S ⊗[R] T) ((x * 1) ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
Tactic: rw [tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
rw : Eq (α := S ⊗[R] T) ((x * 1) ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
⊢ HMul.hMul (α := S ⊗[R] T) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y
have rw₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
Tactic: rw [tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
rw : Eq (α := S ⊗[R] T) ((x * 1) ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
⊢ HMul.hMul (α := S ⊗[R] T) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y
have rw₂ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] y) (x ⊗ₜ[R] y)
Tactic: rw [tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
⊢ AlgHom.comp ((map f A).mulMap (map f B))
      (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)
have ha : ∀ (x : ↥A),
  Eq.{u_3 + 1} (α := T)
    ((AlgHom.comp
            (AlgHom.comp ((map f A).mulMap (map f B))
                (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) :
              AlgHom.{u_1, u_2, u_3} R (↥A ⊗[R] ↥B) T)
            (Algebra.TensorProduct.includeLeft : ↥A →ₐ[R] ↥A ⊗[R] ↥B) :
          (a : ↥A) → T)
        x :
      T)
    (((f.comp (A.mulMap B)).comp Algebra.TensorProduct.includeLeft : (a : ↥A) → T) x : T)
Tactic: ext