awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
s : S
⊢ ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (HSMul.hSMul (β := S ⊗[R] M) s 0) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
          (a : S ⊗[R] M) → B ⊗[A] M)
        0)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
s : S
x y : S ⊗[R] M
hx :
  ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (s • x) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          x :
        B ⊗[A] M)
hy :
  ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (s • y) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          y :
        B ⊗[A] M)
⊢ ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (s • (x + y)) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          (x + y) :
        B ⊗[A] M)

Tactic:
simp only [smul_add, map_add, hx, hy]

Premises used: map_add, smul_add
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
s s' : S
m : M
⊢ ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (HSMul.hSMul (β := S ⊗[R] M) s (s' ⊗ₜ[R] m)) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          (s' ⊗ₜ[R] m) :
        B ⊗[A] M)

Tactic:
simp [Algebra.smul_def, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', Algebra.smul_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_8
B : Type u_9
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : IsPushout R S A B
M : Type u_10
inst_12 : AddCommGroup M
inst_13 : Module R M
inst_14 : Module A M
inst_15 : IsScalarTower R A M
m : M
⊢ Eq (α := S ⊗[R] M)
    (((LinearEquiv.symm (LinearEquiv.symm (cancelBaseChangeAux R S A B M)) : B ⊗[A] M ≃ₗ[R] S ⊗[R] M) :
          (a : B ⊗[A] M) → S ⊗[R] M)
        (1 ⊗ₜ[A] m) :
      S ⊗[R] M)
    (1 ⊗ₜ[R] m : S ⊗[R] M)

Tactic:
simp [cancelBaseChangeAux, TensorProduct.one_def]

Premises used: Algebra.IsPushout.cancelBaseChangeAux, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_8
B : Type u_9
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : IsPushout R S A B
M : Type u_10
inst_12 : AddCommGroup M
inst_13 : Module R M
inst_14 : Module A M
inst_15 : IsScalarTower R A M
s : S
m : M
⊢ Eq (α := B ⊗[A] M)
    ((LinearEquiv.symm (cancelBaseChange R S A B M) : (a : S ⊗[R] M) → B ⊗[A] M) (s ⊗ₜ[R] m) : B ⊗[A] M)
    ((algebraMap S B : (a : S) → B) s ⊗ₜ[A] m : B ⊗[A] M)

Tactic:
IsPushout.cancelBaseChangeAux_symm_tmul R S A B M s m

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Algebra.IsPushout.cancelBaseChangeAux_symm_tmul, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
C : Type u_11
inst_47 : CommRing C
inst_48 : Algebra R C
inst_49 : Algebra A C
inst_50 : IsScalarTower R A C
refine_1 :
  Eq (α := B ⊗[A] C)
    (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) 1) 1
refine_2 :
  ∀ (x y : S ⊗[R] C),
    ((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) (x * y) =
      HMul.hMul (α := B ⊗[A] C) (β := B ⊗[A] C)
        (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) x :
          B ⊗[A] C)
        (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) y :
          B ⊗[A] C)
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C

Tactic:
refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)

Premises used: LinearEquiv.symm, AlgEquiv.symm, Algebra.IsPushout.cancelBaseChange, AlgEquiv.ofLinearEquiv
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
C : Type u_11
inst_47 : CommRing C
inst_48 : Algebra R C
inst_49 : Algebra A C
inst_50 : IsScalarTower R A C
⊢ Eq (α := B ⊗[A] C)
    (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) 1) 1

