awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Reflection
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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
h :
  ∀ (z : M),
    Eq (α := M) (((↑((reflection hf * reflection hg) ^ m) : M →ₗ[R] M) : (a : M) → M) z : M)
      ((LinearMap.id +
                (Polynomial.eval t (S R ((m - 2) / 2)) *
                    (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
                  HSub.hSub (α := M →ₗ[R] M)
                    (LinearMap.smulRight (HSMul.hSMul (α := R) ((g : (a : M) → R) x : R) f - g) y)
                    (LinearMap.smulRight f x) +
              (Polynomial.eval t (S R ((m - 1) / 2)) *
                  (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
                HSub.hSub (α := M →ₗ[R] M)
                  (LinearMap.smulRight (HSMul.hSMul (α := R) ((f : (a : M) → R) y : R) g - f) x)
                  (LinearMap.smulRight g y) :
            (a : M) → M)
          z :
        M)
⊢ (↑((reflection hf * reflection hg) ^ m) : M →ₗ[R] M) =
    LinearMap.id +
        (Polynomial.eval t (S R ((m - 2) / 2)) *
            (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
          HSub.hSub (α := M →ₗ[R] M) (LinearMap.smulRight (HSMul.hSMul (α := R) ((g : (a : M) → R) x : R) f - g) y)
            (LinearMap.smulRight f x) +
      (Polynomial.eval t (S R ((m - 1) / 2)) *
          (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
        HSub.hSub (α := M →ₗ[R] M) (LinearMap.smulRight (HSMul.hSMul (α := R) ((f : (a : M) → R) y : R) g - f) x)
          (LinearMap.smulRight g y)

Tactic:
ext z
-- Module: Mathlib.LinearAlgebra.Reflection
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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
z : M
⊢ Eq (α := M) (((↑((reflection hf * reflection hg) ^ m) : M →ₗ[R] M) : (a : M) → M) z : M)
    ((LinearMap.id +
              (Polynomial.eval t (S R ((m - 2) / 2)) *
                  (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
                HSub.hSub (α := M →ₗ[R] M)
                  (LinearMap.smulRight (HSMul.hSMul (α := R) ((g : (a : M) → R) x : R) f - g) y)
                  (LinearMap.smulRight f x) +
            (Polynomial.eval t (S R ((m - 1) / 2)) *
                (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
              HSub.hSub (α := M →ₗ[R] M) (LinearMap.smulRight (HSMul.hSMul (α := R) ((f : (a : M) → R) y : R) g - f) x)
                (LinearMap.smulRight g y) :
          (a : M) → M)
        z :
      M)

Tactic:
simpa using reflection_mul_reflection_zpow_apply hf hg m z t ht

Premises used: Module.reflection_mul_reflection_zpow_apply
-- Module: Mathlib.LinearAlgebra.Reflection
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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
k : ℤ
⊢ Polynomial.eval t (S R (k - 2)) =
    (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
        Polynomial.eval t (S R (k - 1)) -
      Polynomial.eval t (S R k)

Tactic:
simp [S_sub_two, ht]

Premises used: Polynomial.Chebyshev.S_sub_two
-- Module: Mathlib.LinearAlgebra.Reflection
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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)

Tactic:
have S_eval_t_sub_two (k : ℤ) :
      (S R (k - 2)).eval t = (f y * g x - 2) * (S R (k - 1)).eval t - (S R k).eval t := by
    simp [S_sub_two, ht]
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
⊢ (HPow.hPow (β := ℤ) (reflection hf * reflection hg) 0 : (a : M) → M) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
succ :
  (reflection hf : (a : M) → M)
      ((reflection hg : (a : M) → M)
          ((Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
            HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) •
              y) :
        M) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) • y
⊢ ((reflection hf * reflection hg) ^ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 : (a : M) → M) x =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

Premises used: LinearEquiv.mul_apply, zpow_one_add, Nat.cast, add_comm, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
succ :
  (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) •
        (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) •
        (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) • y
⊢ (reflection hf : (a : M) → M)
      ((reflection hg : (a : M) → M)
          ((Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
            HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) •
              y) :
        M) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]

Premises used: map_sub, map_add, Module.reflection_apply, map_smul
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
match_scalars :
  (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
        (1 - HMul.hMul (α := R) 2 1 -
          HMul.hMul (α := R) ((g : (a : M) → R) x : R)
            (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R))) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
        (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R) -
          2 * -HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R)) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
        Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) *
      1
match_scalars₁ :
  (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
        -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
        (1 - HMul.hMul (α := R) 2 1) =
    HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) * 1
⊢ (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) •
        (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) •
        (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
match_scalars
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
⊢ (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
            (1 - HMul.hMul (α := R) 2 1 -
              HMul.hMul (α := R) ((g : (a : M) → R) x : R)
                (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R))) +
          HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
            (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R) -
              2 * -HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R)) +
        Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 2)) -
      ((Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
            Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) *
          1 +
        ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
            Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1)) -
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
a :
  (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
            (1 - HMul.hMul (α := R) 2 1 -
              HMul.hMul (α := R) ((g : (a : M) → R) x : R)
                (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R))) +
          HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
            (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R) -
              2 * -HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R)) +
        Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 2)) -
      ((Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
            Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) *
          1 +
        ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
            Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1)) -
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)))) =
    0
⊢ (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
        (1 - HMul.hMul (α := R) 2 1 -
          HMul.hMul (α := R) ((g : (a : M) → R) x : R)
            (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R))) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
        (-HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R) -
          2 * -HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) (1 : R)) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ))) +
        Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) *
      1

Tactic:
linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
    (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y
⊢ (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) *
        -HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) *
        (1 - HMul.hMul (α := R) 2 1) =
    HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) (-(g : (a : M) → R) x : R) * 1

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (-(↑m : ℤ)) : (a : M) → M) x =
    (Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) • y
pred :
  (reflection hg : (a : M) → M)
      ((reflection hf : (a : M) → M)
          ((Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) • x +
            HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) •
              y) :
        M) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1)))
          (-(g : (a : M) → R) x : R) •
        y
⊢ ((reflection hf * reflection hg) ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 : (a : M) → M) x =
    (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) +
          Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 - 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
rw [sub_eq_add_neg (-m : ℤ) 1, add_comm (-m : ℤ) (-1), zpow_add, zpow_neg_one, mul_inv_rev,
      reflection_inv, reflection_inv, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

Premises used: zpow_add, zpow_neg_one, Module.reflection_inv, sub_eq_add_neg, LinearEquiv.mul_apply, Nat.cast, add_comm, mul_inv_rev, OfNat.ofNat, Neg.neg
-- Module: Mathlib.LinearAlgebra.Reflection
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)
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
m : ℕ
ih :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (-(↑m : ℤ)) : (a : M) → M) x =
    (Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) • y
pred :
  (Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) •
        (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) y -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
            (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) y)) +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) •
        (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
            (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) y)) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1)))
          (-(g : (a : M) → R) x : R) •
        y
⊢ (reflection hg : (a : M) → M)
      ((reflection hf : (a : M) → M)
          ((Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) • x +
            HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) •
              y) :
        M) =
    (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)))) +
          Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1))) •
        x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1)))
          (-(g : (a : M) → R) x : R) •
        y

Tactic:
simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]

Premises used: map_sub, map_add, Module.reflection_apply, map_smul