-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i j : ι
⊢ HSub.hSub (α := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      (({
              toFun := fun (i : ι) ↦
                Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                    x)
                  ((P.root : (a : ι) → M) i) ⋯,
              inj' := ⋯ :
              Embedding.{u_1 + 1, u_3 + 1} ι ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
            (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
          j :
        ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      (HSMul.hSMul.{u_5, u_3, u_3} (α := K) (β := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
        ((((LinearMap.restrictScalarsRange₂
                      (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
                      (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
                      (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯ :
                    (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) →
                      ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
                  (({
                        toFun := fun (i : ι) ↦
                          Subtype.mk (p := fun (x : M) ↦
                            Membership.mem (γ := Submodule K M)
                              (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                            ((P.root : (a : ι) → M) i) ⋯,
                        inj' := ⋯ :
                        Embedding.{u_1 + 1, u_3 + 1} ι
                          ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
                      (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
                    j) :
                LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
                  (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
              (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
            (({
                    toFun := fun (i : ι) ↦
                      Subtype.mk (p := fun (x : N) ↦
                        Membership.mem (γ := Submodule K N)
                          (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
                        ((P.coroot : (a : ι) → N) i) ⋯,
                    inj' := ⋯ :
                    Embedding.{u_1 + 1, u_4 + 1} ι
                      ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) } :
                  (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
                i :
              ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
          K)
        (({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                      x)
                    ((P.root : (a : ι) → M) i) ⋯,
                inj' := ⋯ :
                Embedding.{u_1 + 1, u_3 + 1} ι ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
              (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
            i :
          ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))) =
    ({
          toFun := fun (i : ι) ↦
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
              ((P.root : (a : ι) → M) i) ⋯,
          inj' := ⋯ } :
        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
      ((P.reflectionPerm i : (a : ι) → ι) j)
have a : (↑(HSub.hSub (α := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
        (({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
                      x)
                    ((P.root : (a : ι) → M) i) sorry,
                inj' := sorry :
                Embedding.{u_1 + 1, u_3 + 1} ι ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
              (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
            j :
          ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
        (HSMul.hSMul.{u_5, u_3, u_3} (α := K) (β := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
          ((((LinearMap.restrictScalarsRange₂
                        (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
                        (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
                        (Algebra.linearMap K L) sorry P.toLinearMap sorry :
                      (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
                    (({
                          toFun := fun (i : ι) ↦
                            Subtype.mk (p := fun (x : M) ↦
                              Membership.mem (γ := Submodule K M)
                                (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                              ((P.root : (a : ι) → M) i) sorry,
                          inj' := sorry :
                          Embedding.{u_1 + 1, u_3 + 1} ι
                            ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
                        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
                      j) :
                  LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
                    (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
                (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
              (({
                      toFun := fun (i : ι) ↦
                        Subtype.mk (p := fun (x : N) ↦
                          Membership.mem (γ := Submodule K N)
                            (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
                          ((P.coroot : (a : ι) → N) i) sorry,
                      inj' := sorry :
                      Embedding.{u_1 + 1, u_4 + 1} ι
                        ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) } :
                    (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
                  i :
                ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
            K)
          (({
                  toFun := fun (i : ι) ↦
                    Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := Submodule K M)
                        (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                      ((P.root : (a : ι) → M) i) sorry,
                  inj' := sorry :
                  Embedding.{u_1 + 1, u_3 + 1} ι ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) } :
                (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
              i :
            ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))))) :
    M) =
  (↑(({
            toFun := fun (i : ι) ↦
              Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                ((P.root : (a : ι) → M) i) sorry,
            inj' := sorry } :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
        ((P.reflectionPerm i : (a : ι) → ι) j)) :
    M)
Tactic: ext