awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
refine :
  MapsTo (α := N) (β := N)
    (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
⊢ HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N) = (P.coroot : (a : ι) → N) i

Tactic:
refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i)
    (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_
    (P.mapsTo_coreflection_coroot i) (mem_range_self i)

Premises used: Set.mem_range_self, Module.eq_of_mapsTo_reflection_of_mem, Set.finite_range, RootPairing.coroot, DFunLike.coe, RootPairing.mapsTo_coreflection_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ MapsTo (α := N) (β := N) (⇑(P.coreflection j) : (a : N) → N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))

Tactic:
P.mapsTo_coreflection_coroot j

Premises used: RootPairing.mapsTo_coreflection_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
h₁ :
  Eq (α := N → N) (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (⇑(P.coreflection j) : (a : N) → N)
⊢ MapsTo (α := N) (β := N)
    (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))

Tactic:
convert! P.mapsTo_coreflection_coroot j

Premises used: RootPairing.mapsTo_coreflection_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
h₁ :
  ∀ (x : N),
    Eq (α := N)
      ((preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i) : (a : N) → N) x : N)
      ((P.coreflection j : (a : N) → N) x : N)
⊢ Eq (α := N → N) (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (⇑(P.coreflection j) : (a : N) → N)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
x : N
h₁ : ∀ (x : N), Eq.{u_2 + 1} (α := R) ((P.root' j : (a : N) → R) x : R) ((t • P.root' i : (a : N) → R) x : R)
⊢ P.root' j = t • P.root' i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
x x_1 : N
⊢ Eq.{u_2 + 1} (α := R) ((P.root' j : (a : N) → R) x_1 : R) ((t • P.root' i : (a : N) → R) x_1 : R)

Tactic:
simp [h, root']

Premises used: RootPairing.root'
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
x : N
⊢ P.root' j = t • P.root' i

Tactic:
replace h : P.root' j = t • P.root' i := by ext; simp [h, root']
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
hij : t * P.pairing i j = 2
x : N
h : P.root' j = t • P.root' i
⊢ Eq (α := N)
    ((preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i) : (a : N) → N) x : N)
    ((P.coreflection j : (a : N) → N) x : N)

Tactic:
simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul]

Premises used: Module.preReflection_apply, RootPairing.coreflection_apply, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i j : ι
t : R
⊢ (P.coroot : (a : ι) → N) i = HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N) ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)

Tactic:
⟨fun h ↦ (P.flip.smul_coroot_eq_of_root_eq_smul j i t h).symm,
    fun h ↦ (P.smul_coroot_eq_of_root_eq_smul i j t h).symm⟩

Premises used: Iff.intro, Eq.symm, RootPairing.smul_coroot_eq_of_root_eq_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
r : M ≃ₗ[R] M
α : M
hr : r ∈ range P.reflection
hα : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) α
obtain :
  ∀ (i : ι), Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (P.reflection i • α)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (r • α)

Tactic:
obtain ⟨i, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
α : M
hα : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) α
i : ι
obtain :
  ∀ (j : ι),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSMul.hSMul (β := M) (P.reflection i) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (P.reflection i • α)

Tactic:
obtain ⟨j, rfl⟩ := hα

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) (P.reflection i) ((P.root : (a : ι) → M) j : M))

Tactic:
⟨P.reflectionPerm i j, P.root_reflectionPerm i j⟩

Premises used: Set.Mem, setOf, Exists.intro, RootPairing.reflectionPerm, Set.range, DFunLike.coe, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) (P.reflection i) ((P.root : (a : ι) → M) j : M))

Tactic:
exact ⟨P.reflectionPerm i j, P.root_reflectionPerm i j⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
r : N ≃ₗ[R] N
α : N
hr : r ∈ range P.coreflection
hα : Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) α
obtain :
  ∀ (i : ι),
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (P.coreflection i • α)
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (r • α)

Tactic:
obtain ⟨i, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
α : N
hα : Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) α
i : ι
obtain :
  ∀ (j : ι),
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
      (HSMul.hSMul (β := N) (P.coreflection i) ((P.coroot : (a : ι) → N) j : N))
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (P.coreflection i • α)

Tactic:
obtain ⟨j, rfl⟩ := hα

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul (β := N) (P.coreflection i) ((P.coroot : (a : ι) → N) j : N))

Tactic:
⟨P.reflectionPerm i j, P.coroot_reflectionPerm i j⟩

Premises used: Set.Mem, setOf, Exists.intro, RootPairing.reflectionPerm, Set.range, DFunLike.coe, RootPairing.coroot_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul (β := N) (P.coreflection i) ((P.coroot : (a : ι) → N) j : N))

Tactic:
exact ⟨P.reflectionPerm i j, P.coroot_reflectionPerm i j⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
    ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)

Tactic:
simp only [← root_reflectionPerm, hij]

Premises used: RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
    ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)

Tactic:
have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by
    simp only [← root_reflectionPerm, hij]
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
h :
  Eq (α := M) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
    ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
⊢ HSMul.hSMul (β := M) (P.pairing k i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing k j) ((P.root : (a : ι) → M) j : M)

Tactic:
simpa only [reflection_apply_root, sub_right_inj] using h

Premises used: sub_right_inj, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ Eq (α := N) ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
    ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)

Tactic:
simp only [← coroot_reflectionPerm, hij]

Premises used: RootPairing.coroot_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ Eq (α := N) ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
    ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)

Tactic:
have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
    simp only [← coroot_reflectionPerm, hij]
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
h :
  Eq (α := N) ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
    ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
⊢ HSMul.hSMul (β := N) (P.pairing i k) ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (β := N) (P.pairing j k) ((P.coroot : (a : ι) → N) j : N)

Tactic:
simpa only [coreflection_apply_coroot, sub_right_inj] using h

Premises used: sub_right_inj, RootPairing.coreflection_apply_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
h :
  ∀ (x : M),
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) x =
      HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M) x
⊢ HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
this :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))
⊢ HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) x =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M) x

Tactic:
simpa [reflection_apply, smul_sub]

Premises used: smul_sub, RootPairing.reflection_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))
⊢ HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) x =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M) x

Tactic:
suffices
      2 • P.toLinearMap x (P.coroot i) • P.root i = 2 • P.toLinearMap x (P.coroot j) • P.root j by
    simpa [reflection_apply, smul_sub]
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (↑2 : R) ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
h₂ h₃ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))

Tactic:
rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Nat.cast_smul_eq_nsmul, SMulCommClass.smul_comm