awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    (f : (a : A ⊗[R] B ⊗[R] C) → D) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
      HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) : D)
        ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) : D)
h_one : Eq.{uD + 1} (α := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) : D) (1 : D)
x : A
x_1 : B
x_2 : C
x_3 : A
x_4 : B
x_5 : C
⊢ (f : (a : A ⊗[R] B ⊗[R] C) → D) ((x * x_3) ⊗ₜ[R] (x_1 * x_4) ⊗ₜ[R] (x_2 * x_5)) =
    HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x ⊗ₜ[R] x_1 ⊗ₜ[R] x_2) : D)
      ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x_3 ⊗ₜ[R] x_4 ⊗ₜ[R] x_5) : D)

Tactic:
h_mul _ _ _ _ _ _
-- 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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    (f : (a : A ⊗[R] B ⊗[R] C) → D) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
      HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) : D)
        ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) : D)
h_one : Eq.{uD + 1} (α := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) : D) (1 : D)
x : A
x_1 : B
x_2 : C
x_3 : A
x_4 : B
x_5 : C
⊢ (f : (a : A ⊗[R] B ⊗[R] C) → D) ((x * x_3) ⊗ₜ[R] (x_1 * x_4) ⊗ₜ[R] (x_2 * x_5)) =
    HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x ⊗ₜ[R] x_1 ⊗ₜ[R] x_2) : D)
      ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x_3 ⊗ₜ[R] x_4 ⊗ₜ[R] x_5) : D)

Tactic:
exact h_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 : Semiring D
inst_7 : Algebra R D
inst_8 : Algebra R C
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    (f : (a : A ⊗[R] B ⊗[R] C) → D) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
      HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) : D)
        ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) : D)
h_one : Eq.{uD + 1} (α := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) : D) (1 : D)
x : A ⊗[R] B ⊗[R] C
⊢ Eq.{uD + 1} (α := D) ((algEquivOfLinearEquivTripleTensorProduct f h_mul h_one : (a : A ⊗[R] B ⊗[R] C) → D) x : D)
    ((f : (a : A ⊗[R] B ⊗[R] C) → D) x : D)

Tactic:
rfl

Premises used: 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 : 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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
a₁ a₂ : A
b₁ b₂ : B
rw :
  HMul.hMul (β := C) (HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C))
      ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
rw₁ :
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C) *
      HMul.hMul (α := C) (β := C) ((g : (a : B) → C) b₁ : C) ((g : (a : B) → C) b₂ : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
rw₂ rw₃ :
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) (a₁ * a₂) : C) ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)

Tactic:
rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm]

Premises used: Commute.mul_mul_mul_comm, map_mul
-- 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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
rw : HMul.hMul (α := C) (β := C) (1 : C) ((g : (a : B) → C) 1 : C) = 1
rw₁ : HMul.hMul (α := C) 1 1 = 1
rw₂ rw₃ : Eq.{uC + 1} (α := C) 1 1
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) 1 : C) ((g : (a : B) → C) 1 : C) = 1

Tactic:
rw [map_one, map_one, one_mul]

Premises used: map_one, one_mul
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 S C
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
a : A
b : B
⊢ ((lift f g hfg : A ⊗[R] B →ₐ[S] C) : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a : C) ((g : (a : B) → C) b : C)

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 : 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
ha :
  ∀ (x : A),
    Eq (α := A ⊗[R] B)
      ((AlgHom.comp (B := A ⊗[R] B) (lift includeLeft includeRight ⋯ : A ⊗[R] B →ₐ[S] A ⊗[R] B)
              (includeLeft : A →ₐ[S] A ⊗[R] B) :
            (a : A) → A ⊗[R] B)
          x :
        A ⊗[R] B)
      ((AlgHom.comp (AlgHom.id S (A ⊗[R] B)) includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
hb :
  ∀ (x : B),
    Eq (α := A ⊗[R] B)
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.restrictScalars R (S := S) (lift includeLeft includeRight ⋯ : A ⊗[R] B →ₐ[S] A ⊗[R] B))
              includeRight :
            (a : B) → A ⊗[R] B)
          x :
        A ⊗[R] B)
      ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id S (A ⊗[R] B))) includeRight : (a : B) → A ⊗[R] B) x : A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B →ₐ[S] A ⊗[R] B) (lift includeLeft includeRight ⋯ : A ⊗[R] B →ₐ[S] A ⊗[R] B)
    (AlgHom.id S (A ⊗[R] B) : A ⊗[R] B →ₐ[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
x : A
⊢ Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B) (lift includeLeft includeRight ⋯ : A ⊗[R] B →ₐ[S] A ⊗[R] B)
            (includeLeft : A →ₐ[S] A ⊗[R] B) :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    ((AlgHom.comp (AlgHom.id S (A ⊗[R] B)) includeLeft : (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
x : B
⊢ Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S) (lift includeLeft includeRight ⋯ : A ⊗[R] B →ₐ[S] A ⊗[R] B))
            includeRight :
          (a : B) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id S (A ⊗[R] B))) includeRight : (a : B) → 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
