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
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
a : A
b : B
⊢ Eq (α := C ⊗[R] D) (((map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D) (a ⊗ₜ[R] b) : C ⊗[R] D)
    ((f : (a : A) → C) a ⊗ₜ[R] (g : (a : B) → D) b : 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
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
⊢ Eq (α := A ⊗[R] B →ₐ[S] A ⊗[R] B) (map (AlgHom.id S A) (AlgHom.id R B) : A ⊗[R] B →ₐ[S] A ⊗[R] B)
    (AlgHom.id S (A ⊗[R] B) : A ⊗[R] B →ₐ[S] A ⊗[R] B)

Tactic:
ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Premises used: AlgHom.ext, Algebra.TensorProduct.ext, rfl
-- 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₂ : C →ₐ[S] E
f₁ : A →ₐ[S] C
g₂ : D →ₐ[R] F
g₁ : B →ₐ[R] D
⊢ Eq (α := A ⊗[R] B →ₐ[S] E ⊗[R] F) (map (f₂.comp f₁) (g₂.comp g₁) : A ⊗[R] B →ₐ[S] E ⊗[R] F)
    (AlgHom.comp (B := C ⊗[R] D) (map f₂ g₂ : C ⊗[R] D →ₐ[S] E ⊗[R] F) (map f₁ g₁ : A ⊗[R] B →ₐ[S] C ⊗[R] D) :
      A ⊗[R] B →ₐ[S] E ⊗[R] F)

Tactic:
ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Premises used: AlgHom.ext, Algebra.TensorProduct.ext, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
D : Type uD
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 D
inst_10 : Algebra R D
inst_11 : Semiring F
inst_12 : Algebra R F
g₂ : D →ₐ[R] F
g₁ : B →ₐ[R] D
⊢ Eq (α := A ⊗[R] B →ₐ[S] A ⊗[R] F) (map (AlgHom.id S A) (g₂.comp g₁) : A ⊗[R] B →ₐ[S] A ⊗[R] F)
    (AlgHom.comp (B := A ⊗[R] D) (map (AlgHom.id S A) g₂ : A ⊗[R] D →ₐ[S] A ⊗[R] F)
        (map (AlgHom.id S A) g₁ : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] A ⊗[R] F)

Tactic:
ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Premises used: AlgHom.ext, Algebra.TensorProduct.ext, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
C : Type uC
E : Type uE
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 C
inst_8 : Algebra R C
inst_9 : Algebra S C
inst_10 : IsScalarTower R S C
inst_11 : Semiring E
inst_12 : Algebra R E
inst_13 : Algebra S E
inst_14 : IsScalarTower R S E
f₂ : C →ₐ[S] E
f₁ : A →ₐ[S] C
⊢ Eq (α := A ⊗[R] E →ₐ[S] E ⊗[R] E) (map (f₂.comp f₁) (AlgHom.id R E) : A ⊗[R] E →ₐ[S] E ⊗[R] E)
    (AlgHom.comp (B := C ⊗[R] E) (map f₂ (AlgHom.id R E) : C ⊗[R] E →ₐ[S] E ⊗[R] E)
        (map f₁ (AlgHom.id R E) : A ⊗[R] E →ₐ[S] C ⊗[R] E) :
      A ⊗[R] E →ₐ[S] E ⊗[R] E)

Tactic:
ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Premises used: AlgHom.ext, Algebra.TensorProduct.ext, rfl
-- 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
⊢ ∀ (x : A),
    Eq (α := C ⊗[R] D)
      (((AlgHom.comp (B := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D) (includeLeft : A →ₐ[S] A ⊗[R] B) :
              A →ₐ[S] C ⊗[R] D) :
            (a : A) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      ((AlgHom.comp includeLeft f : (a : A) → C ⊗[R] D) x : C ⊗[R] D)

Tactic:
simp
-- 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
⊢ ∀ (x : B),
    Eq (α := C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)) includeRight :
            (a : B) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      ((AlgHom.comp includeRight g : (a : B) → C ⊗[R] D) x : C ⊗[R] D)

Tactic:
simp
-- 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] C
g : B →ₐ[R] D
⊢ Eq (α := B →ₐ[R] C ⊗[R] D)
    (AlgHom.comp (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeRight : B →ₐ[R] A ⊗[R] B) : B →ₐ[R] C ⊗[R] D)
    (AlgHom.comp includeRight g : B →ₐ[R] C ⊗[R] D)

Tactic:
map_restrictScalars_comp_includeRight f g

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Quotient.liftOn', Algebra.TensorProduct.map, AddCon.liftOn, AlgHom.ofLinearMap, MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, TensorProduct, Algebra.TensorProduct.map_restrictScalars_comp_includeRight
-- 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] C
g : B →ₐ[R] D
a :
  AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) ≤
    AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)
