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'
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
b : α
this :
  Eq.{u_4 + 1} (α := M') (if a = b then (f : (a : M) → M') m else 0 : M')
    ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] if a = b then m else 0) : M')
⊢ Eq.{u_4 + 1} (α := M')
    ((e : (a : Localization S ⊗[R] M) → 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) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')
    ((e : (a : Localization S ⊗[R] M) → 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) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')

Tactic:
simpa [e', Finsupp.single_apply, -EmbeddingLike.apply_eq_iff_eq, apply_ite]

Premises used: apply_ite, EmbeddingLike.apply_eq_iff_eq, Finsupp.single_apply
-- 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
b : α
h :
  Eq.{u_4 + 1} (α := M') (if a = b then (f : (a : M) → M') m else 0 : M')
    ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] if a = b then m else 0) : M')
⊢ Eq.{u_4 + 1} (α := M')
    ((e : (a : Localization S ⊗[R] M) → 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) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')
    ((e : (a : Localization S ⊗[R] M) → 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) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')

Tactic:
suffices (if a = b then f m else 0) = e (1 ⊗ₜ[R] if a = b then m else 0) by
    simpa [e', Finsupp.single_apply, -EmbeddingLike.apply_eq_iff_eq, apply_ite]
-- 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
b : α
pos :
  ∀ (h : a = b),
    Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') m : M') ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] m) : M')
neg : ∀ (h : ¬a = b), Eq.{u_4 + 1} (α := M') (0 : M') ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] 0) : M')
⊢ Eq.{u_4 + 1} (α := M') (if a = b then (f : (a : M) → M') m else 0 : M')
    ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] if a = b then m else 0) : M')

Tactic:
split_ifs with h
-- 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
b : α
h : a = b
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') m : M') ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] m) : M')

Tactic:
simp [e]
-- 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
b : α
h : ¬a = b
⊢ Eq.{u_4 + 1} (α := M') (0 : M') ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] 0) : M')

Tactic:
simp only [tmul_zero, map_zero]

