awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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 : α
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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 : α
⊢ 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')
have 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')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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')
⊢ 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')
have neg : ∀ (h : ¬a = b), Eq.{u_4 + 1} (α := M') (0 : M') ((e : (a : Localization S ⊗[R] M) → M') (1 ⊗ₜ[R] 0) : M')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
let let₁ let₂ let₃ : IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
have let₄ : let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f;
let 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');
IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
Tactic: classical
  let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
    (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f
  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ M') :=
    finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
  suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    simp
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1
  ext a m
  apply (finsuppRight R R (Localization S) M α).injective
  ext b
  apply e.injective
  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]
  split_ifs with h
  · simp [e]
  · simp only [tmul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
let let₁ let₂ let₃ : IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
let₄ :
  let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
    LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
      IsLocalizedModule.iso S f;
  let 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');
  IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
have let₅ : let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f;
let 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 (Localization (M := R) S)
  ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
Tactic: classical
  let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
    (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f
  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ M') :=
    finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
  suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    simp
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1
  ext a m
  apply (finsuppRight R R (Localization S) M α).injective
  ext b
  apply e.injective
  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]
  split_ifs with h
  · simp [e]
  · simp only [tmul_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ 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))
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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
⊢ 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)
have this₁ : IsScalarTower A Aₚ M'
Tactic: haveI : IsScalarTower A Aₚ M' := (IsLocalizedModule.iso S g).symm.isScalarTower Aₚ
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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'
⊢ 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)
have 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)
Tactic: rw [isLocalizedModule_iff_isBaseChange (S := S) (A := Aₚ)] at h ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ 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)
have 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)
Tactic: apply linearMap_ext S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ 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)
have h₁ : Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
  (((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 ∘ₗ
    ((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.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)
Tactic: rw [map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M' ⊗[R] P)
    (((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 ∘ₗ
      ((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.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)
have h₁ : ∀ (x : M) (x_1 : N),
  Eq (α := M' ⊗[R] P)
    (((((AlgebraTensorModule.curry
                    (((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 ∘ₗ
                      ((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 →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                (a : M) → N →ₗ[R] M' ⊗[R] P)
              x :
            N →ₗ[R] M' ⊗[R] P) :
          (a : N) → M' ⊗[R] P)
        x_1 :
      M' ⊗[R] P)
    (((((AlgebraTensorModule.curry
                    (((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) :
                  M →ₗ[A] N →ₗ[R] M' ⊗[R] P) :
                (a : M) → N →ₗ[R] M' ⊗[R] P)
              x :
            N →ₗ[R] M' ⊗[R] P) :
          (a : N) → M' ⊗[R] P)
        x_1 :
      M' ⊗[R] P)
Tactic: ext