a₁ :
  AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g) ≤
    AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D)
⊢ AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) =
    AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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] C
g : B →ₐ[R] D
a :
  Set.image (α := A ⊗[R] B) (⇑(map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D)
      {t : A ⊗[R] B | ∃ (a : A) (b : B), a ⊗ₜ[R] b = t} ⊆
    (↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) : Set (C ⊗[R] D))
⊢ AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) ≤
    AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)

Tactic:
rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]

Premises used: Algebra.adjoin_image, Algebra.adjoin_le_iff, Algebra.map_top, Algebra.TensorProduct.adjoin_tmul_eq_top
-- 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] C
g : B →ₐ[R] D
a : A
b : B
a₁ :
  HMul.hMul (α := C ⊗[R] D) (β := C ⊗[R] D) ((f : (a : A) → C) a ⊗ₜ[R] 1 : C ⊗[R] D)
      (1 ⊗ₜ[R] (g : (a : B) → D) b : C ⊗[R] D) ∈
    (↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) : Set (C ⊗[R] D))
⊢ Membership.mem (α := C ⊗[R] D)
    (↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) : Set (C ⊗[R] D))
    (((map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D) (a ⊗ₜ[R] b) : C ⊗[R] D)

Tactic:
rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]

Premises used: Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, DFunLike.coe, one_mul
-- 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] C
g : B →ₐ[R] D
a : A
b : B
⊢ HMul.hMul (α := C ⊗[R] D) (β := C ⊗[R] D) ((f : (a : A) → C) a ⊗ₜ[R] 1 : C ⊗[R] D)
      (1 ⊗ₜ[R] (g : (a : B) → D) b : C ⊗[R] D) ∈
    (↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) : Set (C ⊗[R] D))

Tactic:
mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)

Premises used: AlgHom.mem_range_self, Set.Mem, Algebra.mul_mem_sup
-- 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] C
g : B →ₐ[R] D
a : A
b : B
⊢ HMul.hMul (α := C ⊗[R] D) (β := C ⊗[R] D) ((f : (a : A) → C) a ⊗ₜ[R] 1 : C ⊗[R] D)
      (1 ⊗ₜ[R] (g : (a : B) → D) b : C ⊗[R] D) ∈
    (↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)) : Set (C ⊗[R] D))

Tactic:
exact mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)

Premises used: AlgHom.mem_range_self, Algebra.mul_mem_sup
-- 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] C
g : B →ₐ[R] D
a :
  LE.le (α := Subalgebra R (C ⊗[R] D))
    (AlgHom.range (AlgHom.comp (B := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeLeft : A →ₐ[R] A ⊗[R] B)) ⊔
        AlgHom.range (AlgHom.comp (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeRight : B →ₐ[R] A ⊗[R] B)) :
      Subalgebra R (C ⊗[R] D))
    (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : Subalgebra R (C ⊗[R] D))
⊢ AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g) ≤
    AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D)

Tactic:
rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]

Premises used: Algebra.TensorProduct.map_comp_includeRight, Algebra.TensorProduct.map_comp_includeLeft
-- 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] C
g : B →ₐ[R] D
⊢ LE.le (α := Subalgebra R (C ⊗[R] D))
    (AlgHom.range (AlgHom.comp (B := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeLeft : A →ₐ[R] A ⊗[R] B)) ⊔
        AlgHom.range (AlgHom.comp (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeRight : B →ₐ[R] A ⊗[R] B)) :
      Subalgebra R (C ⊗[R] D))
    (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : Subalgebra R (C ⊗[R] D))

