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
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
have 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)
Tactic: refine hNB.1 _ (fun z => ?_)
-- 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)
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) - (↑y : M)) : M →ₗ[R] R) : (a : M) → R) z : R) (0 : R)
have 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)
Tactic: rw [map_sub, LinearMap.sub_apply, sub_eq_zero]
-- 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)
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)
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) z))
  ((fun (x : R) ↦ 2 * x) ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) z))
Tactic: refine h2.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
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
⊢ 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)
have 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 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: rw [h2x z, ← h2y z, hxy, h2xy]
-- 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)
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)
⊢ 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)
have 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 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: rw [h2x z, ← h2y z, hxy, h2xy]
-- 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)
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)
⊢ 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)
have 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 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: rw [h2x z, ← h2y z, hxy, h2xy]
-- 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)
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)
⊢ 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)
have 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 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: rw [h2x z, ← h2y z, hxy, h2xy]
-- 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)
⊢ 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)
have simp : IsReflective.coroot B sorry -
    HSMul.hSMul (α := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B sorry) =
  IsReflective.coroot B (x := (Module.reflection sorry : (a : M) → M) (↑y : M)) sorry
Tactic: simp only [coe_setOf, mem_setOf_eq, Embedding.coeFn_mk, Embedding.subtype_apply,
      Dual.eval_apply, Equiv.coe_fn_mk]
-- 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)
⊢ 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)) ⋯
have h : ∀ (z : M),
  Eq.{u_1 + 1} (α := R)
    ((IsReflective.coroot B sorry -
            HSMul.hSMul (α := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑x : M) : R) (IsReflective.coroot B sorry) :
          (a : M) → R)
        z :
      R)
    ((IsReflective.coroot B (x := (Module.reflection sorry : (a : M) → M) (↑y : M)) sorry : (a : M) → R) z : R)
Tactic: ext z
-- 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)
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)
have h : HSub.hSub (α := R) ((IsReflective.coroot B sorry : (a : M) → R) z : R)
    (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑x : M) : R)
      ((IsReflective.coroot B sorry : (a : M) → R) z : R)) =
  (IsReflective.coroot B (x := (Module.reflection sorry : (a : M) → M) (↑y : M)) sorry : (a : M) → R) z
Tactic: simp only [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
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
have 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 sorry : (a : M) → R) z : R)
      (HMul.hMul (α := R) (β := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑x : M) : R)
        ((IsReflective.coroot B sorry : (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 sorry : (a : M) → M) (↑y : M)) sorry : (a : M) → R) z))
Tactic: refine y.2.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
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
⊢ 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))
have 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 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 (x := (Module.reflection sorry : (a : M) → M) (↑y : M)) sorry : (a : M) → R) z : R)
Tactic: simp only [mem_setOf_eq, mul_sub, apply_self_mul_coroot_apply B y.2, ← mul_assoc]
-- 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)
z : M
⊢ 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)
have 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 sorry : (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 sorry : (a : M) → R) (↑y : M) : R) (↑x : M)) :
      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]