awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
r : R
a : M
rw :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (r •
        Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
rw₁ :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (r *
        Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
rw₂ :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
    r *
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
rw₃ :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
    r * HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R)
⊢ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (r •
        Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
have rw₄ : 2 * HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
  r * HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R)
Tactic: rw [← (hx.2 (r • a)).choose_spec, smul_eq_mul, mul_left_comm, ← (hx.2 a).choose_spec, map_smul,
      two_mul, smul_eq_mul, two_mul, mul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
⊢ HSMul.hSMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (coroot B hx) =
    HSMul.hSMul (α := ℕ) (β := M →ₗ[R] R) 2 ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R)
have h : ∀ (y : M),
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (coroot B hx) :
          (a : M) → R)
        y :
      R)
    ((HSMul.hSMul (α := ℕ) (β := M →ₗ[R] R) 2 ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
⊢ 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)
have 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
Tactic: simp only [reflection_apply, map_sub, map_smul, sub_apply,
    smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
have 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))
Tactic: refine hx.1.1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
⊢ 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))
have 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)
Tactic: simp only [mul_sub, ← mul_assoc, apply_self_mul_coroot_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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)
          (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)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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
⊢ B.IsReflective ((reflection ⋯ : (a : M) → M) y)
have regular : IsRegular.{u_1} (R := R)
  ((((B : (a : M) → M →ₗ[R] R) ((reflection sorry : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
      ((reflection sorry : (a : M) → M) y : M) :
    R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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)
⊢ B.IsReflective ((reflection ⋯ : (a : M) → M) y)
have dvd_two_mul : ∀ (y_1 : M),
  (((B : (a : M) → M →ₗ[R] R) ((reflection sorry : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
      ((reflection sorry : (a : M) → M) y : M) ∣
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) ((reflection sorry : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R) y_1 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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) ((reflection ⋯ : (a : M) → M) y) : M →ₗ[R] R) : (a : M) → R)
        ((reflection ⋯ : (a : M) → M) y : M) :
      R)
have regular : IsRegular.{u_1} (R := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [isOrthogonal_reflection B hx hSB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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
⊢ (((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)
have hz : (reflection sorry : (a : M) → M) ((reflection sorry : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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) ((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)
have 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 sorry : (a : M) → M) z : M) : R)
Tactic: rw [← hz, isOrthogonal_reflection B hx hSB,
      isOrthogonal_reflection B hx hSB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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 ⋯
⊢ x = y
have h1 : ∀ (z : M),
  Eq.{u_1 + 1} (α := R) ((IsReflective.coroot B sorry : (a : M) → R) z : R) ((IsReflective.coroot B sorry : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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)
⊢ x = y
have 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 sorry : (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 sorry : (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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)
⊢ x = y
have 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 sorry : (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 sorry : (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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)
⊢ x = y
have 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 sorry : (a : M) → R) z : R)
Tactic: simp_rw [apply_self_mul_coroot_apply B x.2] at h2x
Cleared hypotheses: h2x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (hypothesis)
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)
⊢ x = y
have 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 sorry : (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
Cleared hypotheses: h2y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
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)
have 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)))
Tactic: refine h2.1 ?_