awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x y z : A ⊗[R] B
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
              ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A ⊗[R] B) → A ⊗[R] B)
                y) :
            A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        z :
      A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
        ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          z) :
      A ⊗[R] B)
have suffices : Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
  ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
            (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
        mul ∘ₗ
      mul :
    A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
  (LinearMap.flip
      ((((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                (a : (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                  (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                    A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
              (↑LinearMap.lflip :
                (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
            A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
        ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
            (LinearMap.flip mul) ∘ₗ
          mul)) :
    A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
Tactic: suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
a : A
b : B
k : ℕ
⊢ HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)
have zero : HPow.hPow (α := A ⊗[R] B) (β := ℕ) (a ⊗ₜ[R] b) 0 = HPow.hPow (β := ℕ) a 0 ⊗ₜ[R] HPow.hPow (β := ℕ) b 0
Tactic: induction k with
  | zero => simp [one_def]
  | succ k ih => simp [pow_succ, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
a : A
b : B
k : ℕ
zero : HPow.hPow (α := A ⊗[R] B) (β := ℕ) (a ⊗ₜ[R] b) 0 = HPow.hPow (β := ℕ) a 0 ⊗ₜ[R] HPow.hPow (β := ℕ) b 0
⊢ HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)
have succ : ∀ (k : ℕ) (ih : HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) k = (a ^ k) ⊗ₜ[R] (b ^ k)),
  HPow.hPow (α := A ⊗[R] B) (a ⊗ₜ[R] b) (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))
Tactic: induction k with
  | zero => simp [one_def]
  | succ k ih => simp [pow_succ, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₃ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = r • (x * 1)
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
rw₃ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = r • (x * 1)
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₄ : r • (1 * x) = r • (x * 1)
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
rw₃ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = r • (x * 1)
rw₄ : r • (1 * x) = r • (x * 1)
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₅ : r • (1 * x) = r • x
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x = x * HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1
rw₁ : HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x = x * HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1)
rw₂ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = x * HSMul.hSMul (β := A ⊗[R] B) r 1
rw₃ : HSMul.hSMul (β := A ⊗[R] B) r 1 * x = r • (x * 1)
rw₄ : r • (1 * x) = r • (x * 1)
rw₅ : r • (1 * x) = r • x
⊢ HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
have rw₆ : r • x = r • x
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
        one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x
have rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x
have rw₁ : r • x = HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
rw₁ : r • x = HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x
have rw₂ : r • x = r • (1 ⊗ₜ[R] 1 * x)
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
rw₁ : r • x = HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x
rw₂ : r • x = r • (1 ⊗ₜ[R] 1 * x)
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x
have rw₃ : r • x = r • (1 * x)
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : SMulCommClass R S A
r : S
x : A ⊗[R] B
rw : r • x = HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1 * x
rw₁ : r • x = HSMul.hSMul (β := A ⊗[R] B) r (1 ⊗ₜ[R] 1) * x
rw₂ : r • x = r • (1 ⊗ₜ[R] 1 * x)
rw₃ : r • x = r • (1 * x)
⊢ r • x = HMul.hMul (α := A ⊗[R] B) ((algebraMap S A : (a : S) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) x
have rw₄ : r • x = r • x
Tactic: rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
have rw : 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 [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
have 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)
Tactic: rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) ((algebraMap R A : (a : R) → A) r ⊗ₜ[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 : A ⊗[R] B) (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
have rw₂ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
Tactic: rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) ((algebraMap R A : (a : R) → A) r ⊗ₜ[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 : 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)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    (1 ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : A ⊗[R] B)
have rw₃ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1) (1 ⊗ₜ[R] HSMul.hSMul (β := B) r 1)
Tactic: rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ Eq (α := R →+* A ⊗[R] B) (RingHom.comp includeLeftRingHom (algebraMap R A))
    (RingHom.comp (AlgHom.toRingHom includeRight) (algebraMap R B))
have a : ∀ (x : R),
  Eq (α := A ⊗[R] B) ((RingHom.comp includeLeftRingHom (algebraMap R A) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)
    ((RingHom.comp (AlgHom.toRingHom includeRight) (algebraMap R B) : (a : R) → A ⊗[R] B) x : A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
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
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
⊢ f = g
have a : f.toLinearMap = g.toLinearMap
Tactic: apply AlgHom.toLinearMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
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
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
⊢ f.toLinearMap = g.toLinearMap
have a : ∀ (a : A) (b : B),
  Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry f.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
    (((((AlgebraTensorModule.curry g.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (hypothesis)
Goal:
R : Type uR
S : Type uS
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
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
⊢ Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry f.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
    (((((AlgebraTensorModule.curry g.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
have this : HMul.hMul (α := C) (β := C) ((f.comp includeLeft : (a : A) → C) a : C)
    ((AlgHom.comp (AlgHom.restrictScalars R f) includeRight : (a : B) → C) b : C) =
  HMul.hMul (α := C) (β := C) ((g.comp includeLeft : (a : A) → C) a : C)
    ((AlgHom.comp (AlgHom.restrictScalars R g) includeRight : (a : B) → C) b : C)
Tactic: have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
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
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R f) includeRight : (a : B) → C) b : C) =
    HMul.hMul (α := C) (β := C) ((g.comp includeLeft : (a : A) → C) a : C)
      ((AlgHom.comp (AlgHom.restrictScalars R g) includeRight : (a : B) → C) b : C)
⊢ Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry f.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
    (((((AlgebraTensorModule.curry g.toLinearMap : A →ₗ[S] B →ₗ[R] C) : (a : A) → B →ₗ[R] C) a : B →ₗ[R] C) :
          (a : B) → C)
        b :
      C)
have a₁ : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: dsimp at *