-- 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'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h_1 : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun (l : M' →ₗ[R] Q) ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
g'' : M' →ₗ[A] Q
h :
  (fun (g' : M' →ₗ[A] Q) ↦
      (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type (max (max u_3 u_4) u_2)} →
                    [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₂)
            g' ∘ₗ
          f =
        ℓ ∘ₗ f)
    g''
⊢ g'' = LinearMap.extendScalarsOfIsLocalization S A ℓ
have refl : ∀
  (h₂ :
    ∀ (y : M' →ₗ[R] Q),
      (fun (l : M' →ₗ[R] Q) ↦
            l ∘ₗ f =
              (↑R :
                    {S : Type u_2} →
                      {M : Type u_4} →
                        {M₂ : Type (max (max u_2 u_3) 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₂)
                  g'' ∘ₗ
                f)
          y →
        y =
          (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type (max (max u_2 u_3) 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₂)
            g'')
  (h :
    Eq (α := M →ₗ[R] Q)
      ((↑R :
            {S : Type u_2} →
              {M : Type u_4} →
                {M₂ : Type (max (max u_3 u_4) u_2)} →
                  [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₂)
          g'' ∘ₗ
        f)
      ((↑R :
            {S : Type u_2} →
              {M : Type u_4} →
                {M₂ : Type (max (max u_2 u_3) 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₂)
          g'' ∘ₗ
        f)),
  g'' =
    LinearMap.extendScalarsOfIsLocalization S A
      ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max (max u_2 u_3) 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₂)
        g'')
Tactic: cases h₂ (LinearMap.restrictScalars R g'') h
Cleared hypotheses: ℓ, h₂, h