-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
rw :
  (((B.form : (a : M) → M →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M)
                ((P.coroot' j : (a : M) → R) ((P.root : (a : ι) → M) i : M) : R) ((P.root : (a : ι) → M) j : M))) :
          M →ₗ[R] R) :
        (a : M) → R)
      ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
rw₁ :
  (((B.form : (a : M) → M →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M)
                ((P.coroot' j : (a : M) → R) ((P.root : (a : ι) → M) i : M) : R) ((P.root : (a : ι) → M) j : M))) :
          M →ₗ[R] R) :
        (a : M) → R)
      (-(P.root : (a : ι) → M) j : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
rw₂ :
  (((B.form : (a : M) → M →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))) :
          M →ₗ[R] R) :
        (a : M) → R)
      (-(P.root : (a : ι) → M) j : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
⊢ (((B.form : (a : M) → M →ₗ[R] R) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M)) : M →ₗ[R] R) :
        (a : M) → R)
      ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) =
    HSub.hSub (β := R)
      (HMul.hMul (β := R) (P.pairing i j)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
have rw₃ : HSub.hSub (α := R) (β := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        (-(P.root : (a : ι) → M) j : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) :
            M →ₗ[R] R) :
          (a : M) → R)
        (-(P.root : (a : ι) → M) j : M) :
      R) =
  HSub.hSub (β := R)
    (HMul.hMul (β := R) (P.pairing i j)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
Tactic: rw [reflection_apply, reflection_apply_self, root_coroot'_eq_pairing, LinearMap.map_sub₂,
    LinearMap.map_smul₂, smul_eq_mul, map_neg, map_neg, mul_neg, neg_sub_neg]