awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
h₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
      (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
⊢ f = (↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₄ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₅ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((h.equiv : (a : TensorProduct R A M) → M')
        ((this.equiv.symm : (a : LocalizedModule S M) → TensorProduct R A M)
            ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x) :
          TensorProduct R A M) :
      M')
h₆ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((h.equiv : (a : TensorProduct R A M) → M') (1 ⊗ₜ[R] x) : M')
h₇ : (f : (a : M) → M') x = HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M') 1 ((f : (a : M) → M') x : M')
h₈ h₉ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') x : M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')

Tactic:
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]

Premises used: LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply, one_smul, LinearMap.coe_comp, IsBaseChange.equiv_tmul, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
s : ↥S
⊢ (LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
      (Localization.mk r s ⊗ₜ[R] x) =
    HSMul.hSMul (β := LocalizedModule S M) r (mk x s)

Tactic:
simp [equivTensorProduct, IsBaseChange.equiv_tmul, mk_smul_mk, smul'_mk]

Premises used: LocalizedModule.smul'_mk, LocalizedModule.equivTensorProduct, IsBaseChange.equiv_tmul, LocalizedModule.mk_smul_mk
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := LocalizedModule S M)
    ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M) (1 ⊗ₜ[R] x) :
      LocalizedModule S M)
    (mk x 1 : LocalizedModule S M)

Tactic:
simp [← Localization.mk_one]

Premises used: Localization.mk_one
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
s : ↥S
a :
  Eq (α := LocalizedModule S M)
    ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
        ((equivTensorProduct S M : (a : LocalizedModule S M) → Localization S ⊗[R] M) (mk x s)) :
      LocalizedModule S M)
    ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
        (Localization.mk 1 s ⊗ₜ[R] x) :
      LocalizedModule S M)
⊢ Eq (α := Localization (M := R) S ⊗[R] M)
    ((equivTensorProduct S M : (a : LocalizedModule S M) → Localization S ⊗[R] M) (mk x s) :
      Localization (M := R) S ⊗[R] M)
    (Localization.mk 1 s ⊗ₜ[R] x : Localization (M := R) S ⊗[R] M)

Tactic:
apply (equivTensorProduct S M).symm.injective

Premises used: LinearEquiv.symm, LocalizedModule.equivTensorProduct, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
s : ↥S
⊢ Eq (α := LocalizedModule S M)
    ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
        ((equivTensorProduct S M : (a : LocalizedModule S M) → Localization S ⊗[R] M) (mk x s)) :
      LocalizedModule S M)
    ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
        (Localization.mk 1 s ⊗ₜ[R] x) :
      LocalizedModule S M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
