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)
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) (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) =
    (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) -
          2 * -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) ((f : (a : M) → R) y : R)
            (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) =
    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) ((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

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) (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) +
        Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 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 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) -
          Polynomial.eval t (S R (-(↑m : ℤ))))) =
    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) (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) +
        Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 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 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) -
          Polynomial.eval t (S R (-(↑m : ℤ))))) =
    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) (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) =
    (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)

Premises used: Nat.cast, 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
⊢ (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) -
              2 * -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) ((f : (a : M) → R) y : R)
                (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) +
        HMul.hMul (α := R) ((g : (a : M) → R) x : R)
          ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) -
            Polynomial.eval t (S R (-(↑m : ℤ)))) -
      (HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1)))
            (-(g : (a : M) → R) x : R) *
          1 +
        HMul.hMul (α := R) ((g : (a : M) → R) x : R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 2)))) =
    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))) *
            (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R) -
              2 * -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) ((f : (a : M) → R) y : R)
                (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) +
        HMul.hMul (α := R) ((g : (a : M) → R) x : R)
          ((HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) -
            Polynomial.eval t (S R (-(↑m : ℤ)))) -
      (HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1)))
            (-(g : (a : M) → R) x : R) *
          1 +
        HMul.hMul (α := R) ((g : (a : M) → R) x : R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 2)))) =
    0
⊢ (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) -
          2 * -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) ((f : (a : M) → R) y : R)
            (-HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) (1 : R))) =
    HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1))) (-(g : (a : M) → R) x : R) *
      1

Tactic:
linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)

Premises used: Nat.cast, DFunLike.coe, 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)
m : ℕ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ ((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

Tactic:
mod_cast reflection_mul_reflection_zpow_apply_self hf hg m t ht

Premises used: zpow_natCast, Polynomial.eval, HMul.hMul, congrArg, HSub.hSub, cast, Polynomial.Chebyshev.S, Nat.cast, HPow.hPow, HAdd.hAdd, Int.cast_subNatNat._simp_1, congr, Module.reflection_mul_reflection_zpow_apply_self, Module.reflection, HSMul.hSMul, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Neg.neg, Eq.trans
-- 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
rw :
  (reflection hg : (a : M) → M)
      ((Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
        HMul.hMul (β := R) (Polynomial.eval t (S R (m - 1))) (-(g : (a : M) → R) x : R) • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R m)) (-(g : (a : M) → R) x : R) • y
⊢ (reflection hg * (reflection hf * reflection hg) ^ m : (a : M) → M) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R m)) (-(g : (a : M) → R) x : R) • y

Tactic:
rw [LinearEquiv.mul_apply, reflection_mul_reflection_zpow_apply_self hf hg m t ht]

Premises used: LinearEquiv.mul_apply, Module.reflection_mul_reflection_zpow_apply_self
-- 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
simp :
  (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) •
        (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 (m - 1))) (-(g : (a : M) → R) x : R) •
        (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R m)) (-(g : (a : M) → R) x : R) • y
⊢ (reflection hg : (a : M) → M)
      ((Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
        HMul.hMul (β := R) (Polynomial.eval t (S R (m - 1))) (-(g : (a : M) → R) x : R) • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R m)) (-(g : (a : M) → R) x : R) • y

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

Premises used: 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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) •
        (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 (m - 1))) (-(g : (a : M) → R) x : R) •
        (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R m)) (-(g : (a : M) → R) x : R) • y

Tactic:
module
-- 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
⊢ (reflection hg * (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 (↑m : ℤ))) (-(g : (a : M) → R) x : R) • y

Tactic:
mod_cast reflection_mul_reflection_mul_reflection_zpow_apply_self hf hg m t ht

Premises used: zpow_natCast, Polynomial.eval, HMul.hMul, congrArg, HSub.hSub, cast, Polynomial.Chebyshev.S, Nat.cast, HPow.hPow, HAdd.hAdd, Int.cast_subNatNat._simp_1, congr, Module.reflection, HSMul.hSMul, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Neg.neg, Module.reflection_mul_reflection_mul_reflection_zpow_apply_self, Eq.trans
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) 0 : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection 0 f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) 0 : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection 0 g) : (a : M) → M) Φ Φ
⊢ False

Tactic:
simp at hf₁
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by rintro rfl; simp at hf₁
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
h :
  ∀ (y : M),
    Eq (α := M) (((↑u : M →ₗ[R] M) : (a : M) → M) y : M)
      ((LinearMap.id + LinearMap.smulRight (f - g) x : (a : M) → M) y : M)
⊢ (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x

Tactic:
ext y
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
y : M
h :
  y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) y : R) x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x =
    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) y : R) x)
⊢ Eq (α := M) (((↑u : M →ₗ[R] M) : (a : M) → M) y : M)
    ((LinearMap.id + LinearMap.smulRight (f - g) x : (a : M) → M) y : M)

Tactic:
simp only [u, reflection_apply, hg₁, two_smul, LinearEquiv.coe_toLinearMap_mul,
      LinearMap.id_coe, LinearEquiv.coe_coe, Module.End.mul_apply, LinearMap.add_apply, id_eq,
      LinearMap.coe_smulRight, LinearMap.sub_apply, map_sub, map_smul, sub_add_cancel_left,
      smul_neg, sub_neg_eq_add, sub_smul]

Premises used: map_sub, LinearMap.id_coe, LinearMap.add_apply, LinearEquiv.coe_toLinearMap_mul, sub_smul, two_smul, smul_neg, sub_add_cancel_left, LinearMap.sub_apply, LinearMap.coe_smulRight, Module.End.mul_apply, Module.reflection_apply, sub_neg_eq_add, LinearEquiv.coe_coe, map_smul, id_eq
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
y : M
⊢ y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) y : R) x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x =
    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) y : R) x)

Tactic:
abel
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
⊢ (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x

Tactic:
have hu : u = LinearMap.id (R := R) (M := M) + (f - g).smulRight x := by
    ext y
    simp only [u, reflection_apply, hg₁, two_smul, LinearEquiv.coe_toLinearMap_mul,
      LinearMap.id_coe, LinearEquiv.coe_coe, Module.End.mul_apply, LinearMap.add_apply, id_eq,
      LinearMap.coe_smulRight, LinearMap.sub_apply, map_sub, map_smul, sub_add_cancel_left,
      smul_neg, sub_neg_eq_add, sub_smul]
    abel
-- 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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ (↑(HPow.hPow (β := ℕ) u 0) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑0 : R) (LinearMap.smulRight (f - g) x)

Tactic:
simp