-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
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)))))) :
      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)) :
      M)

Tactic:
simpa [algebra_compatible_smul L] using P.reflectionPerm_root i j

Premises used: algebra_compatible_smul, RootPairing.reflectionPerm_root