awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
⊢ HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)

Tactic:
rw [h₂, h₃] at h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₅ :
  HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
⊢ lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j

Tactic:
rw [h₂, h₃] at h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₅ :
  HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₆ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
⊢ HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j

Tactic:
rw [h₂, h₃] at h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₅ :
  HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₆ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₇ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
⊢ P.pairing j i * lsq i = P.pairing i j * lsq j

Tactic:
rw [h₂, h₃] at h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
⊢ Eq.{u_4 + 1} (α := N)
    ((fun (n : N) ↦ P.pairing j i • n)
      (HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
        ((P.coroot : (a : ι) → N) k : N)))
    ((fun (n : N) ↦ P.pairing j i • n)
      (HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
        HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)))

Tactic:
replace h₁ := congr_arg (fun n ↦ P.pairing j i • n) h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  Eq.{u_4 + 1} (α := N)
    ((fun (n : N) ↦ P.pairing j i • n)
      (HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
        ((P.coroot : (a : ι) → N) k : N)))
    ((fun (n : N) ↦ P.pairing j i • n)
      (HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
        HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)))
⊢ HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
simp only [add_smul, smul_add, ← mul_smul, smul_eq_mul] at h₁

Premises used: add_smul, smul_eq_mul, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)
⊢ HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (m * n * (P.pairing j i * P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (n * n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  HSMul.hSMul (β := N) (P.pairing j i * (m * m * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (P.pairing j i * (m * n * (P.pairing i j * lsq j))) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * n * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)
⊢ HSMul.hSMul (β := N) (m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N) =
    HSMul.hSMul (β := N) (P.pairing j i * (m * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (P.pairing j i * (n * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
h₁ :
  HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : 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) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : 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) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (m * n * (P.pairing j i * P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (n * n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
replace h₁ :
      (m * m * (P.pairing j i * lsq i)) • P.coroot k +
      (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
        (m * (P.pairing j i * lsq i)) • P.coroot i +
        (n * (P.pairing j i * lsq j)) • P.coroot j := by
    rw [h₂, h₃] at h₁
    replace h₁ := congr_arg (fun n ↦ P.pairing j i • n) h₁
    simp only [add_smul, smul_add, ← mul_smul, smul_eq_mul] at h₁
    convert! h₁ using 1
    · module
    · ring_nf