awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
f₁ : A ≃ₐ[S] C
f₂ : C ≃ₐ[S] E
g₁ : B ≃ₐ[R] D
g₂ : D ≃ₐ[R] F
⊢ Eq (α := A ⊗[R] B ≃ₐ[S] E ⊗[R] F) (congr (f₁.trans f₂) (g₁.trans g₂) : A ⊗[R] B ≃ₐ[S] E ⊗[R] F)
    (AlgEquiv.trans (A₂ := C ⊗[R] D) (congr f₁ g₁ : A ⊗[R] B ≃ₐ[S] C ⊗[R] D) (congr f₂ g₂ : C ⊗[R] D ≃ₐ[S] E ⊗[R] F) :
      A ⊗[R] B ≃ₐ[S] E ⊗[R] F)

Tactic:
AlgEquiv.coe_algHom_injective <| map_comp f₂.toAlgHom f₁.toAlgHom g₂.toAlgHom g₁.toAlgHom

Premises used: Algebra.TensorProduct.map_comp, AlgEquiv.toAlgHom, AlgEquiv.coe_algHom_injective
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
f : A ≃ₐ[S] C
g : B ≃ₐ[R] D
⊢ Eq (α := C ⊗[R] D ≃ₐ[S] A ⊗[R] B) (congr f.symm g.symm : C ⊗[R] D ≃ₐ[S] A ⊗[R] B)
    (AlgEquiv.symm (congr f g) : C ⊗[R] D ≃ₐ[S] A ⊗[R] B)

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofAlgHom, Algebra.TensorProduct.congr, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
m : A
n : B
p : C
⊢ Eq (α := B ⊗[R] (A ⊗[R] C))
    ((leftComm R A B C : (a : A ⊗[R] (B ⊗[R] C)) → B ⊗[R] (A ⊗[R] C)) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) : B ⊗[R] (A ⊗[R] C))
    (n ⊗ₜ[R] (m ⊗ₜ[R] p) : B ⊗[R] (A ⊗[R] C))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
m : A
n : B
p : C
⊢ Eq (α := A ⊗[R] (B ⊗[R] C))
    ((AlgEquiv.symm (leftComm R A B C) : (a : B ⊗[R] (A ⊗[R] C)) → A ⊗[R] (B ⊗[R] C)) (n ⊗ₜ[R] (m ⊗ₜ[R] p)) :
      A ⊗[R] (B ⊗[R] C))
    (m ⊗ₜ[R] (n ⊗ₜ[R] p) : A ⊗[R] (B ⊗[R] C))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
a :
  ∀ (x : A) (x_1 : B) (x_2 : C),
    Eq (α := B ⊗[R] (A ⊗[R] C))
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              (↑(↑(leftComm R A B C) : A ⊗[R] (B ⊗[R] C) ≃ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                                A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                            A →ₗ[R] B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                          (a : A) → B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                        x) :
                    B →ₗ[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                  (a : B) → C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                x_1 :
              C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
            (a : C) → B ⊗[R] (A ⊗[R] C))
          x_2 :
        B ⊗[R] (A ⊗[R] C))
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              (↑(_root_.TensorProduct.leftComm R A B C) : A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                            A →ₗ[R] B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                          (a : A) → B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                        x) :
                    B →ₗ[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                  (a : B) → C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                x_1 :
              C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
            (a : C) → B ⊗[R] (A ⊗[R] C))
          x_2 :
        B ⊗[R] (A ⊗[R] C))