Tactic:
sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)

Premises used: Set.Mem, AlgHom.range_comp_le_range, sup_le
-- 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] C
g : B →ₐ[R] D
⊢ LE.le (α := Subalgebra R (C ⊗[R] D))
    (AlgHom.range (AlgHom.comp (B := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeLeft : A →ₐ[R] A ⊗[R] B)) ⊔
        AlgHom.range (AlgHom.comp (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) (includeRight : B →ₐ[R] A ⊗[R] B)) :
      Subalgebra R (C ⊗[R] D))
    (AlgHom.range (A := A ⊗[R] B) (map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : Subalgebra R (C ⊗[R] D))

Tactic:
exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)

Premises used: AlgHom.range_comp_le_range, sup_le
-- 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] C
g : B →ₐ[R] D
ha :
  ∀ (x : A),
    Eq (α := D ⊗[R] C)
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (↑(TensorProduct.comm R C D) : C ⊗[R] D →ₐ[R] D ⊗[R] C) (map f g) : A ⊗[R] B →ₐ[R] D ⊗[R] C)
              (includeLeft : A →ₐ[R] A ⊗[R] B) :
            (a : A) → D ⊗[R] C)
          x :
        D ⊗[R] C)
      (((AlgHom.comp
                (AlgHom.comp (map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C)
                  ((↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
                includeLeft :
              A →ₐ[R] D ⊗[R] C) :
            (a : A) → D ⊗[R] C)
          x :
        D ⊗[R] C)
hb :
  ∀ (x : B),
    Eq (α := D ⊗[R] C)
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.restrictScalars R
                (AlgHom.comp (↑(TensorProduct.comm R C D) : C ⊗[R] D →ₐ[R] D ⊗[R] C) (map f g) :
                  A ⊗[R] B →ₐ[R] D ⊗[R] C))
              includeRight :
            (a : B) → D ⊗[R] C)
          x :
        D ⊗[R] C)
      ((AlgHom.comp
              (AlgHom.restrictScalars R
                (AlgHom.comp (map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C)
                    ((↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                  A ⊗[R] B →ₐ[R] D ⊗[R] C))
              includeRight :
            (a : B) → D ⊗[R] C)
          x :
        D ⊗[R] C)
⊢ Eq (α := A ⊗[R] B →ₐ[R] D ⊗[R] C)
    (AlgHom.comp (↑(TensorProduct.comm R C D) : C ⊗[R] D →ₐ[R] D ⊗[R] C) (map f g) : A ⊗[R] B →ₐ[R] D ⊗[R] C)
    (AlgHom.comp (map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C)
        ((↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
      A ⊗[R] B →ₐ[R] D ⊗[R] C)

Tactic:
ext
-- 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] C
g : B →ₐ[R] D
x : A
⊢ Eq (α := D ⊗[R] C)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.comp (↑(TensorProduct.comm R C D) : C ⊗[R] D →ₐ[R] D ⊗[R] C) (map f g) : A ⊗[R] B →ₐ[R] D ⊗[R] C)
            (includeLeft : A →ₐ[R] A ⊗[R] B) :
          (a : A) → D ⊗[R] C)
        x :
      D ⊗[R] C)
    (((AlgHom.comp
              (AlgHom.comp (map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C)
                ((↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
              includeLeft :
            A →ₐ[R] D ⊗[R] C) :
          (a : A) → D ⊗[R] C)
        x :
      D ⊗[R] C)

Tactic:
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] C
g : B →ₐ[R] D
x : B
⊢ Eq (α := D ⊗[R] C)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (↑(TensorProduct.comm R C D) : C ⊗[R] D →ₐ[R] D ⊗[R] C) (map f g) : A ⊗[R] B →ₐ[R] D ⊗[R] C))
            includeRight :
          (a : B) → D ⊗[R] C)
        x :
      D ⊗[R] C)
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (AlgHom.comp (map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C)
                  ((↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                A ⊗[R] B →ₐ[R] D ⊗[R] C))
            includeRight :
          (a : B) → D ⊗[R] C)
        x :
      D ⊗[R] C)

