awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) 1 : C) ((g : (a : B) → C) 1 : C) = 1
have rw₂ : Eq.{uC + 1} (α := C) 1 1
Tactic: rw [map_one, map_one, one_mul]
-- 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
⊢ 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)
have ha : ∀ (x : A),
  Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B) (lift includeLeft includeRight sorry : 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: 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
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)
⊢ 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)
have hb : ∀ (x : B),
  Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S) (lift includeLeft includeRight sorry : 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: 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 : 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) }
⊢ (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) =
    fg
have a : ∀ (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) sorry :
                      { 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 sorry :
                        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: 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 : 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
⊢ (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') =
    f'
have ha : ∀ (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 sorry : 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) sorry :
                    { 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: 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 : 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),
    (_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)
have simp : ∀ (a₁ a₂ : R) (b₁ b₂ : A), a₁ • a₂ • (b₁ * b₂) = a₂ • a₁ • (b₁ * b₂)
Tactic: simp only [mul_smul, lid_tmul, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
-- 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 : 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), a₁ • a₂ • (b₁ * b₂) = a₂ • a₁ • (b₁ * b₂)
have simp_rw : ∀ (a₁ a₂ : R) (b₁ b₂ : A), True
Tactic: simp_rw [← mul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] B)
    ((↑R :
            {S M : Type uS} →
              {M₂ : Type (max uB uS)} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ
        AlgEquiv.toLinearMap (TensorProduct.rid R R S) :
      S ⊗[R] R →ₗ[R] S ⊗[R] B)
    (LinearMap.lTensor S (Algebra.linearMap R B) : S ⊗[R] R →ₗ[R] S ⊗[R] B)
have a : ∀ (x : S),
  Eq (α := S ⊗[R] B)
    (((((AlgebraTensorModule.curry
                  ((↑R :
                        {S M : Type uS} →
                          {M₂ : Type (max uB uS)} →
                            [inst : Semiring R] →
                              [inst_5 : Semiring S] →
                                [inst_6 : AddCommMonoid M] →
                                  [inst_7 : AddCommMonoid M₂] →
                                    [inst_8 : Module R M] →
                                      [inst_9 : Module R M₂] →
                                        [inst_10 : Module S M] →
                                          [inst_11 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ
                    AlgEquiv.toLinearMap (TensorProduct.rid R R S)) :
                S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
              (a : S) → R →ₗ[R] S ⊗[R] B)
            x :
          R →ₗ[R] S ⊗[R] B) :
        (a : R) → S ⊗[R] B)
      1)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B)) : S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
              (a : S) → R →ₗ[R] S ⊗[R] B)
            x :
          R →ₗ[R] S ⊗[R] B) :
        (a : R) → S ⊗[R] B)
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
x : A
y : C
⊢ Eq (α := A ⊗[R] B ⊗[A] (A ⊗[R] C)) (x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) (1 ⊗ₜ[A] (x ⊗ₜ[R] y))
have trans : x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y))
Tactic: trans x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
x : A
y : C
trans : x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] B ⊗[A] (A ⊗[R] C)) (x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) (1 ⊗ₜ[A] (x ⊗ₜ[R] y))
have trans₁ : HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)
Tactic: trans x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (hypothesis)
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((q • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q • n))
have this : IsAddTorsionFree (M ⊗[R] N)
Tactic: have : IsAddTorsionFree (M ⊗[R] N) := .of_module_rat _
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) ((q • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q • n))
have suffices : HSMul.hSMul (β := M ⊗[R] N) q.den ((q • m) ⊗ₜ[R] n) = HSMul.hSMul (β := M ⊗[R] N) q.den (m ⊗ₜ[R] (q • n))
Tactic: suffices q.den • ((q • m) ⊗ₜ[R] n) = q.den • (m ⊗ₜ[R] (q • n)) from
      smul_right_injective (M ⊗[R] N) q.den_nz <| by norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ HSMul.hSMul (β := M ⊗[R] N) q.den ((q • m) ⊗ₜ[R] n) = HSMul.hSMul (β := M ⊗[R] N) q.den (m ⊗ₜ[R] (q • n))
have rw : Eq (α := M ⊗[R] N) (HSMul.hSMul (α := ℚ) (↑q.num : ℚ) m ⊗ₜ[R] n) (m ⊗ₜ[R] HSMul.hSMul (α := ℚ) (↑q.num : ℚ) n)
Tactic: rw [smul_tmul', ← tmul_smul, ← smul_assoc, ← smul_assoc, nsmul_eq_mul, Rat.den_mul_eq_num]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) (HSMul.hSMul (α := ℚ) (↑q.num : ℚ) m ⊗ₜ[R] n) (m ⊗ₜ[R] HSMul.hSMul (α := ℚ) (↑q.num : ℚ) n)
have norm_cast : Eq (α := M ⊗[R] N) ((q.num • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q.num • n))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) ((q.num • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q.num • n))
have rw : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (q.num • n)) (m ⊗ₜ[R] (q.num • n))
Tactic: rw [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
⊢ Eq (α := B ⊗[R] A ≃ₐ[R] A ⊗[R] B) (AlgEquiv.symm (TensorProduct.comm R A B)) (TensorProduct.comm R B A)
have h : ∀ (a : B ⊗[R] A),
  Eq (α := A ⊗[R] B) ((AlgEquiv.symm (TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)
    ((TensorProduct.comm R B A : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)
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
⊢ 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 (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