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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (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)
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
k : ℤ
⊢ HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
      t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
    1

Tactic:
simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)

Premises used: Polynomial.eval, Polynomial.Chebyshev.S_sq_add_S_sq, congr_arg
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (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)
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
⊢ ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1

Tactic:
have S_eval_t_sq_add_S_eval_t_sq (k : ℤ) :
        (S R k).eval t ^ 2 + (S R (k + 1)).eval t ^ 2 - t * (S R k).eval t * (S R (k + 1)).eval t
        = 1 := by
      simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R k) + Polynomial.eval t (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)
e : ℤ := HMod.hMod (α := ℤ) (↑m : ℤ) 2
⊢ Ne (α := ℤ) 2 0

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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R k) + Polynomial.eval t (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)
e : ℤ := HMod.hMod (α := ℤ) (↑m : ℤ) 2
⊢ e = 0 ∨ e = 1

Tactic:
lia
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R k) + Polynomial.eval t (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)
e : ℤ := HMod.hMod (α := ℤ) (↑m : ℤ) 2
⊢ e = 0 ∨ e = 1

Tactic:
have he : e = 0 ∨ e = 1 := by lia
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R k) + Polynomial.eval t (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)
e : ℤ
he : e = 0 ∨ e = 1
⊢ Eq.{u_1 + 1} (α := R) 1 1

Tactic:
rfl
-- 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 (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
                    (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
                      Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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 (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
                  (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
                    Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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 (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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 (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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 (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
                  (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
                    Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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 (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
                (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
                  Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑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_pow_apply hf hg m z t ht

Premises used: Module.reflection_mul_reflection_pow_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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
⊢ (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (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 t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (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)

Tactic:
exact_mod_cast reflection_mul_reflection_pow_apply hf hg m z t ht

Premises used: Module.reflection_mul_reflection_pow_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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
h :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑n : ℤ) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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 t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑n : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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)
m : ℕ
rwa rwa₁ rwa₂ rwa₃ : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ t = HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R) - 2

Tactic:
rwa [mul_comm (g x)]

Premises used: mul_comm, DFunLike.coe
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
h :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑n : ℤ) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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 t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑n : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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)
m : ℕ
⊢ t = HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R) - 2

Tactic:
have ht' : t = g x * f y - 2 := by rwa [mul_comm (g x)]
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
h :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑n : ℤ) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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 t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑n : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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)
m : ℕ
ht' : t = HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R) - 2
a b : ℤ
hab : a + b = -3
⊢ a / 2 = -(b / 2) - 2

Tactic:
lia
-- 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)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
h :
  ∀ (n : ℕ),
    (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑n : ℤ) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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 t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑n : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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)
m : ℕ
ht' : t = HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R) - 2
⊢ ∀ (a b : ℤ) (hab : autoParam (a + b = -3) reflection_mul_reflection_zpow_apply._auto_2), a / 2 = -(b / 2) - 2

Tactic:
have aux (a b : ℤ) (hab : a + b = -3 := by lia) : a / 2 = -(b / 2) - 2 := by lia