awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i : ι
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
              LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
            (a : ↥(P.rootSpan R)) → R)
          (P.rootSpanMem R i) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn R : (a : ↥(P.rootSpan R)) → N) (P.rootSpanMem R i) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw₂ : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) (↑(P.rootSpanMem R i) : M) : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (hypothesis)
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
inst_5 : Fintype ι
i : ι
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have this : HSMul.hSMul (α := R) (β := N)
    ((algebraMap R R : (a : R) → R)
        ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
              (a : ↥(P.rootSpan R)) → R)
            (P.rootSpanMem R i) :
          R) :
      R)
    ((P.coroot : (a : ι) → N) i : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: have : (algebraMap R R) ((P.RootFormIn R) (P.rootSpanMem R i) (P.rootSpanMem R i)) • P.coroot i =
      2 • P.Polarization (P.root i) := by
    rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i : ι
this :
  HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw : HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((P.coroot : (a : ι) → N) i : N) =
  HSMul.hSMul (α := R) (β := N)
    ((algebraMap R R : (a : R) → R)
        ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
              (a : ↥(P.rootSpan R)) → R)
            (P.rootSpanMem R i) :
          R) :
      R)
    ((P.coroot : (a : ι) → N) i : N)
Tactic: rw [← this, algebraMap_rootFormIn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i : ι
this :
  HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw₁ : HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((P.coroot : (a : ι) → N) i : N) =
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑(P.rootSpanMem R i) : M) : M →ₗ[R] R) : (a : M) → R)
        (↑(P.rootSpanMem R i) : M) :
      R)
    ((P.coroot : (a : ι) → N) i : N)
Tactic: rw [← this, algebraMap_rootFormIn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i : ι
⊢ (HSMul.hSMul (α := ℕ) 4 (P.CoPolarization ∘ₗ P.Polarization) : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
have rw : HSMul.hSMul (α := ℕ) (β := M) 4
    ((P.CoPolarization ∘ₗ P.Polarization : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) =
  HSMul.hSMul (β := M)
    (HMul.hMul (α := R) (β := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R))
    ((P.root : (a : ι) → M) i : M)
Tactic: rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
    ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i : ι
rw :
  HSMul.hSMul (α := ℕ) (β := M) 4
      ((P.CoPolarization ∘ₗ P.Polarization : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
⊢ (HSMul.hSMul (α := ℕ) 4 (P.CoPolarization ∘ₗ P.Polarization) : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
have rw₁ : HSMul.hSMul (α := ℕ) (β := M) 4
    ((P.CoPolarization : (a : N) → M) ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) : M) =
  HSMul.hSMul (β := M)
    (HMul.hMul (α := R) (β := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R))
    ((P.root : (a : ι) → M) i : M)
Tactic: rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
    ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i j : ι
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
have rw : HSMul.hSMul (α := ℕ) (β := R) 4
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R) =
  HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
      R)
Tactic: rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i j : ι
rw :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
have rw₁ : HSMul.hSMul (α := ℕ) (β := R) 4
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R) =
  HSMul.hSMul (α := ℕ) 2
    (HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R))
Tactic: rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i j : ι
rw :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := ℕ) (β := R) 2
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
          R))
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
have rw₂ : HSMul.hSMul (α := ℕ) (β := R) 4
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R) =
  HSMul.hSMul (β := R) (HSMul.hSMul (α := ℕ) (β := ℕ) 2 2)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R)
Tactic: rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i j : ι
rw :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := ℕ) (β := R) 2
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
          R))
rw₂ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (β := R) (HSMul.hSMul (α := ℕ) (β := ℕ) 2 2)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
have rw₃ : HSMul.hSMul (α := ℕ) (β := R) 4
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R) =
  HSMul.hSMul (β := R) (HMul.hMul (α := ℕ) 2 2)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
      R)
Tactic: rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (hypothesis)
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
inst_5 : Fintype ι
i j : ι
⊢ HSMul.hSMul (α := ℕ) 4
      (HPow.hPow (α := R) (β := ℕ)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        2) =
    P.coxeterWeight i j •
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
have hij : HSMul.hSMul (α := ℕ) (β := R) 4
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R) =
  HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
      R)
Tactic: have hij : 4 • (P.RootForm (P.root i)) (P.root j) =
      2 • P.toLinearMap (P.root j) (2 • P.Polarization (P.root i)) := by
    rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
inst_5 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw : HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R) =
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
    (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
Tactic: rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]