-- 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)
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)
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
have 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')
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]