⊢ Eq (α := A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C))
    (↑(↑(leftComm R A B C) : A ⊗[R] (B ⊗[R] C) ≃ₗ[R] B ⊗[R] (A ⊗[R] C)) : A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C))
    (↑(_root_.TensorProduct.leftComm R A B C) : A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
x : A
x_1 : B
x_2 : C
⊢ Eq (α := B ⊗[R] (A ⊗[R] C))
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (↑(↑(leftComm R A B C) : A ⊗[R] (B ⊗[R] C) ≃ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                              A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                          A →ₗ[R] B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                        (a : A) → B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                      x) :
                  B →ₗ[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                (a : B) → C →ₗ[R] B ⊗[R] (A ⊗[R] C))
              x_1 :
            C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
          (a : C) → B ⊗[R] (A ⊗[R] C))
        x_2 :
      B ⊗[R] (A ⊗[R] C))
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (↑(_root_.TensorProduct.leftComm R A B C) : A ⊗[R] (B ⊗[R] C) →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                          A →ₗ[R] B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                        (a : A) → B ⊗[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C))
                      x) :
                  B →ₗ[R] C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
                (a : B) → C →ₗ[R] B ⊗[R] (A ⊗[R] C))
              x_1 :
            C →ₗ[R] B ⊗[R] (A ⊗[R] C)) :
          (a : C) → B ⊗[R] (A ⊗[R] C))
        x_2 :
      B ⊗[R] (A ⊗[R] C))

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
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra T A
inst_18 : IsScalarTower R T A
inst_19 : SMulCommClass S T A
inst_20 : Algebra S T
inst_21 : IsScalarTower S T A
inst_22 : CommSemiring R'
inst_23 : Algebra R R'
inst_24 : Algebra R' T
inst_25 : Algebra R' A
inst_26 : Algebra R' B
inst_27 : IsScalarTower R R' A
inst_28 : SMulCommClass S R' A
inst_29 : SMulCommClass R' S A
inst_30 : IsScalarTower R' T A
inst_31 : IsScalarTower R R' B
m : A
n : B
p : C
q : D
⊢ Eq (α := A ⊗[S] C ⊗[R'] (B ⊗[R] D))
    (((tensorTensorTensorComm R R' S T A B C D : A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₐ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
          (a : A ⊗[R'] B ⊗[S] (C ⊗[R] D)) → A ⊗[S] C ⊗[R'] (B ⊗[R] D))
        (m ⊗ₜ[R'] n ⊗ₜ[S] (p ⊗ₜ[R] q)) :
      A ⊗[S] C ⊗[R'] (B ⊗[R] D))
    (m ⊗ₜ[S] p ⊗ₜ[R'] (n ⊗ₜ[R] q) : A ⊗[S] C ⊗[R'] (B ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, 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
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra T A
inst_18 : IsScalarTower R T A
inst_19 : SMulCommClass S T A
inst_20 : Algebra S T
inst_21 : IsScalarTower S T A
inst_22 : CommSemiring R'
inst_23 : Algebra R R'
inst_24 : Algebra R' T
inst_25 : Algebra R' A
inst_26 : Algebra R' B
inst_27 : IsScalarTower R R' A
inst_28 : SMulCommClass S R' A
inst_29 : SMulCommClass R' S A
inst_30 : IsScalarTower R' T A
inst_31 : IsScalarTower R R' B
m : A
n : C
p : B
q : D
⊢ Eq (α := A ⊗[R'] B ⊗[S] (C ⊗[R] D))
    (((AlgEquiv.symm (tensorTensorTensorComm R R' S T A B C D) :
            A ⊗[S] C ⊗[R'] (B ⊗[R] D) ≃ₐ[T] A ⊗[R'] B ⊗[S] (C ⊗[R] D)) :
          (a : A ⊗[S] C ⊗[R'] (B ⊗[R] D)) → A ⊗[R'] B ⊗[S] (C ⊗[R] D))
        (m ⊗ₜ[S] n ⊗ₜ[R'] (p ⊗ₜ[R] q)) :
      A ⊗[R'] B ⊗[S] (C ⊗[R] D))
    (m ⊗ₜ[R'] p ⊗ₜ[S] (n ⊗ₜ[R] q) : A ⊗[R'] B ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, 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
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra T A
inst_18 : IsScalarTower R T A
inst_19 : SMulCommClass S T A
inst_20 : Algebra S T
inst_21 : IsScalarTower S T A
inst_22 : CommSemiring R'
inst_23 : Algebra R R'
inst_24 : Algebra R' T
inst_25 : Algebra R' A
inst_26 : Algebra R' B
inst_27 : IsScalarTower R R' A
inst_28 : SMulCommClass S R' A
inst_29 : SMulCommClass R' S A
inst_30 : IsScalarTower R' T A
inst_31 : IsScalarTower R R' B
⊢ Eq (α := A ⊗[S] C ⊗[R'] (B ⊗[R] D) ≃ₐ[T] A ⊗[R'] B ⊗[S] (C ⊗[R] D))
    (AlgEquiv.symm (tensorTensorTensorComm R R' S T A B C D) :
      A ⊗[S] C ⊗[R'] (B ⊗[R] D) ≃ₐ[T] A ⊗[R'] B ⊗[S] (C ⊗[R] D))
    (tensorTensorTensorComm R S R' T A C B D : A ⊗[S] C ⊗[R'] (B ⊗[R] D) ≃ₐ[T] A ⊗[R'] B ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: AlgEquiv.symm, Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.tensorTensorTensorComm, AlgEquiv.ofLinearEquiv, Equiv.symm, 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
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra T A
inst_18 : IsScalarTower R T A
inst_19 : SMulCommClass S T A
inst_20 : Algebra S T
inst_21 : IsScalarTower S T A
inst_22 : CommSemiring R'
inst_23 : Algebra R R'
inst_24 : Algebra R' T
inst_25 : Algebra R' A
inst_26 : Algebra R' B
inst_27 : IsScalarTower R R' A
inst_28 : SMulCommClass S R' A
inst_29 : SMulCommClass R' S A
inst_30 : IsScalarTower R' T A
inst_31 : IsScalarTower R R' B
⊢ Eq (α := A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
    ((↑(tensorTensorTensorComm R R' S T A B C D) : A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
      A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
    (AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D :
      A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm, AlgEquiv.toLinearEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : Semiring D
inst_8 : Algebra R D
⊢ Eq (α := A ⊗[R] B ⊗[R] (C ⊗[R] D) ≃ₗ[R] A ⊗[R] C ⊗[R] (B ⊗[R] D))
    ((↑(tensorTensorTensorComm R R R R A B C D) : A ⊗[R] B ⊗[R] (C ⊗[R] D) ≃ₗ[R] A ⊗[R] C ⊗[R] (B ⊗[R] D)) :
      A ⊗[R] B ⊗[R] (C ⊗[R] D) ≃ₗ[R] A ⊗[R] C ⊗[R] (B ⊗[R] D))
    (_root_.TensorProduct.tensorTensorTensorComm R A B C D : A ⊗[R] B ⊗[R] (C ⊗[R] D) ≃ₗ[R] A ⊗[R] C ⊗[R] (B ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tensorTensorTensorComm, AlgEquiv.toLinearEquiv, TensorProduct.tmul, LinearEquiv.trans, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : Semiring D
inst_8 : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
hf : Function.Bijective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Bijective.{uC + 1, uD + 1} (α := C) (β := D) (⇑g : (a : C) → D)
⊢ Function.Bijective (α := A ⊗[R] C) (β := B ⊗[R] D) (⇑(map f g : A ⊗[R] C →ₐ[R] B ⊗[R] D) : (a : A ⊗[R] C) → B ⊗[R] D)

Tactic:
_root_.TensorProduct.map_bijective hf hg

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.map_bijective, TensorProduct, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
ha :
  ∀ (x : A),
    Eq (α := A ⊗[R] B)
      ((AlgHom.comp (B := A ⊗[R] R)
              (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
              (includeLeft : A →ₐ[S] A ⊗[R] R) :
            (a : A) → A ⊗[R] B)
          x :
        A ⊗[R] B)
      (((AlgHom.comp (B := A ⊗[R] R) (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
                (includeLeft : A →ₐ[S] A ⊗[R] R) :
              A →ₐ[S] A ⊗[R] B) :
            (a : A) → A ⊗[R] B)
          x :
        A ⊗[R] B)
⊢ Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)

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 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
x : A
⊢ Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] R)
            (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
            (includeLeft : A →ₐ[S] A ⊗[R] R) :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    (((AlgHom.comp (B := A ⊗[R] R) (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
              (includeLeft : A →ₐ[S] A ⊗[R] R) :
            A →ₐ[S] A ⊗[R] B) :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)

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 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)

Tactic:
have : (includeLeft : A →ₐ[S] A ⊗[R] B).comp (TensorProduct.rid R S A).toAlgHom =
      map (.id S A) (Algebra.ofId R B) := by ext; simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
rw :
  Function.Bijective (α := A ⊗[R] R) (β := A ⊗[R] B)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))
⊢ Function.Bijective (α := A) (β := A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)

Tactic:
rw [← Function.Bijective.of_comp_iff _ (TensorProduct.rid R S A).bijective]

Premises used: Function.Bijective.of_comp_iff, Algebra.TensorProduct.rid, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
h₁ :
  Eq (α := A ⊗[R] R → A ⊗[R] B)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)
convert_to :
  Function.Bijective (α := A ⊗[R] R) (β := A ⊗[R] B)
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)
⊢ Function.Bijective (α := A ⊗[R] R) (β := A ⊗[R] B)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))

Tactic:
convert_to Function.Bijective (map (.id R A) (Algebra.ofId R B))

Premises used: Algebra.TensorProduct.map, AlgHom.id, Algebra.ofId, Function.Bijective, DFunLike.coe
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
⊢ Eq (α := A ⊗[R] R → A ⊗[R] B)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)

Tactic:
DFunLike.coe_fn_eq.mpr this

Premises used: Iff.mpr, DFunLike.coe_fn_eq, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
⊢ Eq (α := A ⊗[R] R → A ⊗[R] B)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)

Tactic:
exact DFunLike.coe_fn_eq.mpr this

Premises used: Iff.mpr, DFunLike.coe_fn_eq
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
⊢ Function.Bijective (α := A ⊗[R] R) (β := A ⊗[R] B)
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)

Tactic:
Algebra.TensorProduct.map_bijective Function.bijective_id h

Premises used: Function.bijective_id, Algebra.TensorProduct.map_bijective
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
h : Function.Bijective.{uR + 1, uB + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
this :
  Eq (α := A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (AlgHom.comp includeLeft (↑(TensorProduct.rid R S A) : A ⊗[R] R →ₐ[S] A) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
    (map (AlgHom.id S A) (ofId R B) : A ⊗[R] R →ₐ[S] A ⊗[R] B)
⊢ Function.Bijective (α := A ⊗[R] R) (β := A ⊗[R] B)
    (⇑(map (AlgHom.id R A) (ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) : (a : A ⊗[R] R) → A ⊗[R] B)

Tactic:
exact Algebra.TensorProduct.map_bijective Function.bijective_id h

Premises used: Algebra.TensorProduct.map_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
h : Function.Bijective.{uR + 1, uA + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
rw :
  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))
⊢ Function.Bijective (α := B) (β := A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)

Tactic:
rw [← Function.Bijective.of_comp_iff' (TensorProduct.comm R A B).bijective]

Premises used: Algebra.TensorProduct.comm, Function.Bijective.of_comp_iff', AlgEquiv.bijective