C : Type uC
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 S C
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
⊢ ∀ (x : A),
    Eq.{uC + 1} (α := C)
      ((AlgHom.comp (B := A ⊗[R] B) (lift f g hfg : A ⊗[R] B →ₐ[S] C) (includeLeft : A →ₐ[S] A ⊗[R] B) : (a : A) → C)
          x :
        C)
      ((f : (a : A) → C) x : C)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 S C
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
⊢ ∀ (x : B),
    Eq.{uC + 1} (α := C)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (lift f g hfg : A ⊗[R] B →ₐ[S] C)) includeRight :
            (a : B) → C)
          x :
        C)
      ((g : (a : B) → C) x : C)

Tactic:
simp
-- 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
f : A →ₐ[R] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
⊢ ∀ (x : B),
    Eq.{uC + 1} (α := C)
      ((AlgHom.comp (lift f g hfg : A ⊗[R] B →ₐ[R] C) (includeRight : B →ₐ[R] A ⊗[R] B) : (a : B) → C) x : C)
      ((g : (a : B) → C) x : C)

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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
fg :
  { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
    ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }
x : A
⊢ Eq.{uC + 1} (α := C)
    (((↑((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                        (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
                      { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                  ((fun
                        (fg :
                          { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                            ∀ (x : A) (y : B),
                              Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                      (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ :
                        A ⊗[R] B →ₐ[S] C))
                    fg)) :
              (A →ₐ[S] C) × (B →ₐ[R] C)).1 :
          (a : A) → C)
        x :
      C)
    (((↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 : (a : A) → C) x : C)

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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
fg :
  { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
    ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }
x : B
⊢ Eq.{uC + 1} (α := C)
    (((↑((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                        (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
                      { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                  ((fun
                        (fg :
                          { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                            ∀ (x : A) (y : B),
                              Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                      (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ :
                        A ⊗[R] B →ₐ[S] C))
                    fg)) :
              (A →ₐ[S] C) × (B →ₐ[R] C)).2 :
          (a : B) → C)
        x :
      C)
    (((↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 : (a : B) → C) x : C)

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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x : A
⊢ Eq.{uC + 1} (α := C)
    ((AlgHom.comp (B := A ⊗[R] B)
            ((fun
                  (fg :
                    { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                      ∀ (x : A) (y : B),
                        Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ : A ⊗[R] B →ₐ[S] C))
              ((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                  (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                      ∀ (x : A) (y : B),
                        Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                      (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
                    { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                      ∀ (x : A) (y : B),
                        Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                f'))
            includeLeft :
          (a : A) → C)
        x :
      C)
    ((f'.comp includeLeft : (a : A) → C) x : C)

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 S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x : B
⊢ Eq.{uC + 1} (α := C)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S)
              ((fun
                    (fg :
                      { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                  (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ : A ⊗[R] B →ₐ[S] C))
                ((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                        (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
                      { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                  f')))
            includeRight :
          (a : B) → C)
        x :
      C)
    ((AlgHom.comp (AlgHom.restrictScalars R f') includeRight : (a : B) → C) x : C)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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 S C
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
inst_13 : CommSemiring R'
inst_14 : Algebra R R'
inst_15 : Algebra R' S
inst_16 : Algebra R' A
inst_17 : IsScalarTower R R' A
inst_18 : IsScalarTower R' S A
inst_19 : Algebra R' C
inst_20 : IsScalarTower R R' C
inst_21 : IsScalarTower R' S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
⊢ Eq (α := A ⊗[R] B →ₐ[R'] C) (AlgHom.restrictScalars R' (lift f g hfg : A ⊗[R] B →ₐ[S] C) : A ⊗[R] B →ₐ[R'] C)
    (lift (AlgHom.restrictScalars R' f) g hfg : A ⊗[R] B →ₐ[R'] C)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Quotient.liftOn', AddCon.liftOn, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, TensorProduct, 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 : 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
simp : ∀ (a₁ a₂ : R) (b₁ b₂ : A), a₁ • a₂ • (b₁ * b₂) = a₂ • a₁ • (b₁ * b₂)
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A),
    (_root_.TensorProduct.lid R A : (a : R ⊗[R] A) → A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := A) (β := A) ((_root_.TensorProduct.lid R A : (a : R ⊗[R] A) → A) (a₁ ⊗ₜ[R] b₁) : A)
        ((_root_.TensorProduct.lid R A : (a : R ⊗[R] A) → A) (a₂ ⊗ₜ[R] b₂) : A)

Tactic:
simp only [mul_smul, lid_tmul, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]

Premises used: Algebra.mul_smul_comm, TensorProduct.lid_tmul, Algebra.smul_mul_assoc, SemigroupAction.mul_smul
-- 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
simp_rw : ∀ (a₁ a₂ : R) (b₁ b₂ : A), True
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A), a₁ • a₂ • (b₁ * b₂) = a₂ • a₁ • (b₁ * b₂)

Tactic:
simp_rw [← mul_smul, mul_comm]

Premises used: mul_comm, SemigroupAction.mul_smul
-- 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
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A), True

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
⊢ Eq.{uA + 1} (α := A) ((_root_.TensorProduct.lid R A : (a : R ⊗[R] A) → A) (1 ⊗ₜ[R] 1) : A) (1 : A)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := R ⊗[R] A ≃ₗ[R] A) (↑(TensorProduct.lid R A) : R ⊗[R] A ≃ₗ[R] A) (_root_.TensorProduct.lid R A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, AlgEquiv.toLinearEquiv, TensorProduct.lid, TensorProduct, TensorProduct.lift, rfl