Tactic:
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] C
g : B →ₐ[R] D
x : A ⊗[R] B
⊢ Eq (α := D ⊗[R] C)
    ((TensorProduct.comm R C D : (a : C ⊗[R] D) → D ⊗[R] C)
        (((map f g : A ⊗[R] B →ₐ[R] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D) x) :
      D ⊗[R] C)
    (((map g f : B ⊗[R] A →ₐ[R] D ⊗[R] C) : (a : B ⊗[R] A) → D ⊗[R] C)
        ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x) :
      D ⊗[R] C)

Tactic:
congr($(comm_comp_map f g) x)

Premises used: congrArg, id, Algebra.TensorProduct.comm_comp_map, DFunLike.coe
-- 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 : 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
g : B ≃ₐ[R] D
b : C
d : D
⊢ Eq (α := C ⊗[R] D)
    (((AlgHom.comp (B := A ⊗[R] B) (map (↑f : A →ₐ[S] C) (↑g : B →ₐ[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D)
              (map (↑f.symm : C →ₐ[S] A) (↑g.symm : D →ₐ[R] B) : C ⊗[R] D →ₐ[S] A ⊗[R] B) :
            C ⊗[R] D →ₐ[S] C ⊗[R] D) :
          (a : C ⊗[R] D) → C ⊗[R] D)
        (b ⊗ₜ[R] d) :
      C ⊗[R] D)
    ((AlgHom.id S (C ⊗[R] D) : (a : C ⊗[R] D) → C ⊗[R] D) (b ⊗ₜ[R] d) : C ⊗[R] D)

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 : 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
g : B ≃ₐ[R] D
a : A
c : B
⊢ Eq (α := A ⊗[R] B)
    (((AlgHom.comp (B := C ⊗[R] D) (map (↑f.symm : C →ₐ[S] A) (↑g.symm : D →ₐ[R] B) : C ⊗[R] D →ₐ[S] A ⊗[R] B)
              (map (↑f : A →ₐ[S] C) (↑g : B →ₐ[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D) :
            A ⊗[R] B →ₐ[S] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        (a ⊗ₜ[R] c) :
      A ⊗[R] B)
    ((AlgHom.id S (A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B) (a ⊗ₜ[R] c) : A ⊗[R] B)

Tactic:
simp
-- 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 (α := A ⊗[R] B ≃ₗ[S] C ⊗[R] D) ((↑(congr f g) : A ⊗[R] B ≃ₗ[S] C ⊗[R] D) : A ⊗[R] B ≃ₗ[S] C ⊗[R] D)
    (AlgebraTensorModule.congr (↑f : A ≃ₗ[S] C) (↑g : B ≃ₗ[R] D) : A ⊗[R] B ≃ₗ[S] C ⊗[R] D)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.AlgebraTensorModule.congr, AlgEquiv.toLinearEquiv, TensorProduct, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- 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
x : A ⊗[R] B
⊢ Eq (α := C ⊗[R] D) (((congr f g : A ⊗[R] B ≃ₐ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D) x : C ⊗[R] D)
    (((map (↑f : A →ₐ[S] C) (↑g : B →ₐ[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D) x : C ⊗[R] D)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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
x : C ⊗[R] D
⊢ Eq (α := A ⊗[R] B) (((AlgEquiv.symm (congr f g) : C ⊗[R] D ≃ₐ[S] A ⊗[R] B) : (a : C ⊗[R] D) → A ⊗[R] B) x : A ⊗[R] B)
    (((map (↑f.symm : C →ₐ[S] A) (↑g.symm : D →ₐ[R] B) : C ⊗[R] D →ₐ[S] A ⊗[R] B) : (a : C ⊗[R] D) → A ⊗[R] B) x :
      A ⊗[R] B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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
⊢ Eq (α := A ⊗[R] B ≃ₐ[S] A ⊗[R] B) (congr AlgEquiv.refl AlgEquiv.refl : A ⊗[R] B ≃ₐ[S] A ⊗[R] B)
    (AlgEquiv.refl : A ⊗[R] B ≃ₐ[S] A ⊗[R] B)

Tactic:
AlgEquiv.coe_algHom_injective <| map_id

Premises used: Algebra.TensorProduct.map_id, AlgEquiv.coe_algHom_injective