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)
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)
refine :
  Eq.{u_1 + 1} (α := R)
    ((fun (x : R) ↦ 2 * x) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M)))
    ((fun (x : R) ↦ 2 * x) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M)))
⊢ 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:
refine h2.1 ?_

Premises used: 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
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)
⊢ 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) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R)

Tactic:
specialize h2x y

Premises used: Subtype.val
-- 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) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)
h2x :
  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) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      ((IsReflective.coroot B ⋯ : (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) (↑y : M) : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) (2 : R)

Tactic:
rw [coroot_apply_self] at h2x

Premises used: LinearMap.IsReflective.coroot_apply_self
-- 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) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)
h2x :
  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) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) (2 : 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) (↑x : M) : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)

Tactic:
specialize h2y x

Premises used: Subtype.val
-- 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 :
  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) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) (2 : R)
h2y :
  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) (↑x : M) : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) (2 : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)

Tactic:
rw [coroot_apply_self] at h2y

Premises used: LinearMap.IsReflective.coroot_apply_self
-- 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 :
  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) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) (2 : R)
h2y :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) (2 : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) (2 : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
rw₁ :
  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) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
rw₂ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
rw₃ :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : 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) (↑y : M) : R)
rw₄ :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) (2 : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
rw₅ rw₆ :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : 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) (↑x : M) : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
rw [mul_comm, ← h2x, ← hSB.eq, RingHom.id_apply, ← h2y, mul_comm]

Premises used: RingHom.id_apply, LinearMap.IsSymm.eq, mul_comm
-- 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:
have h2xy : B x x = B y y := by
          refine h2.1 ?_
          dsimp only
          specialize h2x y
          rw [coroot_apply_self] at h2x
          specialize h2y x
          rw [coroot_apply_self] at h2y
          rw [mul_comm, ← h2x, ← hSB.eq, RingHom.id_apply, ← h2y, mul_comm]
-- 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)
h2xy :
  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)
rw : (↑x : M) - (↑y : M) = 0
⊢ x = y

Tactic:
rw [Subtype.ext_iff, ← sub_eq_zero]

Premises used: sub_eq_zero, Subtype.ext_iff
-- 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)
h2xy :
  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)
⊢ (↑x : M) - (↑y : M) = 0

Tactic:
hNB.1 _ (fun z => ?_)

Premises used: And.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
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)
h2xy :
  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)
refine :
  ∀ (z : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ((↑x : M) - (↑y : M)) : M →ₗ[R] R) : (a : M) → R) z : R) (0 : R)
⊢ (↑x : M) - (↑y : M) = 0

Tactic:
refine hNB.1 _ (fun z => ?_)

Premises used: And.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
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)
h2xy :
  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)
z : M
rw :
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : 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) - (↑y : M)) : M →ₗ[R] R) : (a : M) → R) z : R) (0 : R)

Tactic:
rw [map_sub, LinearMap.sub_apply, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, LinearMap.sub_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)
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)
h2xy :
  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)
z : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
h2.1 ?_

Premises used: 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
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)
h2xy :
  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)
z : M
refine :
  Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ 2 * x) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z))
    ((fun (x : R) ↦ 2 * x) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z))
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
refine h2.1 ?_

Premises used: 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
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)
h2xy :
  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)
z : M
rw :
  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) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)
rw₁ :
  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) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
rw₂ :
  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) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)
rw₃ rw₄ :
  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)
⊢ 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) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
rw [h2x z, ← h2y z, hxy, h2xy]