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
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)
⊢ (fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
            ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ :
          { x : M // Membership.mem (γ := Set M) {x : M | B.IsReflective x} x }))
      ((fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
              ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ :
            { x : M // Membership.mem (γ := Set M) {x : M | B.IsReflective x} x }))
        y) =
    y

Tactic:
simp [involutive_reflection (coroot_apply_self B x.2) y]

Premises used: Module.involutive_reflection, LinearMap.IsReflective.coroot_apply_self, Subtype.val, 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)
⊢ HSub.hSub (α := M)
      ((Embedding.subtype fun (x : M) ↦ B.IsReflective x : (a : (↑{x : M | B.IsReflective x} : Type u_2)) → M) y : M)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((((Dual.eval R M : (a : M) → Dual R M →ₗ[R] R)
                  ((Embedding.subtype fun (x : M) ↦ B.IsReflective x :
                      (a : (↑{x : M | B.IsReflective x} : Type u_2)) → M)
                    y) :
                Dual R M →ₗ[R] R) :
              (a : Dual R M) → R)
            (({ toFun := fun (x : (↑{x : M | B.IsReflective x} : Type u_2)) ↦ IsReflective.coroot B ⋯, inj' := ⋯ :
                    (↑{x : M | B.IsReflective x} : Type u_2) ↪ Dual R M } :
                  (a : (↑{x : M | B.IsReflective x} : Type u_2)) → Dual R M)
                x :
              Dual R M) :
          R)
        ((Embedding.subtype fun (x : M) ↦ B.IsReflective x : (a : (↑{x : M | B.IsReflective x} : Type u_2)) → M) x :
          M)) =
    (Embedding.subtype fun (x : M) ↦ B.IsReflective x : (a : (↑{x : M | B.IsReflective x} : Type u_2)) → M)
      (({
              toFun := fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
                Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
                  ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯,
              invFun := fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
                Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
                  ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯,
              left_inv := ⋯, right_inv := ⋯ :
              (↑{x : M | B.IsReflective x} : Type u_2) ≃ (↑{x : M | B.IsReflective x} : Type u_2) } :
            (a : (↑{x : M | B.IsReflective x} : Type u_2)) → (↑{x : M | B.IsReflective x} : Type u_2))
          y :
        (↑{x : M | B.IsReflective x} : Type u_2))

Tactic:
simp [Module.reflection_apply]

Premises used: Module.reflection_apply
-- 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)
simp :
  IsReflective.coroot B ⋯ -
      HSMul.hSMul (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B ⋯) =
    IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯
⊢ HSub.hSub (α := Dual R M)
      (({ toFun := fun (x : (↑{x : M | B.IsReflective x} : Type u_2)) ↦ IsReflective.coroot B ⋯, inj' := ⋯ :
              (↑{x : M | B.IsReflective x} : Type u_2) ↪ Dual R M } :
            (a : (↑{x : M | B.IsReflective x} : Type u_2)) → Dual R M)
          y :
        Dual R M)
      (HSMul.hSMul (α := R) (β := Dual R M)
        ((((Dual.eval R M : (a : M) → Dual R M →ₗ[R] R)
                  ((Embedding.subtype fun (x : M) ↦ B.IsReflective x :
                      (a : (↑{x : M | B.IsReflective x} : Type u_2)) → M)
                    x) :
                Dual R M →ₗ[R] R) :
              (a : Dual R M) → R)
            (({ toFun := fun (x : (↑{x : M | B.IsReflective x} : Type u_2)) ↦ IsReflective.coroot B ⋯, inj' := ⋯ :
                    (↑{x : M | B.IsReflective x} : Type u_2) ↪ Dual R M } :
                  (a : (↑{x : M | B.IsReflective x} : Type u_2)) → Dual R M)
                y :
              Dual R M) :
          R)
        (({ toFun := fun (x : (↑{x : M | B.IsReflective x} : Type u_2)) ↦ IsReflective.coroot B ⋯, inj' := ⋯ :
                (↑{x : M | B.IsReflective x} : Type u_2) ↪ Dual R M } :
              (a : (↑{x : M | B.IsReflective x} : Type u_2)) → Dual R M)
            x :
          Dual R M)) =
    ({ toFun := fun (x : (↑{x : M | B.IsReflective x} : Type u_2)) ↦ IsReflective.coroot B ⋯, inj' := ⋯ :
          (↑{x : M | B.IsReflective x} : Type u_2) ↪ Dual R M } :
        (a : (↑{x : M | B.IsReflective x} : Type u_2)) → Dual R M)
      (({
            toFun := fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
                ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯,
            invFun := fun (y : (↑{x : M | B.IsReflective x} : Type u_2)) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | B.IsReflective x} x)
                ((Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯,
            left_inv := ⋯, right_inv := ⋯ :
            (↑{x : M | B.IsReflective x} : Type u_2) ≃ (↑{x : M | B.IsReflective x} : Type u_2) } :
          (a : (↑{x : M | B.IsReflective x} : Type u_2)) → (↑{x : M | B.IsReflective x} : Type u_2))
        y)

Tactic:
simp only [coe_setOf, mem_setOf_eq, Embedding.coeFn_mk, Embedding.subtype_apply,
      Dual.eval_apply, Equiv.coe_fn_mk]

Premises used: Module.Dual.eval_apply, Set.mem_setOf_eq, Function.Embedding.subtype_apply, Equiv.coe_fn_mk, Function.Embedding.coeFn_mk, Set.coe_setOf
-- 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)
h :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R)
      ((IsReflective.coroot B ⋯ -
              HSMul.hSMul (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B ⋯) :
            (a : M) → R)
          z :
        R)
      ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z : R)
