awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
h :
  ∀ (x : M),
    Eq (α := M)
      (((preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) : End R M) :
            (a : M) → M)
          x :
        M)
      ((sα ∘ₗ sβ ∘ₗ sα : (a : M) → M) x : M)
⊢ preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
x : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) i : M) :
      R)
    (2 : R)

Tactic:
simp [hp i]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
x : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) i : M) :
      R)
    (2 : R)

Tactic:
have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
x : M
hpi :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) i : M) :
      R)
    (2 : R)
⊢ Eq (α := M)
    (((preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) : End R M) :
          (a : M) → M)
        x :
      M)
    ((sα ∘ₗ sβ ∘ₗ sα : (a : M) → M) x : M)

Tactic:
simp [α, β, α', β', sα, sβ, sα', ← preReflection_preReflection β (p.flip β') hpi,
      preReflection_apply]

Premises used: Module.preReflection_preReflection, Module.preReflection_apply, LinearMap.flip, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
⊢ preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα

Tactic:
have hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα := by
    ext
    have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
    simp [α, β, α', β', sα, sβ, sα', ← preReflection_preReflection β (p.flip β') hpi,
      preReflection_apply]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
obtain :
  ∀ (l : ι)
    (hl :
      Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : N)
        (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
              (a : N) → N)
            ((coroot : (a : ι) → N) j : N) :
          N)),
    Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
      ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)

Tactic:
obtain ⟨l, hl⟩ := hc i (mem_range_self j)

Premises used: Set.mem_range_self
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
rw : Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N) ((coroot : (a : ι) → N) l : N)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)

Tactic:
rw [← hl]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
⊢ 2 -
        HMul.hMul (α := R) (β := R)
          ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((coroot : (a : ι) → N) i : N) :
            R)
          ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
              ((coroot : (a : ι) → N) j : N) :
            R) +
      HMul.hMul (α := R) (β := R)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) i : N) :
          R)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) j : N) :
          R) =
    2

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
⊢ Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)

Tactic:
have hkl : (p.flip (coroot l)) (root k) = 2 := by
    simp only [hl, preReflection_apply, map_sub, map_smul, hk, LinearMap.flip_apply,
      LinearMap.sub_apply, hp j, LinearMap.smul_apply, smul_eq_mul, hp i, mul_two,
      sub_add_cancel_right, mul_neg, sub_neg_eq_add, sα, α, α', β]
    rw [mul_comm (p (root i) (coroot j))]
    abel
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hr :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
suffices :
  Eq (α := M →ₗ[R] R) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) k) : M →ₗ[R] R)
    ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N) ((coroot : (a : ι) → N) l : N)

Tactic:
suffices p.flip (coroot k) = p.flip (coroot l) from p.flip.toPerfPair.injective this