Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case a.inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((0 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (0 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (0 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

pp: case a.inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((1 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (1 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (1 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

Tactic:
<;>

Goal state after:
case a.inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((0 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (0 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (0 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

case a.inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((1 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (1 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (1 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0