awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
h : Function.Bijective.{uR + 1, uA + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Bijective (α := B) (β := B ⊗[R] A)
    (Function.comp (β := A ⊗[R] B) (⇑(TensorProduct.comm R A B) : (a : A ⊗[R] B) → B ⊗[R] A)
      (⇑includeRight : (a : B) → A ⊗[R] B))

Tactic:
Algebra.TensorProduct.includeLeft_bijective (S := R) h

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.includeLeft_bijective, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
h : Function.Bijective.{uR + 1, uA + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Bijective (α := B) (β := B ⊗[R] A)
    (Function.comp (β := A ⊗[R] B) (⇑(TensorProduct.comm R A B) : (a : A ⊗[R] B) → B ⊗[R] A)
      (⇑includeRight : (a : B) → A ⊗[R] B))

Tactic:
exact Algebra.TensorProduct.includeLeft_bijective (S := R) h

Premises used: Algebra.TensorProduct.includeLeft_bijective
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
r : R
rw :
  Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 : A ⊗[R] B) (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
rw₂ rw₃ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x : S ⊗[R] S
⊢ AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (HSMul.hSMul (β := S ⊗[R] S) s 0) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := S ⊗[R] S) (LinearMap.toAddHom (LinearMap.mul' R S)) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x : S ⊗[R] S
x_1 x_2 : S
⊢ AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (HSMul.hSMul (β := S ⊗[R] S) s (x_1 ⊗ₜ[R] x_2)) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := S ⊗[R] S) (LinearMap.toAddHom (LinearMap.mul' R S)) (x_1 ⊗ₜ[R] x_2))

Tactic:
simp [TensorProduct.smul_tmul', mul_assoc]

Premises used: mul_assoc, TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x_1 x y : S ⊗[R] S
hx :
  AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (s • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) x)
hy :
  AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (s • y) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) y)
⊢ AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (s • (x + y)) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (LinearMap.mul' R S)) (x + y))

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a₁ a₂ b₁ b₂ : S
⊢ (let __spread.0 : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S;
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ } :
        (a : S ⊗[R] S) → S)
      ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    HMul.hMul (α := S) (β := S)
      ((let __spread.0 : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S;
            { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : S ⊗[R] S →ₗ[S] S } :
            (a : S ⊗[R] S) → S)
          (a₁ ⊗ₜ[R] b₁) :
        S)
      ((let __spread.0 : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S;
            { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : S ⊗[R] S →ₗ[S] S } :
            (a : S ⊗[R] S) → S)
          (a₂ ⊗ₜ[R] b₂) :
        S)

Tactic:
simp [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ Eq.{uS + 1} (α := S)
    ((let __spread.0 : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S;
          { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ } :
          (a : S ⊗[R] S) → S)
        (1 ⊗ₜ[R] 1) :
      S)
    (1 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h :
  ∀ (x : S),
    Eq (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (lmul'' R)) includeRight : (a : S) → S) x : S)
      ((AlgHom.comp (B := S ⊗[R] S)
              (AlgHom.restrictScalars R
                (AlgHom.comp (↑(TensorProduct.lid S S) : S ⊗[S] S →ₐ[S] S) (mapOfCompatibleSMul S R S S S)))
              includeRight :
            (a : S) → S)
          x :
        S)
⊢ Eq (α := S ⊗[R] S →ₐ[S] S) (lmul'' R)
    (AlgHom.comp (↑(TensorProduct.lid S S) : S ⊗[S] S →ₐ[S] S) (mapOfCompatibleSMul S R S S S))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : S
⊢ Eq (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (lmul'' R)) includeRight : (a : S) → S) x : S)
    ((AlgHom.comp (B := S ⊗[R] S)
            (AlgHom.restrictScalars R
              (AlgHom.comp (↑(TensorProduct.lid S S) : S ⊗[S] S →ₐ[S] S) (mapOfCompatibleSMul S R S S S)))
            includeRight :
          (a : S) → S)
        x :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := S ⊗[R] S →ₗ[R] S) (AlgHom.toLinearMap (lmul' R)) (LinearMap.mul' R S)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Quotient.liftOn', AddCon.liftOn, TensorProduct, LinearMap.mul', TensorProduct.lift, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
a b : S
⊢ (lmul' R : (a : S ⊗[R] S) → S) (a ⊗ₜ[R] b) = a * b

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := S →ₐ[R] S) (AlgHom.comp (lmul' R) includeLeft) (AlgHom.id R S)

Tactic:
AlgHom.ext <| mul_one

Premises used: AlgHom.ext, mul_one
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := S →ₐ[R] S) (AlgHom.comp (lmul' R) includeRight) (AlgHom.id R S)

Tactic:
AlgHom.ext <| one_mul

Premises used: AlgHom.ext, one_mul
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
ha :
  ∀ (x : A),
    Eq.{uS + 1} (α := S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
              (includeLeft : A →ₐ[R] A ⊗[R] B) :
            (a : A) → S)
          x :
        S)
      ((AlgHom.comp (B := A ⊗[R] B) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S) (includeLeft : A →ₐ[R] A ⊗[R] B) : (a : A) → S) x :
        S)
hb :
  ∀ (x : B),
    Eq.{uS + 1} (α := S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
              includeRight :
            (a : B) → S)
          x :
        S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (lift f g ⋯ : A ⊗[R] B →ₐ[R] S)) includeRight :
            (a : B) → S)
          x :
        S)
