awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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
⊢ 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)
have 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))
Tactic: rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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
⊢ 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)
have 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))
Tactic: rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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
⊢ 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)
have 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))
Tactic: rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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 (α := 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (hypothesis)
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)
⊢ Function.Bijective (α := A) (β := A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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) (β := A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
have 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))
Tactic: rw [← Function.Bijective.of_comp_iff _ (TensorProduct.rid R S A).bijective]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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)
    (Function.comp (β := A) (⇑includeLeft : (a : A) → A ⊗[R] B)
      (⇑(TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A))
have 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)
Tactic: convert_to Function.Bijective (map (.id R A) (Algebra.ofId R B))
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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)
⊢ 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))
have 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)
Tactic: convert_to Function.Bijective (map (.id R A) (Algebra.ofId R B))
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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
h : Function.Bijective.{uR + 1, uA + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Bijective (α := B) (β := A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
have 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))
Tactic: rw [← Function.Bijective.of_comp_iff' (TensorProduct.comm R A B).bijective]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : (a : R) → A) r ⊗ₜ[R] 1 : 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 [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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) (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 : (a : R) → A) r ⊗ₜ[R] 1 : 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 [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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) (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 : (a : R) → A) r ⊗ₜ[R] 1 : 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 [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := S ⊗[R] S →ₐ[S] S) (lmul'' R)
    (AlgHom.comp (↑(TensorProduct.lid S S) : S ⊗[S] S →ₐ[S] S) (mapOfCompatibleSMul S R S S S))
have h : ∀ (x : S),
  Eq (α := S) ((AlgHom.comp (AlgHom.restrictScalars R (lmul'' R)) includeRight : (a : S) → S) x : S)
    ((AlgHom.comp (B := S ⊗[R] S)
            (AlgHom.restrictScalars R
              (AlgHom.comp (↑(TensorProduct.lid S S) : S ⊗[S] S →ₐ[S] S) (mapOfCompatibleSMul S R S S S)))
            includeRight :
          (a : S) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ Eq (α := A ⊗[R] B →ₐ[R] S) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S)
have ha : ∀ (x : A),
  Eq.{uS + 1} (α := S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
            (includeLeft : A →ₐ[R] A ⊗[R] B) :
          (a : A) → S)
        x :
      S)
    ((AlgHom.comp (B := A ⊗[R] B) (lift f g sorry : A ⊗[R] B →ₐ[R] S) (includeLeft : A →ₐ[R] A ⊗[R] B) : (a : A) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
ha :
  ∀ (x : A),
    Eq.{uS + 1} (α := S)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S)
              (includeLeft : A →ₐ[R] A ⊗[R] B) :
            (a : A) → S)
          x :
        S)
      ((AlgHom.comp (B := A ⊗[R] B) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S) (includeLeft : A →ₐ[R] A ⊗[R] B) : (a : A) → S) x :
        S)
⊢ Eq (α := A ⊗[R] B →ₐ[R] S) (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S) (lift f g ⋯ : A ⊗[R] B →ₐ[R] S)
have hb : ∀ (x : B),
  Eq.{uS + 1} (α := S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (AlgHom.comp (lmul' R) (map f g) : A ⊗[R] B →ₐ[R] S))
            includeRight :
          (a : B) → S)
        x :
      S)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (lift f g sorry : A ⊗[R] B →ₐ[R] S)) includeRight : (a : B) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
have rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
Tactic: rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
have rw₁ : Eq (α := S ⊗[R] S) ((y • x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
Tactic: rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] S) ((y • x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
have rw₂ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] HSMul.hSMul (β := S) y 1) (x ⊗ₜ[R] y)
Tactic: rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] S) ((y • x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₂ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] HSMul.hSMul (β := S) y 1) (x ⊗ₜ[R] y)
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
have rw₃ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] (y * 1)) (x ⊗ₜ[R] y)
Tactic: rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (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 : Semiring B
inst_3 : CommSemiring S
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst_7 : CompatibleSMul R S S S
x_1 : S ⊗[R] S
x y : S
rw : Eq (α := S ⊗[R] S) ((y * x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] S) ((y • x) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
rw₂ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] HSMul.hSMul (β := S) y 1) (x ⊗ₜ[R] y)
rw₃ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] (y * 1)) (x ⊗ₜ[R] y)
⊢ Eq (α := S ⊗[R] S) ((x * y) ⊗ₜ[R] 1) (x ⊗ₜ[R] y)
have rw₄ : Eq (α := S ⊗[R] S) (x ⊗ₜ[R] y) (x ⊗ₜ[R] y)
Tactic: rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CompatibleSMul R S S S
⊢ Eq (α := S ⊗[R] S →ₐ[S] S) (↑(lmulEquiv R S) : S ⊗[R] S →ₐ[S] S) (↑(lidOfCompatibleSMul R S S) : S ⊗[R] S →ₐ[S] S)
have h : ∀ (x : S),
  Eq (α := S)
    ((AlgHom.comp (AlgHom.restrictScalars R (↑(lmulEquiv R S) : S ⊗[R] S →ₐ[S] S)) includeRight : (a : S) → S) x : S)
    ((AlgHom.comp (B := S ⊗[R] S) (AlgHom.restrictScalars R (↑(lidOfCompatibleSMul R S S) : S ⊗[R] S →ₐ[S] S))
            includeRight :
          (a : S) → S)
        x :
      S)
Tactic: ext