-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₄ :
  Eq.{u_2 + 1} (α := R)
    ((∑ x ∈ b.support,
            (P.toLinearMap : (a : M) → N →ₗ[R] R) (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₅ :
  Eq.{u_2 + 1} (α := R)
    ((∑ x ∈ b.support,
            HSMul.hSMul (β := N →ₗ[R] R) (f x)
              ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) x) : N →ₗ[R] R) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R) : R)
simp_rw₆ :
  Eq.{u_2 + 1} (α := R)
    ((∑ i ∈ b.support,
        (⇑(HSMul.hSMul (β := N →ₗ[R] R) (f i)
              ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R)) :
          (a : N) → R))
      ((P.coroot : (a : ι) → N) i))
    (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R))
simp_rw₇ :
  Eq.{u_2 + 1} (α := R)
    (∑ c ∈ b.support,
      (HSMul.hSMul (β := N →ₗ[R] R) (f c)
            ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) c) : N →ₗ[R] R) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N))
    (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R))
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₈ : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ b.support,
    HSMul.hSMul (β := R) (f x)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) x) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R))
  (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R))
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]