awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (hypothesis)
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 (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (m - 1))) (-(g : (a : M) → R) x : R) • y
have 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)
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]
-- 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)
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
⊢ ((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
have 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
Tactic: rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
-- 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)
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
⊢ (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
have 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
Tactic: simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
-- 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)
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))) •
        (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
have 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
Tactic: match_scalars
-- 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)
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
⊢ (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
have 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
Tactic: match_scalars
-- 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)
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 (α := ℤ) 1 (↑m : ℤ))) +
        Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) 1 (↑m : ℤ) - 1))) *
      1
have 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
Tactic: linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
-- 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)
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
⊢ ((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
have 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
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]
-- 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)
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
⊢ (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
have 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
Tactic: simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
-- 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)
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))) •
        (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
have 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
Tactic: match_scalars
-- 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)
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
⊢ (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
have 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
Tactic: match_scalars