awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
simp :
  HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
        (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)) -
      HMul.hMul (α := R) ((coroot B hx : (a : M) → R) z : R)
        (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))) =
    (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
⊢ Eq.{u_1 + 1} (α := R)
    ((((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
        ((reflection ⋯ : (a : M) → M) z : M) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
simp only [reflection_apply, map_sub, map_smul, sub_apply,
    smul_apply, smul_eq_mul]

Premises used: map_sub, LinearMap.smul_apply, LinearMap.sub_apply, smul_eq_mul, Module.reflection_apply, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
        (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)) -
      HMul.hMul (α := R) ((coroot B hx : (a : M) → R) z : R)
        (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))) =
    (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z

Tactic:
hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
refine :
  Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
          (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)) -
        HMul.hMul (α := R) ((coroot B hx : (a : M) → R) z : R)
          (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
            (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)))))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z))
⊢ HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
        (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)) -
      HMul.hMul (α := R) ((coroot B hx : (a : M) → R) z : R)
        (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))) =
    (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z

Tactic:
refine hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
simp :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) -
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) -
      (HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) -
        HMul.hMul (β := R)
          (HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
            ((coroot B hx : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
          (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)) -
        HMul.hMul (α := R) ((coroot B hx : (a : M) → R) z : R)
          (HSub.hSub (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
            (HMul.hMul (α := R) (β := R) ((coroot B hx : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)))))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z))

Tactic:
simp only [mul_sub, ← mul_assoc, apply_self_mul_coroot_apply]

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, mul_sub, mul_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) -
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) +
      (HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) -
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) *
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) -
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) -
      (HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) -
        HMul.hMul (β := R)
          (HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
            ((coroot B hx : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
rw [sub_eq_iff_eq_add, ← hSB.eq x y, RingHom.id_apply, mul_assoc _ _ (B x x), mul_comm _ (B x x),
    apply_self_mul_coroot_apply]

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, RingHom.id_apply, mul_assoc, LinearMap.IsSymm.eq, sub_eq_iff_eq_add, mul_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) -
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R) +
      (HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) -
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R) *
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
regular :
  IsRegular.{u_1} (R := R)
    ((((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
        ((reflection ⋯ : (a : M) → M) y : M) :
      R)
dvd_two_mul :
  ∀ (y_1 : M),
    (((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
        ((reflection ⋯ : (a : M) → M) y : M) ∣
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R) y_1 : R)
⊢ B.IsReflective ((reflection ⋯ : (a : M) → M) y)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
regular : IsRegular.{u_1} (R := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ IsRegular.{u_1} (R := R)
    ((((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
        ((reflection ⋯ : (a : M) → M) y : M) :
      R)

Tactic:
rw [isOrthogonal_reflection B hx hSB]

Premises used: LinearMap.IsReflective.isOrthogonal_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular.{u_1} (R := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
hy.1

Premises used: LinearMap.IsReflective.regular
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular.{u_1} (R := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
exact hy.1

Premises used: LinearMap.IsReflective.regular
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z

Tactic:
(LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl

Premises used: LinearEquiv.eq_symm_apply, LinearMap.IsReflective.coroot_apply_self, Iff.mp, Module.reflection, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z

Tactic:
exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl

Premises used: LinearEquiv.eq_symm_apply, LinearMap.IsReflective.coroot_apply_self, Iff.mp, Module.reflection, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z

Tactic:
have hz : Module.reflection (coroot_apply_self B hx)
        (Module.reflection (coroot_apply_self B hx) z) = z := by
      exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z
dvd_two_mul :
  (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y ∣
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ((reflection ⋯ : (a : M) → M) z : M) : R)
⊢ (((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
      ((reflection ⋯ : (a : M) → M) y : M) ∣
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
rw [← hz, isOrthogonal_reflection B hx hSB,
      isOrthogonal_reflection B hx hSB]

Premises used: LinearMap.IsReflective.isOrthogonal_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z
⊢ (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y ∣
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ((reflection ⋯ : (a : M) → M) z : M) : R)

Tactic:
hy.2 _

Premises used: LinearMap.IsReflective.dvd_two_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯ : (a : M) → M) ((reflection ⋯ : (a : M) → M) z : M) = z
⊢ (((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y ∣
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ((reflection ⋯ : (a : M) → M) z : M) : R)

Tactic:
exact hy.2 _

Premises used: LinearMap.IsReflective.dvd_two_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
⊢ ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)

Tactic:
have h1 : ∀ z, IsReflective.coroot B x.2 z = IsReflective.coroot B y.2 z :=
          fun z => congrFun (congrArg DFunLike.coe hxy) z
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
⊢ ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)

Tactic:
have h2x : ∀ z, B x x * IsReflective.coroot B x.2 z =
            B x x * IsReflective.coroot B y.2 z :=
          fun z => congrArg (HMul.hMul ((B x) x)) (h1 z)
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2x :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
⊢ ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)

Tactic:
have h2y : ∀ z, B y y * IsReflective.coroot B x.2 z =
            B y y * IsReflective.coroot B y.2 z :=
          fun z => congrArg (HMul.hMul ((B y) y)) (h1 z)
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2x :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2y :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
⊢ ∀ (z : M),
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)

Tactic:
simp_rw [apply_self_mul_coroot_apply B x.2] at h2x

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, Subtype.property
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2y :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2x :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
⊢ ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
simp_rw [apply_self_mul_coroot_apply B y.2] at h2y

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, Subtype.property
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2x :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
h2y :
  ∀ (z : M),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
h2.1 ?_

Premises used: IsRegular.left