Premises used: TensorProduct.tmul_zero, map_zero
-- 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'
α : Type u_7
v : α → M
inst_10 : IsLocalizedModule S f
h :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := M')
      ((((map S (mapRange.linearMap (Algebra.linearMap R A)) f : (a : (α →₀ R) →ₗ[R] M) → (α →₀ A) →ₗ[R] M')
                  (linearCombination R v) ∘ₗ
                mapRange.linearMap (Algebra.linearMap R A)) ∘ₗ
              lsingle a :
            (a : R) → M')
          1 :
        M')
      ((((↑R :
                    {S : Type u_2} →
                      {M : Type (max u_2 u_7)} →
                        {M₂ : Type u_4} →
                          [inst : Semiring R] →
                            [inst_11 : Semiring S] →
                              [inst_12 : AddCommMonoid M] →
                                [inst_13 : AddCommMonoid M₂] →
                                  [inst_14 : Module R M] →
                                    [inst_15 : Module R M₂] →
                                      [inst_16 : Module S M] →
                                        [inst_17 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (linearCombination A ((⇑f : (a : M) → M') ∘ v)) ∘ₗ
                mapRange.linearMap (Algebra.linearMap R A)) ∘ₗ
              lsingle a :
            (a : R) → M')
          1 :
        M')
⊢ Eq (α := (α →₀ R) →ₗ[R] M')
    ((map S (mapRange.linearMap (Algebra.linearMap R A)) f : (a : (α →₀ R) →ₗ[R] M) → (α →₀ A) →ₗ[R] M')
        (linearCombination R v) ∘ₗ
      mapRange.linearMap (Algebra.linearMap R A))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_7)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (linearCombination A ((⇑f : (a : M) → M') ∘ v)) ∘ₗ
      mapRange.linearMap (Algebra.linearMap R A))

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'
α : Type u_7
v : α → M
inst_10 : IsLocalizedModule S f
a : α
⊢ Eq.{u_4 + 1} (α := M')
    ((((map S (mapRange.linearMap (Algebra.linearMap R A)) f : (a : (α →₀ R) →ₗ[R] M) → (α →₀ A) →ₗ[R] M')
                (linearCombination R v) ∘ₗ
              mapRange.linearMap (Algebra.linearMap R A)) ∘ₗ
            lsingle a :
          (a : R) → M')
        1 :
      M')
    ((((↑R :
                  {S : Type u_2} →
                    {M : Type (max u_2 u_7)} →
                      {M₂ : Type u_4} →
                        [inst : Semiring R] →
                          [inst_11 : Semiring S] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module R M] →
                                  [inst_15 : Module R M₂] →
                                    [inst_16 : Module S M] →
                                      [inst_17 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (linearCombination A ((⇑f : (a : M) → M') ∘ v)) ∘ₗ
              mapRange.linearMap (Algebra.linearMap R A)) ∘ₗ
            lsingle a :
          (a : R) → M')
        1 :
      M')

Tactic:
simp [IsLocalizedModule.map_comp]

Premises used: IsLocalizedModule.map_comp
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S_1 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
S : Submonoid A
N : Type u_7
inst_18 : AddCommMonoid N
inst_19 : Module R N
inst_20 : Module A M
inst_21 : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization (M := A) S
this : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
⊢ IsScalarTower A Aₚ M'

Tactic:
haveI : IsScalarTower A Aₚ M' := (IsLocalizedModule.iso S g).symm.isScalarTower Aₚ
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S_1 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
S : Submonoid A
N : Type u_7
inst_18 : AddCommMonoid N
inst_19 : Module R N
inst_20 : Module A M
inst_21 : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization (M := A) S
this_1 : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this : IsScalarTower A Aₚ M'
r : R
x : M'
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := Aₚ) (((algebraMap R Aₚ : R →+* Aₚ) : (a : R) → Aₚ) r : Aₚ) x = r • x

Tactic:
simp [IsScalarTower.algebraMap_apply R A Aₚ]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S_1 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
S : Submonoid A
N : Type u_7
inst_18 : AddCommMonoid N
inst_19 : Module R N
inst_20 : Module A M
inst_21 : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization (M := A) S
this_1 : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this_2 : IsScalarTower A Aₚ M'
this : IsScalarTower R Aₚ M'
rw :
  ∀ (h : IsBaseChange Aₚ g) (this : IsScalarTower R Aₚ M'),
    IsBaseChange (R := A) (M := M ⊗[R] N) (N := M' ⊗[R] N) Aₚ
      (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)
⊢ IsLocalizedModule (M := M ⊗[R] N) (M' := M' ⊗[R] N) S
    (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
        (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
      g)

Tactic:
rw [isLocalizedModule_iff_isBaseChange (S := S) (A := Aₚ)] at h ⊢

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S_1 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
S : Submonoid A
N : Type u_7
inst_18 : AddCommMonoid N
inst_19 : Module R N
inst_20 : Module A M
inst_21 : IsScalarTower R A M
g : M →ₗ[A] M'
h_1 : IsLocalizedModule S g
Aₚ : Type u_2 := Localization (M := A) S
this_1 : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this_2 : IsScalarTower A Aₚ M'
h : IsBaseChange Aₚ g
this : IsScalarTower R Aₚ M'
⊢ IsBaseChange (R := A) (M := M ⊗[R] N) (N := M' ⊗[R] N) Aₚ
    (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
        (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
      g)

Tactic:
isBaseChange_tensorProduct_map _ h

Premises used: isBaseChange_tensorProduct_map, TensorProduct.AlgebraTensorModule.map, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S_1 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
S : Submonoid A
N : Type u_7
inst_18 : AddCommMonoid N
inst_19 : Module R N
inst_20 : Module A M
inst_21 : IsScalarTower R A M
g : M →ₗ[A] M'
h_1 : IsLocalizedModule S g
Aₚ : Type u_2 := Localization (M := A) S
this_1 : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this_2 : IsScalarTower A Aₚ M'
h : IsBaseChange Aₚ g
this : IsScalarTower R Aₚ M'
⊢ IsBaseChange (R := A) (M := M ⊗[R] N) (N := M' ⊗[R] N) Aₚ
    (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
        (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
      g)

Tactic:
exact isBaseChange_tensorProduct_map _ h

Premises used: isBaseChange_tensorProduct_map
-- 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
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
M' : Type u_4
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module A M'
inst_8 : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : Module A M
inst_12 : IsScalarTower R A M
P : Type u_8
inst_13 : AddCommMonoid P
inst_14 : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
h₁ :
  Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
    ((map S
            (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
                (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
              g)
            (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
                (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
              g) :
          (a : M ⊗[R] N →ₗ[A] M ⊗[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        (((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
          f) ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)
    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        f ∘ₗ
      ((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
          (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
        g)
⊢ Eq (α := M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
    ((map S
            (((AlgebraTensorModule.rTensor R N : (M →ₗ[A] M') →ₗ[R] M ⊗[R] N →ₗ[A] M' ⊗[R] N) :
                (a : M →ₗ[A] M') → M ⊗[R] N →ₗ[A] M' ⊗[R] N)
              g)
            (((AlgebraTensorModule.rTensor R P : (M →ₗ[A] M') →ₗ[R] M ⊗[R] P →ₗ[A] M' ⊗[R] P) :
                (a : M →ₗ[A] M') → M ⊗[R] P →ₗ[A] M' ⊗[R] P)
              g) :
          (a : M ⊗[R] N →ₗ[A] M ⊗[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        (((AlgebraTensorModule.lTensor A M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[A] M ⊗[R] P)
          f) :
      M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
    (((AlgebraTensorModule.lTensor A M' : (N →ₗ[R] P) →ₗ[R] M' ⊗[R] N →ₗ[A] M' ⊗[R] P) :
          (a : N →ₗ[R] P) → M' ⊗[R] N →ₗ[A] M' ⊗[R] P)
        f :
      M' ⊗[R] N →ₗ[A] M' ⊗[R] P)

Tactic:
apply linearMap_ext S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)

Premises used: TensorProduct.AlgebraTensorModule.rTensor, IsLocalizedModule.linearMap_ext, DFunLike.coe