awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
refine_1 :
  ∀ (x' : R) (hx : (algebraMap R S : (a : R) → S) x' = (↑x : S)),
    ((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)
⊢ ((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)

Tactic:
obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 S : (a : R) → S) x' = (↑x : S)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x

Tactic:
replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
refine_1 :
  ∀ (y' : R) (hy : (algebraMap R S : (a : R) → S) y' = (↑y : S)),
    ((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)
⊢ ((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)

Tactic:
obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 S : (a : R) → S) y' = (↑y : S)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y

Tactic:
replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
⊢ Eq.{u_2 + 1} (α := ↥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)
        (1 ⊗ₜ[R] 1) :
      ↥A)
    (1 : ↥A)

Tactic:
Submodule.lTensorOne_one_tmul _

Premises used: Set.Mem, Subsemiring.copy, Submodule.lTensorOne_one_tmul, AlgHom.range, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
⊢ Eq.{u_2 + 1} (α := ↥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)
        (1 ⊗ₜ[R] 1) :
      ↥A)
    (1 : ↥A)

Tactic:
exact Submodule.lTensorOne_one_tmul _

Premises used: Submodule.lTensorOne_one_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
x : R
a : ↥A
⊢ (A.lTensorBot : (a : ↥⊥ ⊗[R] ↥A) → ↥A) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] a) = x • a

Tactic:
(toSubmodule A).lTensorOne_tmul x a

Premises used: Set.Mem, Submodule.lTensorOne_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
a : ↥A
⊢ (A.lTensorBot : (a : ↥⊥ ⊗[R] ↥A) → ↥A) (1 ⊗ₜ[R] a) = a

Tactic:
(toSubmodule A).lTensorOne_one_tmul a

Premises used: Set.Mem, Submodule.lTensorOne_one_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
a : ↥A
⊢ Eq (α := ↥⊥ ⊗[R] ↥A) ((A.lTensorBot.symm : (a : ↥A) → ↥⊥ ⊗[R] ↥A) a : ↥⊥ ⊗[R] ↥A) (1 ⊗ₜ[R] a : ↥⊥ ⊗[R] ↥A)

Tactic:
rfl

Premises used: Set.Mem, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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)
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)
⊢ ↥A ⊗[R] ↥⊥ ≃ₐ[R] ↥A

Tactic:
refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).rTensorOne ?_ ?_

Premises used: Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 : ↥⊥
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)
⊢ ((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

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x

Tactic:
replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
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)
⊢ ((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

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y

Tactic:
replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
⊢ 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:
Submodule.rTensorOne_tmul_one _

Premises used: Set.Mem, Submodule.rTensorOne_tmul_one, Subsemiring.copy, AlgHom.range, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
⊢ 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:
exact Submodule.rTensorOne_tmul_one _

Premises used: Submodule.rTensorOne_tmul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
x : R
a : ↥A
⊢ (A.rTensorBot : (a : ↥A ⊗[R] ↥⊥) → ↥A) (a ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) = x • a

Tactic:
(toSubmodule A).rTensorOne_tmul x a

Premises used: Set.Mem, Submodule.rTensorOne_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
a : ↥A
⊢ (A.rTensorBot : (a : ↥A ⊗[R] ↥⊥) → ↥A) (a ⊗ₜ[R] 1) = a

Tactic:
(toSubmodule A).rTensorOne_tmul_one a

Premises used: Set.Mem, Submodule.rTensorOne_tmul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
a : ↥A
⊢ Eq (α := ↥A ⊗[R] ↥⊥) ((A.rTensorBot.symm : (a : ↥A) → ↥A ⊗[R] ↥⊥) a : ↥A ⊗[R] ↥⊥) (a ⊗ₜ[R] 1 : ↥A ⊗[R] ↥⊥)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ AlgEquiv.trans (Algebra.TensorProduct.comm R ↥A ↥⊥) A.lTensorBot = A.rTensorBot

Tactic:
AlgEquiv.toLinearEquiv_injective (toSubmodule A).comm_trans_lTensorOne

Premises used: Submodule.comm_trans_lTensorOne, Subalgebra.toSubmodule, AlgEquiv.toLinearEquiv_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ AlgEquiv.trans (Algebra.TensorProduct.comm R ↥⊥ ↥A) A.rTensorBot = A.lTensorBot

Tactic:
AlgEquiv.toLinearEquiv_injective (toSubmodule A).comm_trans_rTensorOne

Premises used: Submodule.comm_trans_rTensorOne, Subalgebra.toSubmodule, AlgEquiv.toLinearEquiv_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 (α := ↥(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) ⋯ ⊗ₜ[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))
⊢ 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))

Tactic:
rw [tmul_mul_tmul, mul_one, one_mul, _root_.TensorProduct.map_tmul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.map_tmul, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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))
    (((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) ⋯ ⊗ₜ[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))

Tactic:
rfl