awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
x : R
rw :
  Eq.{u_8 + 1} (α := T') ((algebraMap S' T' : (a : S') → T') ((algebraMap R S' : (a : R) → S') x : S') : T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
⊢ Eq.{u_8 + 1} (α := T') ((algebraMap R T' : (a : R) → T') x : T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
have rw₁ : Eq.{u_8 + 1} (α := T')
  ((algebraMap S' T' : (a : S') → T') ((algebraMap S S' : (a : S) → S') ((algebraMap R S : (a : R) → S) x : S) : S') :
    T')
  ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
Tactic: rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
x : R
rw :
  Eq.{u_8 + 1} (α := T') ((algebraMap S' T' : (a : S') → T') ((algebraMap R S' : (a : R) → S') x : S') : T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
rw₁ :
  Eq.{u_8 + 1} (α := T')
    ((algebraMap S' T' : (a : S') → T') ((algebraMap S S' : (a : S) → S') ((algebraMap R S : (a : R) → S) x : S) : S') :
      T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
⊢ Eq.{u_8 + 1} (α := T') ((algebraMap R T' : (a : R) → T') x : T')
    ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
have rw₂ : Eq.{u_8 + 1} (α := T') ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
  ((algebraMap S T' : (a : S) → T') ((algebraMap R S : (a : R) → S) x : S) : T')
Tactic: rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'
have this : IsScalarTower R S T'
Tactic: haveI : IsScalarTower R S T' := .of_algebraMap_eq fun x ↦ by
    rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
this : IsScalarTower R S T'
⊢ Eq (α := R' →ₗ[R] T')
    ((↑R :
          {S : Type v₃} →
            {M : Type u_7} →
              {M₂ : Type u_8} →
                [inst : Semiring R] →
                  [inst_28 : Semiring S] →
                    [inst_29 : AddCommMonoid M] →
                      [inst_30 : AddCommMonoid M₂] →
                        [inst_31 : Module R M] →
                          [inst_32 : Module R M₂] →
                            [inst_33 : Module S M] →
                              [inst_34 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (AlgHom.toLinearMap (toAlgHom S S' T')) ∘ₗ
      f)
    (AlgHom.toLinearMap (toAlgHom R R' T'))
have h : ∀ (x : R'),
  Eq.{u_8 + 1} (α := T')
    (((↑R :
                {S : Type v₃} →
                  {M : Type u_7} →
                    {M₂ : Type u_8} →
                      [inst : Semiring R] →
                        [inst_28 : Semiring S] →
                          [inst_29 : AddCommMonoid M] →
                            [inst_30 : AddCommMonoid M₂] →
                              [inst_31 : Module R M] →
                                [inst_32 : Module R M₂] →
                                  [inst_33 : Module S M] →
                                    [inst_34 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (AlgHom.toLinearMap (toAlgHom S S' T')) ∘ₗ
            f :
          (a : R') → T')
        x :
      T')
    ((AlgHom.toLinearMap (toAlgHom R R' T') : (a : R') → T') x : T')
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
this : IsScalarTower R S T'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'
have heq : Eq (α := R' →ₗ[R] T')
  ((↑R :
        {S : Type v₃} →
          {M : Type u_7} →
            {M₂ : Type u_8} →
              [inst : Semiring R] →
                [inst_28 : Semiring S] →
                  [inst_29 : AddCommMonoid M] →
                    [inst_30 : AddCommMonoid M₂] →
                      [inst_31 : Module R M] →
                        [inst_32 : Module R M₂] →
                          [inst_33 : Module S M] →
                            [inst_34 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (AlgHom.toLinearMap (toAlgHom S S' T')) ∘ₗ
    f)
  (AlgHom.toLinearMap (toAlgHom R R' T'))
Tactic: have heq : (toAlgHom S S' T').toLinearMap.restrictScalars R ∘ₗ f =
      (toAlgHom R R' T').toLinearMap := by
    ext x
    simp [f, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst_7 : CommSemiring R'
inst_8 : CommSemiring S'
inst_9 : Algebra R R'
inst_10 : Algebra S S'
inst_11 : Algebra R' S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
T' : Type u_8
inst_15 : CommSemiring T'
inst_16 : Algebra R T'
inst_17 : Algebra S' T'
inst_18 : Algebra S T'
inst_19 : Algebra T T'
inst_20 : Algebra R' T'
inst_21 : IsScalarTower R T T'
inst_22 : IsScalarTower S T T'
inst_23 : IsScalarTower S S' T'
inst_24 : IsScalarTower R R' T'
inst_25 : IsScalarTower R S' T'
inst_26 : IsScalarTower R' S' T'
inst_27 : IsPushout R S R' S'
f : R' →ₗ[R] S' := AlgHom.toLinearMap (toAlgHom R R' S')
this : IsScalarTower R S T'
heq :
  Eq (α := R' →ₗ[R] T')
    ((↑R :
          {S : Type v₃} →
            {M : Type u_7} →
              {M₂ : Type u_8} →
                [inst : Semiring R] →
                  [inst_28 : Semiring S] →
                    [inst_29 : AddCommMonoid M] →
                      [inst_30 : AddCommMonoid M₂] →
                        [inst_31 : Module R M] →
                          [inst_32 : Module R M₂] →
                            [inst_33 : Module S M] →
                              [inst_34 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (AlgHom.toLinearMap (toAlgHom S S' T')) ∘ₗ
      f)
    (AlgHom.toLinearMap (toAlgHom R R' T'))
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'
have hf : IsBaseChange S f
Tactic: rw [isPushout_iff, isPushout_iff, ← heq, IsBaseChange.comp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R R' S S'
T : Type u_8
inst_11 : CommSemiring T
inst_12 : Algebra R' T
inst_13 : Algebra S T
inst_14 : Algebra R T
inst_15 : IsScalarTower R S T
inst_16 : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : Eq (α := S →+* T) (e.toRingEquiv.toRingHom.comp (algebraMap S S')) (algebraMap S T)
⊢ IsPushout R R' S T
have rw : ∀ (h : IsBaseChange R' (AlgHom.toLinearMap (toAlgHom R S S'))) {T : Type u_8} [inst_17 : CommSemiring T]
  [inst_18 : Algebra R' T] [inst_19 : Algebra S T] [inst_20 : Algebra R T] [inst_21 : IsScalarTower R S T]
  [inst_22 : IsScalarTower R R' T] (e : S' ≃ₐ[R'] T)
  (he : Eq (α := S →+* T) (e.toRingEquiv.toRingHom.comp (algebraMap S S')) (algebraMap S T)),
  IsBaseChange R' (AlgHom.toLinearMap (toAlgHom R S T))
Tactic: rw [isPushout_iff] at h ⊢
Cleared hypotheses: h, T, inst_11, inst_12, inst_13, inst_14, inst_15, inst_16, e, he
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsBaseChange R' (AlgHom.toLinearMap (toAlgHom R S S'))
T : Type u_8
inst_11 : CommSemiring T
inst_12 : Algebra R' T
inst_13 : Algebra S T
inst_14 : Algebra R T
inst_15 : IsScalarTower R S T
inst_16 : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : Eq (α := S →+* T) (e.toRingEquiv.toRingHom.comp (algebraMap S S')) (algebraMap S T)
⊢ IsBaseChange R' (AlgHom.toLinearMap (toAlgHom R S T))
have refine : ∀ (x : S),
  Eq.{u_8 + 1} (α := T) ((h.equiv ≪≫ₗ (↑e : S' ≃ₗ[R'] T) : (a : R' ⊗[R] S) → T) (1 ⊗ₜ[R] x) : T)
    ((AlgHom.toLinearMap (toAlgHom R S T) : (a : S) → T) x : T)
Tactic: refine IsBaseChange.of_equiv (h.equiv ≪≫ₗ e.toLinearEquiv) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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 : S ⊗[R] 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) =
    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)
have zero : ((↑(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: induction x with
    | zero => simp
    | add x y hx hy => simp only [smul_add, map_add, hx, hy]
    | tmul s' m => simp [Algebra.smul_def, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C
have 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
Tactic: refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C
have 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)
Tactic: refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
⊢ ∀ (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)
have 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)
Tactic: apply LinearMap.map_mul_of_map_mul_tmul
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Artinian (hypothesis)
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 ↔ Ring.KrullDimLE 0 A
have this : IsNoetherianRing A
Tactic: have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A