inst_10 : CommSemiring T
inst_11 : Algebra R T
rw :
  IsBaseChange (M := T) (N := A ⊗[R] T) A
    (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
      [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
        [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)
⊢ IsLocalizedModule (M := T) (M' := A ⊗[R] T) S
    (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
      [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
        [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)

Tactic:
rw [isLocalizedModule_iff_isBaseChange (S := S) (A := A)]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
inst_10 : CommSemiring T
inst_11 : Algebra R T
⊢ IsBaseChange (M := T) (N := A ⊗[R] T) A
    (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
      [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
        [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)

Tactic:
TensorProduct.isBaseChange _ _ _

Premises used: SemilinearMapClass.semilinearMap, TensorProduct.isBaseChange, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
inst_10 : CommSemiring T
inst_11 : Algebra R T
⊢ IsBaseChange (M := T) (N := A ⊗[R] T) A
    (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
      [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
        [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)

Tactic:
exact TensorProduct.isBaseChange _ _ _

Premises used: TensorProduct.isBaseChange
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
⊢ IsLocalizedModule (M := M) (M' := A ⊗[R] M) S ((mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)

Tactic:
(isLocalizedModule_iff_isBaseChange _ A _).mpr (TensorProduct.isBaseChange _ _ _)

Premises used: Iff.mpr, isLocalizedModule_iff_isBaseChange, TensorProduct.isBaseChange
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
a : A
x : M₁
x_1 : M₂
obtain : ∀ (r : R) (s : ↥S), Eq (α := M₁ ⊗[R] M₂) ((mk' A r s • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (mk' A r s • x_1))
⊢ Eq (α := M₁ ⊗[R] M₂) ((a • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (a • x_1))

Tactic:
obtain ⟨r, s, rfl⟩ := exists_mk'_eq S a

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
x : M₁
x_1 : M₂
r : R
s : ↥S
rw :
  HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) (x ⊗ₜ[R] (mk' A r s • x_1))
⊢ Eq (α := M₁ ⊗[R] M₂) ((mk' A r s • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (mk' A r s • x_1))

Tactic:
rw [← (map_units A s).smul_left_cancel]

Premises used: IsUnit.smul_left_cancel, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
x : M₁
x_1 : M₂
r : R
s : ↥S
simp_rw :
  HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) (x ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₁ : Eq (α := M₁ ⊗[R] M₂) (((↑s : R) • mk' A r s • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₂ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₃ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] ((↑s : R) • mk' A r s • x_1))
simp_rw₄ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (((↑s : R) • mk' A r s) • x_1))
simp_rw₅ :
  Eq (α := M₁ ⊗[R] M₂) (HSMul.hSMul.{u_2, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) x ⊗ₜ[R] x_1)
    (x ⊗ₜ[R] HSMul.hSMul.{u_2, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) x_1)
simp_rw₆ : Eq (α := M₁ ⊗[R] M₂) ((r • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (r • x_1))
⊢ HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) (x ⊗ₜ[R] (mk' A r s • x_1))

Tactic:
simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
      algebraMap_smul, smul_tmul]

Premises used: TensorProduct.smul_tmul, smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type u_5
M₂ : Type u_6
B : Type ?u.63057
C : Type ?u.63180
inst_10 : AddCommMonoid M₁
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₁
inst_13 : Module R M₂
inst_14 : Module A M₁
inst_15 : Module A M₂
inst_16 : IsScalarTower R A M₁
inst_17 : IsScalarTower R A M₂
inst_18 : Semiring B
inst_19 : Algebra R B
inst_20 : Algebra A B
inst_21 : IsScalarTower R A B
inst_22 : Semiring C
inst_23 : Algebra R C
inst_24 : Algebra A C
inst_25 : IsScalarTower R A C
inst_26 : Module.{u_1, u_5} (Localization (M := R) S) M₁
inst_27 : Module.{u_1, u_6} (Localization (M := R) S) M₂
inst_28 : IsScalarTower R (Localization (M := R) S) M₁
inst_29 : IsScalarTower R (Localization (M := R) S) M₂
⊢ CompatibleSMul R (Localization (M := R) S) M₁ M₂

Tactic:
tensorProduct_compatibleSMul S ..

Premises used: IsLocalization.tensorProduct_compatibleSMul
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.68522
M₂ : Type ?u.68525
B : Type ?u.70458
C : Type ?u.70581
inst_10 : AddCommMonoid M₁
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₁
inst_13 : Module R M₂
inst_14 : Module A M₁
inst_15 : Module A M₂
inst_16 : IsScalarTower R A M₁
inst_17 : IsScalarTower R A M₂
inst_18 : Semiring B
inst_19 : Algebra R B
inst_20 : Algebra A B
inst_21 : IsScalarTower R A B
inst_22 : Semiring C
inst_23 : Algebra R C
inst_24 : Algebra A C
inst_25 : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst_26 : AddCommMonoid N
inst_27 : Module R N
inst_28 : AddCommMonoid N'
inst_29 : Module R N'
g : N →ₗ[R] N'
inst_30 : IsLocalizedModule S f
inst_31 : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization (M := R) S ⊗[R] M :=
  IsLocalizedModule.linearEquiv S f
    ((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M) 1)
eN : N' ≃ₗ[R] Localization (M := R) S ⊗[R] N :=
  IsLocalizedModule.linearEquiv S g
    ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N) 1)
⊢ IsLocalizedModule (M := M ⊗[R] N) S
    ((↑(LinearEquiv.restrictScalars R (AlgebraTensorModule.distribBaseChange R (Localization (M := R) S) M N) ≪≫ₗ
            LinearEquiv.symm
              (TensorProduct.congr eM eN ≪≫ₗ
                TensorProduct.equivOfCompatibleSMul (Localization (M := R) S) R R (Localization (M := R) S ⊗[R] M)
                  (Localization (M := R) S ⊗[R] N))) :
        Localization S ⊗[R] (M ⊗[R] N) →ₗ[R] M' ⊗[R] N') ∘ₗ
      (mk R (Localization (M := R) S) (M ⊗[R] N) : (a : Localization S) → M ⊗[R] N →ₗ[R] Localization S ⊗[R] (M ⊗[R] N))
        1)

Tactic:
IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm

Premises used: LinearEquiv.symm, TensorProduct.AlgebraTensorModule.distribBaseChange, LinearEquiv.restrictScalars, Localization, TensorProduct.congr, TensorProduct, IsLocalizedModule.of_linearEquiv, OfNat.ofNat, LinearEquiv.trans, DFunLike.coe, TensorProduct.mk, TensorProduct.equivOfCompatibleSMul
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.68522
M₂ : Type ?u.68525
B : Type ?u.70458
C : Type ?u.70581
inst_10 : AddCommMonoid M₁
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₁
inst_13 : Module R M₂
inst_14 : Module A M₁
inst_15 : Module A M₂
inst_16 : IsScalarTower R A M₁
inst_17 : IsScalarTower R A M₂
inst_18 : Semiring B
inst_19 : Algebra R B
inst_20 : Algebra A B
inst_21 : IsScalarTower R A B
inst_22 : Semiring C
inst_23 : Algebra R C
inst_24 : Algebra A C
inst_25 : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst_26 : AddCommMonoid N
inst_27 : Module R N
inst_28 : AddCommMonoid N'
inst_29 : Module R N'
g : N →ₗ[R] N'
inst_30 : IsLocalizedModule S f
inst_31 : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization (M := R) S ⊗[R] M :=
  IsLocalizedModule.linearEquiv S f
    ((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M) 1)
eN : N' ≃ₗ[R] Localization (M := R) S ⊗[R] N :=
  IsLocalizedModule.linearEquiv S g
    ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N) 1)
h :
  TensorProduct.map f g =
    (↑(LinearEquiv.restrictScalars R (AlgebraTensorModule.distribBaseChange R (Localization (M := R) S) M N) ≪≫ₗ
            LinearEquiv.symm
              (TensorProduct.congr eM eN ≪≫ₗ
                TensorProduct.equivOfCompatibleSMul (Localization (M := R) S) R R (Localization (M := R) S ⊗[R] M)
                  (Localization (M := R) S ⊗[R] N))) :
        Localization S ⊗[R] (M ⊗[R] N) →ₗ[R] M' ⊗[R] N') ∘ₗ
      (mk R (Localization (M := R) S) (M ⊗[R] N) : (a : Localization S) → M ⊗[R] N →ₗ[R] Localization S ⊗[R] (M ⊗[R] N))
        1
⊢ IsLocalizedModule S (TensorProduct.map f g)

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm

Premises used: LinearEquiv.symm, TensorProduct.AlgebraTensorModule.distribBaseChange, LinearEquiv.restrictScalars, Localization, TensorProduct.congr, TensorProduct, IsLocalizedModule.of_linearEquiv, OfNat.ofNat, LinearEquiv.trans, DFunLike.coe, TensorProduct.mk, TensorProduct.equivOfCompatibleSMul
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
⊢ Function.Bijective (α := A ⊗[R] A) (β := A) (⇑(LinearMap.mul' R A) : (a : A ⊗[R] A) → A)

Tactic:
have := tensorProduct_compatibleSMul S A A A
  (Algebra.TensorProduct.lmulEquiv R A).bijective

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.lmulEquiv, IsLocalization.tensorProduct_compatibleSMul, TensorProduct, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
T : Type u_5
B : Type u_6
inst_4 : CommSemiring T
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra T B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R T B
inst_11 : IsScalarTower R A B
rw :
  IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
    IsBaseChange A (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))
⊢ IsLocalization (algebraMapSubmonoid T S) B ↔ IsPushout R T A B

Tactic:
rw [Algebra.IsPushout.comm, Algebra.isPushout_iff, ← isLocalizedModule_iff_isLocalization]

Premises used: Algebra.IsPushout.comm, isLocalizedModule_iff_isLocalization, Algebra.isPushout_iff
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
T : Type u_5
B : Type u_6
inst_4 : CommSemiring T
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra T B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R T B
inst_11 : IsScalarTower R A B
rw rw₁ :
  IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
    IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
    IsBaseChange A (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))

Tactic:
rw [← isLocalizedModule_iff_isBaseChange (S := S)]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
T : Type u_5
B : Type u_6
inst_4 : CommSemiring T
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra T B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R T B
inst_11 : IsScalarTower R A B
inst_12 : IsLocalization (algebraMapSubmonoid T S) B
⊢ IsPushout R T A B

Tactic:
(Algebra.isLocalization_iff_isPushout S _).mp inferInstance

Premises used: inferInstance, Iff.mp, Algebra.isLocalization_iff_isPushout
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
M : Type u_7
N : Type u_8
inst : Monoid M
inst_1 : Monoid N
F : Type u_9
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
y : M
hy : y ∈ (↑(IsUnit.submonoid M) : Set M)
⊢ Membership.mem (α := N) (γ := Submonoid N) (IsUnit.submonoid N) ((f : (a : M) → N) y : N)

Tactic:
hy.map _

Premises used: Set.Mem, setOf, IsUnit, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
M : Type u_7
N : Type u_8
inst : Monoid M
inst_1 : Monoid N
F : Type u_9
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
y : M
hy : y ∈ (↑(IsUnit.submonoid M) : Set M)
⊢ Membership.mem (α := N) (γ := Submonoid N) (IsUnit.submonoid N) ((f : (a : M) → N) y : N)

Tactic:
exact hy.map _

Premises used: IsUnit.map
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
y : R
hy : y ∈ (↑(IsUnit.submonoid R) : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
hy.map _

Premises used: Set.Mem, setOf, IsUnit, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
y : R
hy : y ∈ (↑(IsUnit.submonoid R) : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact hy.map _

Premises used: IsUnit.map