awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : M
f : Dual R M
y : M
g : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
m : M
⊢ Eq (α := M)
    (((preReflection ((preReflection x f : (a : M) → M) y)
              (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
                  (a : Dual R M) → Dual R M)
                g) :
            End R M) :
          (a : M) → M)
        m :
      M)
    ((preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f : (a : M) → M) m : M)
have h₁ : m -
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
      (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x -
        HMul.hMul (α := R) ((f : (a : M) → R) m : R)
            (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
          x)) =
  m - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
        HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x) -
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x +
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x) -
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
        HMul.hMul (α := R) ((f : (a : M) → R) m : R)
            (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
          x))
Tactic: simp only [h, preReflection_apply, mul_comm (g x) (f m), mul_two, mul_assoc, Dual.eval_apply,
    LinearMap.sub_apply, LinearMap.coe_comp, LinearMap.smul_apply, smul_eq_mul, smul_sub, sub_smul,
    smul_smul, sub_mul, comp_apply, map_sub, map_smul, add_smul]
-- 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 : M
f : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hx : x ∈ p
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
have suffices : ∀ y ∈ p, Membership.mem (α := M) p ((reflection h : (a : M) → M) y : M)
Tactic: suffices ∀ y ∈ p, reflection h y ∈ p from
    (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M) ↔ p ≤ LinearMap.ker f
have refine_1 : ∀ (h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)) (y : M) (hy : y ∈ p), y ∈ LinearMap.ker f
Tactic: refine ⟨fun h' y hy ↦ ?_, fun h' y hy ↦ ?_⟩
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
refine_1 : ∀ (h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)) (y : M) (hy : y ∈ p), y ∈ LinearMap.ker f
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M) ↔ p ≤ LinearMap.ker f
have refine_2 : ∀ (h' : p ≤ LinearMap.ker f) (y : M) (hy : y ∈ p), y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
Tactic: refine ⟨fun h' y hy ↦ ?_, fun h' y hy ↦ ?_⟩
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
⊢ y ∈ LinearMap.ker f
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := by rintro rfl; exact two_ne_zero (α := R) <| by simp [← h]
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
⊢ y ∈ LinearMap.ker f
have aux : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p ⊓ R ∙ x
Tactic: have aux : f y • x ∈ p ⊓ R ∙ x := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
aux : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p ⊓ R ∙ x
⊢ y ∈ LinearMap.ker f
have aux₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R) ∨ x = 0
Tactic: rw [hp.eq_bot, Submodule.mem_bot, smul_eq_zero] at aux
Cleared hypotheses: aux
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
⊢ y ∈ LinearMap.ker f
have refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
Tactic: suffices f y • x ∈ p by
      have aux : f y • x ∈ p ⊓ R ∙ x := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩
      rw [hp.eq_bot, Submodule.mem_bot, smul_eq_zero] at aux
      exact aux.resolve_right hx
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
have h'₁ : y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
Tactic: specialize h' hy
Cleared hypotheses: h'
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
y : M
hy : y ∈ p
hx : x ≠ 0
h' : y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
have h'₁ : y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
Tactic: simp only [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply] at h'
Cleared hypotheses: h'
-- 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 : M
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ≤ LinearMap.ker f
y : M
hy : y ∈ p
⊢ y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
have hy' : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)
Tactic: have hy' : f y = 0 := by simpa using h' hy
-- 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)
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)
⊢ ((reflection hf * reflection hg) ^ (m + 1) : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 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) : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑(m + 1) : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 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)
have 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)
Tactic: have S_eval_t_sub_two (k : ℤ) :
        (S R (k - 2)).eval t = t * (S R (k - 1)).eval t - (S R k).eval t := by
      simp [S_sub_two]
-- 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)
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)
⊢ ((reflection hf * reflection hg) ^ (m + 1) : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 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) : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑(m + 1) : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 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)
have 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
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)
-- 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)
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) : 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)
have 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)
Tactic: ext z
-- 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)
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 : ℕ
⊢ (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)
have ht' : 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)]
-- 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)
m : ℤ
z : 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) z =
    z +
        (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 (β := 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 ((m - 1) / 2)) *
          (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((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)
have nat : ∀ (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: induction m using Int.negInduction with
  | nat m => exact_mod_cast reflection_mul_reflection_pow_apply hf hg m z t ht
  | neg _ m =>
    have ht' : t = g x * f y - 2 := by rwa [mul_comm (g x)]
    rw [zpow_neg, ← inv_zpow, mul_inv_rev, reflection_inv, reflection_inv, zpow_natCast,
      reflection_mul_reflection_pow_apply hg hf m z t ht', add_right_comm z]
    have aux (a b : ℤ) (hab : a + b = -3 := by lia) : a / 2 = -(b / 2) - 2 := by lia
    rw [aux (-m - 3) m, aux (-m - 2) (m - 1), aux (-m - 1) (m - 2), aux (-m) (m - 3)]
    simp only [S_neg_sub_two, Polynomial.eval_neg]
    ring_nf
Cleared hypotheses: m
-- 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)
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) : 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)
have 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)
Tactic: ext z