awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R_1 A
inst_3 : IsLocalization S_1 A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A M'
inst_9 : IsScalarTower R_1 A M'
f : M →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (IsUnit.submonoid R)) S

Tactic:
IsLocalization.of_le_isUnit Algebra.algebraMapSubmonoid_isUnit_le_isUnit

Premises used: Algebra.algebraMapSubmonoid_isUnit_le_isUnit, IsLocalization.of_le_isUnit
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsLocalization (IsUnit.submonoid R) A

Tactic:
have : IsLocalization (IsUnit.submonoid R) A :=
    IsLocalization.of_le_isUnit_of_bijective Algebra.algebraMapSubmonoid_isUnit_le_isUnit H
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this : IsLocalization (IsUnit.submonoid R) A
⊢ IsPushout R T A T

Tactic:
apply isPushout_of_isLocalization (IsUnit.submonoid R)

Premises used: Algebra.isPushout_of_isLocalization, IsUnit.submonoid
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
apply :
  LE.le (α := Submonoid T) (algebraMapSubmonoid T (algebraMapSubmonoid A (IsUnit.submonoid R))) (IsUnit.submonoid T)
⊢ IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T

Tactic:
apply IsLocalization.of_le_isUnit_of_bijective _ H

Premises used: IsLocalization.of_le_isUnit_of_bijective
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
⊢ LE.le (α := Submonoid T) (algebraMapSubmonoid T (algebraMapSubmonoid A (IsUnit.submonoid R))) (IsUnit.submonoid T)

Tactic:
simpa using Algebra.algebraMapSubmonoid_isUnit_le

Premises used: Algebra.algebraMapSubmonoid_isUnit_le
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
⊢ IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T

Tactic:
have : IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T := by
    apply IsLocalization.of_le_isUnit_of_bijective _ H
    simpa using Algebra.algebraMapSubmonoid_isUnit_le
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
this : IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T
⊢ IsPushout R A R T

Tactic:
apply Algebra.isPushout_of_isLocalization (IsUnit.submonoid R)

Premises used: Algebra.isPushout_of_isLocalization, IsUnit.submonoid
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule S
    ((↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
      (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)

Tactic:
this.of_linearEquiv (e := e')

Premises used: IsLocalizedModule.of_linearEquiv
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
h :
  Finsupp.mapRange.linearMap f =
    (↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
      (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)

Tactic:
convert! this.of_linearEquiv (e := e')

Premises used: IsLocalizedModule.of_linearEquiv
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
h :
  ∀ (a : α) (x : M) (a_1 : α),
    Eq.{u_4 + 1} (α := M')
      ((((Finsupp.mapRange.linearMap f ∘ₗ Finsupp.lsingle a : (a : M) → α →₀ M') x : α →₀ M') : (a : α) → M') a_1 : M')
      ((((((↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
                      (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
                    Finsupp.lsingle a :
                  (a : M) → α →₀ M')
                x :
              α →₀ M') :
            (a : α) → M')
          a_1 :
        M')
⊢ Finsupp.mapRange.linearMap f =
    (↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
      (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f

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'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
a : α
x : M
a_1 : α
⊢ Eq.{u_4 + 1} (α := M')
    ((((Finsupp.mapRange.linearMap f ∘ₗ Finsupp.lsingle a : (a : M) → α →₀ M') x : α →₀ M') : (a : α) → M') a_1 : M')
    ((((((↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
                    (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
                  Finsupp.lsingle a :
                (a : M) → α →₀ M')
              x :
            α →₀ M') :
          (a : α) → M')
        a_1 :
      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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
suffices :
  IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)

Tactic:
suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
rw :
  IsBaseChange (Localization (M := R) S)
    ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)

Tactic:
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]

Premises used: isLocalizedModule_iff_isBaseChange, Localization
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
⊢ IsBaseChange (R := R) (M := α →₀ M) (N := Localization (M := R) S ⊗[R] (α →₀ M)) (Localization (M := R) S)
    ((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M)) 1)

Tactic:
TensorProduct.isBaseChange R (α →₀ M) (Localization S)

Premises used: Localization, TensorProduct.isBaseChange, Finsupp
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
h :
  (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f =
    (mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M)) 1
⊢ IsBaseChange (Localization (M := R) S)
    ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)

Tactic:
convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1

Premises used: Localization, TensorProduct.isBaseChange, Finsupp
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
h :
  ∀ (a : α) (m : M),
    Eq (α := Localization (M := R) S ⊗[R] (α →₀ M))
      ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
              Finsupp.lsingle a :
            (a : M) → Localization S ⊗[R] (α →₀ M))
          m :
        Localization (M := R) S ⊗[R] (α →₀ M))
      (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
                1 ∘ₗ
              Finsupp.lsingle a :
            (a : M) → Localization S ⊗[R] (α →₀ M))
          m :
        Localization (M := R) S ⊗[R] (α →₀ M))
⊢ (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f =
    (mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M)) 1

Tactic:
ext a m
-- 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
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
a : α
m : M
h :
  Eq (α := α →₀ Localization (M := R) S ⊗[R] M)
    (((finsuppRight R R (Localization (M := R) S) M α :
            Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
          (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
        ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
              Finsupp.lsingle a :
            (a : M) → Localization S ⊗[R] (α →₀ M))
          m) :
      α →₀ Localization (M := R) S ⊗[R] M)
    (((finsuppRight R R (Localization (M := R) S) M α :
            Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
          (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
        (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
                1 ∘ₗ
              Finsupp.lsingle a :
            (a : M) → Localization S ⊗[R] (α →₀ M))
          m) :
      α →₀ Localization (M := R) S ⊗[R] M)
⊢ Eq (α := Localization (M := R) S ⊗[R] (α →₀ M))
    ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))
    (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
              1 ∘ₗ
            Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))

Tactic:
apply (finsuppRight R R (Localization S) M α).injective

Premises used: TensorProduct.finsuppRight, Localization, LinearEquiv.injective