awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
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 S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
    ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)

Tactic:
(AlgHom.congr_fun h₂ s :)

Premises used: AlgHom.congr_fun
-- Module: Mathlib.RingTheory.IsTensorProduct
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 S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
    ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)

Tactic:
exact (AlgHom.congr_fun h₂ s :)

Premises used: AlgHom.congr_fun
-- Module: Mathlib.RingTheory.IsTensorProduct
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 S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x s₁ s₂ : S'
e₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₁ : A)
e₂ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s₂ : A) ((g : (a : S') → A) s₂ : A)
H₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) = (g : (a : S') → A) (s₁ + s₂)
H₂ :
  HAdd.hAdd (α := A) (β := A) ((f : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
H₃ :
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((f : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
H₄ H₅ :
  HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A) =
    HAdd.hAdd (α := A) (β := A) ((g : (a : S') → A) s₁ : A) ((g : (a : S') → A) s₂ : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s₁ + s₂) : A) ((g : (a : S') → A) (s₁ + s₂) : A)

Tactic:
rw [map_add, map_add, e₁, e₂]

Premises used: map_add
-- Module: Mathlib.RingTheory.IsTensorProduct
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')
rw₂ 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')

Tactic:
rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IsTensorProduct
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')
⊢ 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']
-- Module: Mathlib.RingTheory.IsTensorProduct
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'
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')
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.IsTensorProduct
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'
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:
simp [f, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IsTensorProduct
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'))

Tactic:
have heq : (toAlgHom S S' T').toLinearMap.restrictScalars R ∘ₗ f =
      (toAlgHom R R' T').toLinearMap := by
    ext x
    simp [f, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.IsTensorProduct
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'))
hf : IsBaseChange S f
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
rw [isPushout_iff, isPushout_iff, ← heq, IsBaseChange.comp_iff]

Premises used: IsBaseChange.comp_iff, Algebra.isPushout_iff
-- Module: Mathlib.RingTheory.IsTensorProduct
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'))
⊢ IsBaseChange S f

Tactic:
Algebra.IsPushout.out

Premises used: Algebra.IsPushout.out
-- Module: Mathlib.RingTheory.IsTensorProduct
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'))
⊢ IsBaseChange S f

Tactic:
exact Algebra.IsPushout.out

Premises used: Algebra.IsPushout.out
-- Module: Mathlib.RingTheory.IsTensorProduct
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)
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))
⊢ IsPushout R R' S T

Tactic:
rw [isPushout_iff] at h ⊢

Premises used: Algebra.isPushout_iff
-- Module: Mathlib.RingTheory.IsTensorProduct
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))

Tactic:
IsBaseChange.of_equiv (h.equiv ≪≫ₗ e.toLinearEquiv) fun x ↦ ?_

Premises used: IsBaseChange.of_equiv, AlgEquiv.toLinearEquiv, LinearEquiv.trans, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
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)
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)
⊢ IsBaseChange R' (AlgHom.toLinearMap (toAlgHom R S T))

Tactic:
refine IsBaseChange.of_equiv (h.equiv ≪≫ₗ e.toLinearEquiv) fun x ↦ ?_

Premises used: IsBaseChange.of_equiv, AlgEquiv.toLinearEquiv, LinearEquiv.trans, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
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)
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:
simpa [h.equiv_tmul] using DFunLike.congr_fun he x

Premises used: DFunLike.congr_fun, IsBaseChange.equiv_tmul
-- 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 (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] 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:
simp [IsPushout.cancelBaseChangeAux, IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul, Algebra.IsPushout.cancelBaseChangeAux