-- 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
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)
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)
h :
  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');
  (↑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
h₁ :
  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');
  ∀ (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))
h₂ :
  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');
  ∀ (a : α) (m : M),
    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)
h₃ :
  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');
  ∀ (a : α) (m : M) (b : α),
    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) :
            (a : α) → Localization S ⊗[R] M)
          b :
        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) :
            (a : α) → Localization S ⊗[R] M)
          b :
        Localization (M := R) S ⊗[R] M)
h₄ :
  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');
  ∀ (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')
h₅ :
  let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
    LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
      IsLocalizedModule.iso S f;
  ∀ (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')
pos :
  let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
    LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
      IsLocalizedModule.iso S f;
  ∀ (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')
neg neg₁ :
  let e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
    LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
      IsLocalizedModule.iso S f;
  ∀ (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')
⊢ IsLocalizedModule (M := α →₀ M) S (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]

Premises used: isLocalizedModule_iff_isBaseChange, TensorProduct.tmul_zero, map_zero, Localization, TensorProduct.isBaseChange, Finsupp