-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
f g : Dual R M
hf : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
z : M
m : ℕ
k : ℤ := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2
e : ℤ
he : e = 0 ∨ e = 1
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
        (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
            (S R (k - 1)) -
        Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ)
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R k))
            2 +
          HPow.hPow (β := ℕ)
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (k + 1)))
            2 -
        (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R k) *
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
            (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 3 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
            (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R k) +
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
a :
  -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (HSub.hSub (α := ℤ) 0 2 / 2 + k)) *
                (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (HSub.hSub (α := ℤ) 0 1 / 2 + k)) +
                  Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (HSub.hSub (α := ℤ) 0 3 / 2 + k))) *
              (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                    ((g : (a : M) → R) z : R) *
                  (1 - HMul.hMul (α := R) 2 1) -
                HMul.hMul (α := R) ((f : (a : M) → R) z : R)
                  (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) +
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) 0 1 / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (0 / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (HSub.hSub (α := ℤ) 0 2 / 2 + k))) *
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
                  ((f : (a : M) → R) z : R) *
                -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) -
              HMul.hMul (α := R) ((g : (a : M) → R) z : R) (1 - HMul.hMul (α := R) 2 1)) +
        (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) 0 1 + k))) *
            ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (0 + k - 1)) -
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (0 + k))) +
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R)) -
      (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((HAdd.hAdd (α := ℤ) 0 1 - 2) / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((HAdd.hAdd (α := ℤ) 0 1 - 1) / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((HAdd.hAdd (α := ℤ) 0 1 - 3) / 2 + k))) *
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) *
              1) +
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((HAdd.hAdd (α := ℤ) 0 1 - 1) / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (HAdd.hAdd (α := ℤ) 0 1 / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((HAdd.hAdd (α := ℤ) 0 1 - 2) / 2 + k))) *
            -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
        (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) 0 1 + k))) *
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (0 + k - 2)) +
          HMul.hMul (α := R) ((g : (a : M) → R) z : R)
            (HPow.hPow (β := ℕ)
                  (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1)))
                  2 +
                HPow.hPow (β := ℕ)
                  (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1 + 1)))
                  2 -
              (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
                  Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1)) *
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (k - 1 + 1))))) =
    0
⊢ -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e - 2) / 2 + k)) *
                (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R ((e - 1) / 2 + k)) +
                  Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R ((e - 3) / 2 + k))) *
              (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                    ((g : (a : M) → R) z : R) *
                  (1 - HMul.hMul (α := R) 2 1) -
                HMul.hMul (α := R) ((f : (a : M) → R) z : R)
                  (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) +
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((e - 1) / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (e / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e - 2) / 2 + k))) *
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
                  ((f : (a : M) → R) z : R) *
                -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) -
              HMul.hMul (α := R) ((g : (a : M) → R) z : R) (1 - HMul.hMul (α := R) 2 1)) +
        (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (e - 1 + k))) *
            ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (e + k - 1)) -
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (e + k))) +
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R)) -
      (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((e + 1 - 2) / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e + 1 - 1) / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e + 1 - 3) / 2 + k))) *
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) *
              1) +
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((e + 1 - 1) / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e + 1) / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R ((e + 1 - 2) / 2 + k))) *
            -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
        (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (e - 1 + k))) *
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (e + k - 2)) +
          HMul.hMul (α := R) ((g : (a : M) → R) z : R)
            (HPow.hPow (β := ℕ)
                  (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1)))
                  2 +
                HPow.hPow (β := ℕ)
                  (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1 + 1)))
                  2 -
              (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
                  Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                    (S R (k - 1)) *
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (k - 1 + 1))))) =
    0
have a₁ : -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) 1 2 / 2 + k)) *
              (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (HSub.hSub (α := ℤ) 1 1 / 2 + k)) +
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (HSub.hSub (α := ℤ) 1 3 / 2 + k))) *
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                  ((g : (a : M) → R) z : R) *
                (1 - HMul.hMul (α := R) 2 1) -
              HMul.hMul (α := R) ((f : (a : M) → R) z : R)
                (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) +
        Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (HSub.hSub (α := ℤ) 1 1 / 2 + k)) *
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (1 / 2 + k)) +
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HSub.hSub (α := ℤ) 1 2 / 2 + k))) *
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
                ((f : (a : M) → R) z : R) *
              -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) -
            HMul.hMul (α := R) ((g : (a : M) → R) z : R) (1 - HMul.hMul (α := R) 2 1)) +
      (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (HSub.hSub (α := ℤ) 1 1 + k))) *
          ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (1 + k - 1)) -
            Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (1 + k))) +
        HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R)) -
    (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R ((HAdd.hAdd (α := ℤ) 1 1 - 2) / 2 + k)) *
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((HAdd.hAdd (α := ℤ) 1 1 - 1) / 2 + k)) +
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((HAdd.hAdd (α := ℤ) 1 1 - 3) / 2 + k))) *
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
              ((g : (a : M) → R) z : R) *
            1) +
        Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R ((HAdd.hAdd (α := ℤ) 1 1 - 1) / 2 + k)) *
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (HAdd.hAdd (α := ℤ) 1 1 / 2 + k)) +
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R ((HAdd.hAdd (α := ℤ) 1 1 - 2) / 2 + k))) *
          -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) z : R) (1 : R) +
      (HMul.hMul (α := R) ((g : (a : M) → R) z : R)
            (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
              (S R (HSub.hSub (α := ℤ) 1 1 + k))) *
          Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
            (S R (1 + k - 2)) +
        HMul.hMul (α := R) ((g : (a : M) → R) z : R)
          (HPow.hPow (β := ℕ)
                (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (k - 1)))
                2 +
              HPow.hPow (β := ℕ)
                (Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (k - 1 + 1)))
                2 -
            (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
                Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                  (S R (k - 1)) *
              Polynomial.eval (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2)
                (S R (k - 1 + 1))))) =
  0
Tactic: obtain rfl | rfl : e = 0 ∨ e = 1 := he
Cleared hypotheses: e, he