⊢ Eq (α := A ⊗[R] B →ₐ[R] S) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x : A
⊢ Eq.{uS + 1} (α := S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
            (includeLeft : A →ₐ[R] A ⊗[R] B) :
          (a : A) → S)
        x :
      S)
    ((AlgHom.comp (B := A ⊗[R] B) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S) (includeLeft : A →ₐ[R] A ⊗[R] B) : (a : A) → S) x : S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x : B
⊢ Eq.{uS + 1} (α := S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
            includeRight :
          (a : B) → S)
        x :
      S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (lift f g ⋯ : A ⊗[R] B →ₐ[R] S)) includeRight : (a : B) → S)
        x :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x : S ⊗[R] S
⊢ Eq (α := S ⊗[R] S) ((AlgHom.comp includeLeft (lmul'' R) : (a : S ⊗[R] S) → S ⊗[R] S) 0)
    ((AlgHom.id S (S ⊗[R] S) : (a : S ⊗[R] S) → S ⊗[R] S) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] S) ((y • x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₂ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] HSMul.hSMul (β := S) y 1) (x ⊗ₜ[R] y)
rw₃ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] (y * 1)) (x ⊗ₜ[R] y)
rw₄ rw₅ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] y) (x ⊗ₜ[R] y)
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)

Tactic:
rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul, mul_comm, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x x_1 x_2 : S ⊗[R] S
hx :
  Eq (α := S ⊗[R] S) ((AlgHom.comp includeLeft (lmul'' R) : (a : S ⊗[R] S) → S ⊗[R] S) x_1 : S ⊗[R] S)
    ((AlgHom.id S (S ⊗[R] S) : (a : S ⊗[R] S) → S ⊗[R] S) x_1 : S ⊗[R] S)
hy :
  Eq (α := S ⊗[R] S) ((AlgHom.comp includeLeft (lmul'' R) : (a : S ⊗[R] S) → S ⊗[R] S) x_2 : S ⊗[R] S)
    ((AlgHom.id S (S ⊗[R] S) : (a : S ⊗[R] S) → S ⊗[R] S) x_2 : S ⊗[R] S)
⊢ Eq (α := S ⊗[R] S) ((AlgHom.comp includeLeft (lmul'' R) : (a : S ⊗[R] S) → S ⊗[R] S) (x_1 + x_2) : S ⊗[R] S)
    ((AlgHom.id S (S ⊗[R] S) : (a : S ⊗[R] S) → S ⊗[R] S) (x_1 + x_2) : S ⊗[R] S)

Tactic:
simp_all [add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CompatibleSMul R S S S
h :
  ∀ (x : S),
    Eq (α := S)
      ((AlgHom.comp (AlgHom.restrictScalars R (↑(lmulEquiv R S) : S ⊗[R] S →ₐ[S] S)) includeRight : (a : S) → S) x : S)
      ((AlgHom.comp (B := S ⊗[R] S) (AlgHom.restrictScalars R (↑(lidOfCompatibleSMul R S S) : S ⊗[R] S →ₐ[S] S))
              includeRight :
            (a : S) → S)
          x :
        S)
⊢ Eq (α := S ⊗[R] S →ₐ[S] S) (↑(lmulEquiv R S) : S ⊗[R] S →ₐ[S] S) (↑(lidOfCompatibleSMul R S S) : S ⊗[R] S →ₐ[S] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CompatibleSMul R S S S
x : S
⊢ Eq (α := S)
    ((AlgHom.comp (AlgHom.restrictScalars R (↑(lmulEquiv R S) : S ⊗[R] S →ₐ[S] S)) includeRight : (a : S) → S) x : S)
    ((AlgHom.comp (B := S ⊗[R] S) (AlgHom.restrictScalars R (↑(lidOfCompatibleSMul R S S) : S ⊗[R] S →ₐ[S] S))
            includeRight :
          (a : S) → S)
        x :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
ha :
  ∀ (x : A),
    Eq.{uS + 1} (α := S) (((productMap f g).comp includeLeft : (a : A) → S) x : S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
              (includeLeft : A →ₐ[R] A ⊗[R] B) :
            (a : A) → S)
          x :
        S)
hb :
  ∀ (x : B),
    Eq.{uS + 1} (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (productMap f g)) includeRight : (a : B) → S) x : S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
              includeRight :
            (a : B) → S)
          x :
        S)
