awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
hM : Eq (α := Submodule L M) (span L (↑(Q.rootSpan K) : Set M)) ⊤
⊢ finrank.{u_7, u_4} K ↥(Q.rootSpan K) = finrank L M
have hN : Eq (α := Submodule L N) (span L (↑(Q.corootSpan K) : Set N)) ⊤
Tactic: rw [LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
hM : Eq (α := Submodule L M) (span L (↑(Q.rootSpan K) : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑(Q.corootSpan K) : Set N)) ⊤
⊢ finrank.{u_7, u_4} K ↥(Q.rootSpan K) = finrank L M
have hp : ∀ (x : M),
  Membership.mem (γ := Submodule K M) (Q.rootSpan K) x →
    ∀ (y : N),
      Membership.mem (γ := Submodule K N) (Q.corootSpan K) y →
        Membership.mem.{u_8, u_8} (α := L) (γ := Subring L) (RingHom.range.{u_7, u_8} (R := K) (algebraMap K L))
          ((((Q.toLinearMap : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
Tactic: rw [LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (hypothesis)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
_i_1 : Module ℚ M := compHom M (algebraMap ℚ L)
_i : Module ℚ N := compHom N (algebraMap ℚ L)
⊢ finrank.{0, u_4} ℤ ↥(Q.rootSpan ℤ) = finrank L M
have _i₁ : IsAddTorsionFree M
Tactic: have _i : IsAddTorsionFree M := .of_isTorsionFree L M
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
_i_1 : Module ℚ M := compHom M (algebraMap ℚ L)
_i_2 : Module ℚ N := compHom N (algebraMap ℚ L)
_i : IsAddTorsionFree M
⊢ finrank.{0, u_4} ℤ ↥(Q.rootSpan ℤ) = finrank L M
have rw : finrank.{0, u_4} ℚ ↥(span ℚ (range.{u_4, u_1 + 1} (ι := ι) (⇑Q.root : (a : ι) → M))) = finrank L M
Tactic: rw [← Submodule.finrank_span_eq_finrank_span ℤ ℚ, ← Q.finrank_rootSpanIn ℚ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
_i_1 : Module ℚ M := compHom M (algebraMap ℚ L)
_i_2 : Module ℚ N := compHom N (algebraMap ℚ L)
_i : IsAddTorsionFree M
rw : finrank.{0, u_4} ℚ ↥(span ℚ (range.{u_4, u_1 + 1} (ι := ι) (⇑Q.root : (a : ι) → M))) = finrank L M
⊢ finrank.{0, u_4} ℤ ↥(Q.rootSpan ℤ) = finrank L M
have rw₁ : finrank.{0, u_4} ℚ ↥(span ℚ (range.{u_4, u_1 + 1} (ι := ι) (⇑Q.root : (a : ι) → M))) =
  finrank.{0, u_4} ℚ ↥(Q.rootSpan ℚ)
Tactic: rw [← Submodule.finrank_span_eq_finrank_span ℤ ℚ, ← Q.finrank_rootSpanIn ℚ]
-- 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
a b : M
⊢ 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 + b) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      ⋯ =
    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)
        ⋯ +
      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) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯
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)
    (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 + b) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      sorry))
  ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
    (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)
        sorry +
      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) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        sorry))
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
a b : M
⊢ 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 + b) : 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)
      (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)
          ⋯ +
        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) b : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
have rw : HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : 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)
        sorry +
      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) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        sorry)
Tactic: rw [← (hx.2 (a + b)).choose_spec, mul_add, ← (hx.2 a).choose_spec, ← (hx.2 b).choose_spec,
      map_add, 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
a b : M
rw :
  HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : 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)
          ⋯ +
        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) b : 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)
      (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 + b) : 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)
      (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)
          ⋯ +
        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) b : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
have rw₁ : HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : 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)
        sorry) +
    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) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        sorry)
Tactic: rw [← (hx.2 (a + b)).choose_spec, mul_add, ← (hx.2 a).choose_spec, ← (hx.2 b).choose_spec,
      map_add, 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
r : R
a : M
⊢ 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)
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) 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 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)
    (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)
      sorry))
  ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) 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)
        sorry)))
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
r : R
a : 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)
      (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)
        ⋯))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) 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 simp : 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)
      sorry) =
  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)
        sorry)
Tactic: simp only [RingHom.id_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
r : R
a : M
⊢ 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 : 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)
        sorry)
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
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)
          ⋯)
⊢ 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₁ : 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)
        sorry)
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
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)
          ⋯)
⊢ 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₂ : 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)
        sorry)
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
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)
          ⋯)
⊢ 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₃ : 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)
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]