-- Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
lemma isOrthogonal_reflection (hSB : LinearMap.IsSymm B) :
    B.IsOrthogonal (Module.reflection (coroot_apply_self B hx))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z - (2 * (B x) z * (B y) x - 2 * (B x) z * (coroot B hx) y * (B x) x) =
    (B x) x * (B y) z

Tactic:
rw [sub_eq_iff_eq_add, ← hSB x y, RingHom.id_apply, mul_assoc _ _ (B x x), mul_comm _ (B x x),
  apply_self_mul_coroot_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z = (B x) x * (B y) z + (2 * (B x) z * (B x) y - 2 * (B x) z * (2 * (B x) y))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
⊢ B.IsOrthogonal ⇑(reflection ⋯)

Tactic:
intro y z

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) z) = (B y) z

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z = (B x) x * (B y) z + (2 * (B x) z * (B x) y - 2 * (B x) z * (2 * (B x) y))

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (fun x_1 => (B x) x * x_1)
      ((B y) z - (coroot B hx) y * (B x) z - (coroot B hx) z * ((B y) x - (coroot B hx) y * (B x) x)) =
    (fun x_1 => (B x) x * x_1) ((B y) z)

Tactic:
simp only [mul_sub, ← mul_assoc, apply_self_mul_coroot_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z - (2 * (B x) z * (B y) x - 2 * (B x) z * (coroot B hx) y * (B x) x) =
    (B x) x * (B y) z

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B y) z - (coroot B hx) y * (B x) z - (coroot B hx) z * ((B y) x - (coroot B hx) y * (B x) x) = (B y) z

Tactic:
refine hx.1.1 ?_

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (fun x_1 => (B x) x * x_1)
      ((B y) z - (coroot B hx) y * (B x) z - (coroot B hx) z * ((B y) x - (coroot B hx) y * (B x) x)) =
    (fun x_1 => (B x) x * x_1) ((B y) z)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) z) = (B y) z

Tactic:
simp only [LinearEquiv.coe_coe, reflection_apply, LinearMap.map_sub, map_smul, sub_apply,
  smul_apply, smul_eq_mul]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B y) z - (coroot B hx) y * (B x) z - (coroot B hx) z * ((B y) x - (coroot B hx) y * (B x) x) = (B y) z