-- Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
lemma reflective_reflection (hSB : LinearMap.IsSymm B) {y : M}
    (hx : IsReflective B x) (hy : IsReflective B y) :
    IsReflective B (Module.reflection (coroot_apply_self B hx) y)

Proof state:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) z

Tactic:
rw [← hz, isOrthogonal_reflection B hx hSB,
  isOrthogonal_reflection B hx hSB]

Result:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B y) y ∣ 2 * (B y) ((reflection ⋯) 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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ B.IsReflective ((reflection ⋯) y)

Tactic:
constructor

Result:
case regular
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular ((B ((reflection ⋯) y)) ((reflection ⋯) y))

case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ ∀ (y_1 : M), (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) y_1

Proof state:
case regular
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular ((B y) y)

Tactic:
exact hy.1

Result:
no goals

Proof state:
case regular
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular ((B ((reflection ⋯) y)) ((reflection ⋯) y))

Tactic:
rw [isOrthogonal_reflection B hx hSB]

Result:
case regular
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ IsRegular ((B y) y)

Proof state:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B y) y ∣ 2 * (B y) ((reflection ⋯) z)

Tactic:
exact hy.2 _

Result:
no goals

Proof state:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) 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

Result:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
hz : (reflection ⋯) ((reflection ⋯) z) = z
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) 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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (reflection ⋯) ((reflection ⋯) z) = z

Tactic:
exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl

Result:
no goals

Proof state:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ ∀ (y_1 : M), (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) y_1

Tactic:
intro z

Result:
case dvd_two_mul
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
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
z : M
⊢ (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) z