⊢ productMap f g = AlgHom.comp (lmul' R) (map f g)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x : A
⊢ Eq.{uS + 1} (α := S) (((productMap f g).comp includeLeft : (a : A) → S) x : S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
            (includeLeft : A →ₐ[R] A ⊗[R] B) :
          (a : A) → S)
        x :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x : B
⊢ Eq.{uS + 1} (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (productMap f g)) includeRight : (a : B) → S) x : S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
            includeRight :
          (a : B) → S)
        x :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
b : B
⊢ (productMap f g : (a : A ⊗[R] B) → S) (a ⊗ₜ[R] b) =
    HMul.hMul (α := S) (β := S) ((f : (a : A) → S) a : S) ((g : (a : B) → S) b : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
⊢ Eq.{uS + 1} (α := S) ((productMap f g : (a : A ⊗[R] B) → S) (a ⊗ₜ[R] 1) : S) ((f : (a : A) → S) a : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (productMap f g).comp includeLeft = f

Tactic:
lift_comp_includeLeft _ _ (fun _ _ => Commute.all _ _)

Premises used: Algebra.TensorProduct.lift_comp_includeLeft, Algebra.TensorProduct.algHomOfLinearMapTensorProduct, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, Algebra.TensorProduct.productMap
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
b : B
⊢ Eq.{uS + 1} (α := S) ((productMap f g : (a : A ⊗[R] B) → S) (1 ⊗ₜ[R] b) : S) ((g : (a : B) → S) b : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (productMap f g).comp includeRight = g

Tactic:
lift_comp_includeRight _ _ (fun _ _ => Commute.all _ _)

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Quotient.liftOn', AddCon.liftOn, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, Algebra.TensorProduct.lift_comp_includeRight, MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, Algebra.TensorProduct.productMap, TensorProduct
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
rw : AlgHom.range (A := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) = f.range ⊔ g.range
rw₁ : Subalgebra.map (lmul' R) (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] S ⊗[R] S)) = f.range ⊔ g.range
rw₂ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₃ :
  Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeLeft f)) ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₄ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      Subalgebra.map (lmul' R) (AlgHom.range (AlgHom.comp includeRight g)) =
    f.range ⊔ g.range
rw₅ :
  (AlgHom.comp (lmul' R) (AlgHom.comp includeLeft f)).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₆ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (lmul' R) (AlgHom.comp includeRight g)).range =
    f.range ⊔ g.range
rw₇ :
  (AlgHom.comp (AlgHom.comp (lmul' R) includeLeft) f).range ⊔
      (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range =
    f.range ⊔ g.range
rw₈ :
  (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.comp (lmul' R) includeRight) g).range = f.range ⊔ g.range
rw₉ : (AlgHom.comp (AlgHom.id R S) f).range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
rw₁₀ : f.range ⊔ (AlgHom.comp (AlgHom.id R S) g).range = f.range ⊔ g.range
rw₁₁ rw₁₂ : f.range ⊔ g.range = f.range ⊔ g.range
⊢ (productMap f g).range = f.range ⊔ g.range

Tactic:
rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]

Premises used: Algebra.map_sup, AlgHom.comp_assoc, AlgHom.id_comp, Algebra.TensorProduct.productMap_eq_comp_map, Algebra.TensorProduct.lmul'_comp_includeRight, Algebra.TensorProduct.map_range, Algebra.TensorProduct.lmul'_comp_includeLeft, AlgHom.range_comp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
⊢ ∀ (x y : A),
    HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N) (x + y) (baseChangeHom R A M N) =
      HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N) x (baseChangeHom R A M N) +
        HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N) y (baseChangeHom R A M N)

Tactic:
simp only [add_smul, forall_true_iff]

Premises used: add_smul, forall_true_iff
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
⊢ ∀ (m x : A),
    HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N) (m • x) (baseChangeHom R A M N) =
      HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) m : A)
        (HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N) x (baseChangeHom R A M N))

Tactic:
simp only [smul_assoc, RingHom.id_apply, forall_true_iff]

Premises used: RingHom.id_apply, smul_assoc, forall_true_iff