⊢ IsReflective.coroot B ⋯ -
      HSMul.hSMul (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B ⋯) =
    IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯

Tactic:
ext 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)
z : M
h :
  HSub.hSub (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    (IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z
⊢ Eq.{u_1 + 1} (α := R)
    ((IsReflective.coroot B ⋯ -
            HSMul.hSMul (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B ⋯) :
          (a : M) → R)
        z :
      R)
    ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z : R)

Tactic:
simp only [sub_apply, smul_apply, smul_eq_mul]

Premises used: LinearMap.smul_apply, LinearMap.sub_apply, smul_eq_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)
z : M
⊢ HSub.hSub (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    (IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z

Tactic:
y.2.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left, 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)
z : M
h :
  Eq.{u_1 + 1} (α := R)
    ((fun (x : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) x)
      (HSub.hSub (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
        (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R)
          ((IsReflective.coroot B ⋯ : (a : M) → R) z : R))))
    ((fun (x : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) x)
      ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z))
⊢ HSub.hSub (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
      (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    (IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z

Tactic:
refine y.2.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left, 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)
z : M
h :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R) -
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : 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) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
      ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) x)
      (HSub.hSub (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
        (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑x : M) : R)
          ((IsReflective.coroot B ⋯ : (a : M) → R) z : R))))
    ((fun (x : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) x)
      ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z))

Tactic:
simp only [mem_setOf_eq, mul_sub, apply_self_mul_coroot_apply B y.2, ← mul_assoc]

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, mul_sub, mul_assoc, Set.mem_setOf_eq, 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)
z : M
h :
  HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
        R)
⊢ HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R) -
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : 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) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
      ((IsReflective.coroot B (x := (Module.reflection ⋯ : (a : M) → M) (↑y : M)) ⋯ : (a : M) → R) z : R)

Tactic:
rw [← isOrthogonal_reflection B x.2 hSB y y, apply_self_mul_coroot_apply, ← hSB.eq z,
      ← hSB.eq z, RingHom.id_apply, RingHom.id_apply, Module.reflection_apply, map_sub,
      mul_sub, sub_eq_sub_iff_comm, sub_left_inj]

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, map_sub, RingHom.id_apply, mul_sub, LinearMap.IsReflective.isOrthogonal_reflection, sub_left_inj, LinearMap.IsSymm.eq, Module.reflection_apply, Subtype.val, sub_eq_sub_iff_comm, 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)
z : M
⊢ HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
        R)

Tactic:
x.2.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left, 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)
z : M
h :
  Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)))
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
          R)))
⊢ HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
        R)

Tactic:
refine x.2.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left, 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)
z : M
h :
  HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (2 *
        HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R)
          ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)))
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
          R)))

Tactic:
simp only [mem_setOf_eq, map_smul, smul_eq_mul]

Premises used: Set.mem_setOf_eq, smul_eq_mul, 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
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)
z : M
h :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) *
      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)
      (2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R))
      ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (2 *
        HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R)
          ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))

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

Premises used: LinearMap.IsReflective.apply_self_mul_coroot_apply, RingHom.id_apply, mul_assoc, mul_left_comm, LinearMap.IsSymm.eq, Subtype.val, DFunLike.coe, 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)
z : M
⊢ HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) *
      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)
      (2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R))
      ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
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
rw :
  (∀ (i j : ι)
      (h :
        ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
            (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)) ↔
    ∀ (i j : ι),
      i ≠ j →
        ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
              (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M) →
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ P.IsReduced ↔
    ∀ (i j : ι),
      i ≠ j →
        ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
              (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M) →
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
rw [isReduced_iff]

Premises used: RootPairing.isReduced_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
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 : ι)
      (h :
        ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
            (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)) ↔
    ∀ (i j : ι),
      i ≠ j →
        ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
              (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M) →
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩

Premises used: Iff.intro