Tactic:
simp [TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
C : Type u_11
inst_47 : CommRing C
inst_48 : Algebra R C
inst_49 : Algebra A C
inst_50 : IsScalarTower R A C
refine_2 :
  ∀ (a₁ a₂ : S) (b₁ b₂ : C),
    (((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
          (a : S ⊗[R] C) → B ⊗[A] C)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := B ⊗[A] C) (β := B ⊗[A] C)
        ((((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
              (a : S ⊗[R] C) → B ⊗[A] C)
            (a₁ ⊗ₜ[R] b₁) :
          B ⊗[A] C)
        ((((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
              (a : S ⊗[R] C) → B ⊗[A] C)
            (a₂ ⊗ₜ[R] b₂) :
          B ⊗[A] C)
⊢ ∀ (x y : S ⊗[R] C),
    ((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) (x * y) =
      HMul.hMul (α := B ⊗[A] C) (β := B ⊗[A] C)
        (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) x :
          B ⊗[A] C)
        (((LinearEquiv.symm (cancelBaseChange R S A B C) : S ⊗[R] C ≃ₗ[S] B ⊗[A] C) : (a : S ⊗[R] C) → B ⊗[A] C) y :
          B ⊗[A] C)

Tactic:
apply LinearMap.map_mul_of_map_mul_tmul

Premises used: LinearMap.map_mul_of_map_mul_tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
C : Type u_11
inst_47 : CommRing C
inst_48 : Algebra R C
inst_49 : Algebra A C
inst_50 : IsScalarTower R A C
⊢ ∀ (a₁ a₂ : S) (b₁ b₂ : C),
    (((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
          (a : S ⊗[R] C) → B ⊗[A] C)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := B ⊗[A] C) (β := B ⊗[A] C)
        ((((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
              (a : S ⊗[R] C) → B ⊗[A] C)
            (a₁ ⊗ₜ[R] b₁) :
          B ⊗[A] C)
        ((((↑(LinearEquiv.symm (cancelBaseChange R S A B C)) : S ⊗[R] C →ₗ[S] B ⊗[A] C) : S ⊗[R] C →ₗ[S] B ⊗[A] C) :
              (a : S ⊗[R] C) → B ⊗[A] C)
            (a₂ ⊗ₜ[R] b₂) :
          B ⊗[A] C)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_8
B : Type u_9
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : IsPushout R S A B
C : Type u_11
inst_12 : CommRing C
inst_13 : Algebra R C
inst_14 : Algebra A C
inst_15 : IsScalarTower R A C
⊢ Eq (α := B ⊗[A] C ≃ₗ[S] S ⊗[R] C) (↑(cancelBaseChangeAlg R S A B C) : B ⊗[A] C ≃ₗ[S] S ⊗[R] C)
    (cancelBaseChange R S A B C)

Tactic:
rfl
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_8
B : Type u_9
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : IsPushout R S A B
C : Type u_11
inst_12 : CommRing C
inst_13 : Algebra R C
inst_14 : Algebra A C
inst_15 : IsScalarTower R A C
c : C
⊢ Eq (α := S ⊗[R] C) ((cancelBaseChangeAlg R S A B C : (a : B ⊗[A] C) → S ⊗[R] C) (1 ⊗ₜ[A] c) : S ⊗[R] C)
    (1 ⊗ₜ[R] c : S ⊗[R] C)

Tactic:
simp [cancelBaseChangeAlg]

Premises used: Algebra.IsPushout.cancelBaseChangeAlg
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_8
B : Type u_9
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : IsPushout R S A B
C : Type u_11
inst_12 : CommRing C
inst_13 : Algebra R C
inst_14 : Algebra A C
inst_15 : IsScalarTower R A C
s : S
c : C
⊢ Eq (α := B ⊗[A] C)
    ((AlgEquiv.symm (cancelBaseChangeAlg R S A B C) : (a : S ⊗[R] C) → B ⊗[A] C) (s ⊗ₜ[R] c) : B ⊗[A] C)
    ((algebraMap S B : (a : S) → B) s ⊗ₜ[A] c : B ⊗[A] C)

Tactic:
simp [cancelBaseChangeAlg]

Premises used: Algebra.IsPushout.cancelBaseChangeAlg
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_8
inst_1 : CommRing A
inst_2 : Algebra R A
C : Type u_11
inst_3 : CommRing C
inst_4 : Algebra R C
inst_5 : Algebra A C
inst_6 : IsScalarTower R A C
S : Type u_12
inst_7 : CommRing S
inst_8 : Algebra R S
h :
  ∀ (x : A),
    Eq (α := S ⊗[R] A ⊗[A] C)
      ((AlgHom.comp (B := S ⊗[R] A)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := S ⊗[R] C)
                    (↑(AlgEquiv.symm (cancelBaseChangeAlg R S A (S ⊗[R] A) C)) : S ⊗[R] C →ₐ[S] S ⊗[R] A ⊗[A] C)
                    (TensorProduct.lTensor S (toAlgHom R A C)) :
                  S ⊗[R] A →ₐ[S] S ⊗[R] A ⊗[A] C))
              TensorProduct.includeRight :
            (a : A) → S ⊗[R] A ⊗[A] C)
          x :
        S ⊗[R] A ⊗[A] C)
      ((AlgHom.comp (AlgHom.restrictScalars R (S := S) TensorProduct.includeLeft) TensorProduct.includeRight :
            (a : A) → S ⊗[R] A ⊗[A] C)
          x :
        S ⊗[R] A ⊗[A] C)
⊢ Eq (α := S ⊗[R] A →ₐ[S] S ⊗[R] A ⊗[A] C)
    (AlgHom.comp (B := S ⊗[R] C)
        (↑(AlgEquiv.symm (cancelBaseChangeAlg R S A (S ⊗[R] A) C)) : S ⊗[R] C →ₐ[S] S ⊗[R] A ⊗[A] C)
        (TensorProduct.lTensor S (toAlgHom R A C)) :
      S ⊗[R] A →ₐ[S] S ⊗[R] A ⊗[A] C)
    (TensorProduct.includeLeft : S ⊗[R] A →ₐ[S] S ⊗[R] A ⊗[A] C)

Tactic:
ext
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_8
inst_1 : CommRing A
inst_2 : Algebra R A
C : Type u_11
inst_3 : CommRing C
inst_4 : Algebra R C
inst_5 : Algebra A C
inst_6 : IsScalarTower R A C
S : Type u_12
inst_7 : CommRing S
inst_8 : Algebra R S
x : A
⊢ Eq (α := S ⊗[R] A ⊗[A] C)
    ((AlgHom.comp (B := S ⊗[R] A)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := S ⊗[R] C)
                  (↑(AlgEquiv.symm (cancelBaseChangeAlg R S A (S ⊗[R] A) C)) : S ⊗[R] C →ₐ[S] S ⊗[R] A ⊗[A] C)
                  (TensorProduct.lTensor S (toAlgHom R A C)) :
                S ⊗[R] A →ₐ[S] S ⊗[R] A ⊗[A] C))
            TensorProduct.includeRight :
          (a : A) → S ⊗[R] A ⊗[A] C)
        x :
      S ⊗[R] A ⊗[A] C)
    ((AlgHom.comp (AlgHom.restrictScalars R (S := S) TensorProduct.includeLeft) TensorProduct.includeRight :
          (a : A) → S ⊗[R] A ⊗[A] C)
        x :
      S ⊗[R] A ⊗[A] C)

Tactic:
simp [← TensorProduct.one_def, ← TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]

Premises used: Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Jacobson.Artinian
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsJacobsonRing R
inst_5 : IsSemisimpleRing A
⊢ Module.Finite R A

Tactic:
have (I : MaximalSpectrum A) := finite_of_finite_type_of_isJacobsonRing R (A ⧸ I.asIdeal)
  .equiv ((IsArtinianRing.equivPi A).restrictScalars R).toLinearEquiv.symm

Premises used: MaximalSpectrum.asIdeal, LinearEquiv.symm, finite_of_finite_type_of_isJacobsonRing, AlgEquiv.restrictScalars, HasQuotient.Quotient, IsArtinianRing.equivPi, AlgEquiv.toLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Jacobson.Artinian
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsJacobsonRing R
inst_5 : IsArtinianRing A
⊢ Module.Finite R A

Tactic:
have := finite_of_isSemisimpleRing R (A ⧸ Ring.jacobson A)
  IsSemiprimaryRing.finite_of_isArtinian R A A

Premises used: Module.finite_of_isSemisimpleRing, HasQuotient.Quotient, Ring.jacobson, IsSemiprimaryRing.finite_of_isArtinian
-- Module: Mathlib.RingTheory.Jacobson.Artinian
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsArtinianRing R
⊢ Module.Finite R A ↔ IsArtinianRing A

Tactic:
⟨isArtinian_of_tower _ ∘ ((IsArtinianRing.tfae R A).out 0 2).mp,
    fun _ ↦ finite_of_isArtinianRing R A⟩

Premises used: Function.comp, Module.finite_of_isArtinianRing, isArtinian_of_tower, List.TFAE.out, IsArtinianRing.tfae, Iff.intro, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Jacobson.Artinian
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsArtinianRing R
⊢ IsNoetherianRing A

Tactic:
have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A