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 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 (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) (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: linear_combination (norm := ring_nf) -S_eval_t_sub_two (-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)
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) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) - 1))) (-(g : (a : M) → R) x : R) *
      1
have 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
Tactic: linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-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
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)
⊢ ((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 zero : (HPow.hPow (β := ℤ) (reflection hf * reflection hg) 0 : (a : M) → M) x =
  (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) • x +
    HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) (-(g : (a : M) → R) x : R) • y
Tactic: induction m with
  | zero => simp
  | succ m ih =>
    -- Apply the inductive hypothesis.
    rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
    · ring_nf
  | pred m ih =>
    -- Apply the inductive hypothesis.
    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]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (-m)
    · linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)
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
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)
zero :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) 0 : (a : M) → M) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) (-(g : (a : M) → R) x : R) • y
⊢ ((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 succ : ∀ (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
Tactic: induction m with
  | zero => simp
  | succ m ih =>
    -- Apply the inductive hypothesis.
    rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
    · ring_nf
  | pred m ih =>
    -- Apply the inductive hypothesis.
    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]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (-m)
    · linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)
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 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
have 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
Tactic: rw [LinearEquiv.mul_apply, reflection_mul_reflection_zpow_apply_self hf hg m t 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)
m : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ (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
have 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
Tactic: simp only [reflection_apply, map_add, map_smul, hg]
-- 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
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) Φ Φ
⊢ f = g
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := by rintro rfl; simp at hf₁
-- 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
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
have 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)
Tactic: ext y
-- 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
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
⊢ Eq (α := M) (((↑u : M →ₗ[R] M) : (a : M) → M) y : M)
    ((LinearMap.id + LinearMap.smulRight (f - g) x : (a : M) → M) y : M)
have 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)
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]
-- 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
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₁
⊢ f = g
have hu : (↑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
-- 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
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
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
⊢ Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0
have h : ∀ (x_1 : M),
  Eq (α := M)
    ((LinearMap.smulRight (f - g) x ∘ₗ
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) :
          (a : M) → M)
        x_1 :
      M)
    ((0 : (a : M) → M) x_1 : M)
Tactic: ext
-- 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
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
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
⊢ (↑(u ^ (n + 1)) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
have this : Eq (α := M →ₗ[R] M)
  (LinearMap.smulRight (f - g) x ∘ₗ
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
  0
Tactic: have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
        ext; simp [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
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
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this :
  Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0
⊢ (↑(u ^ (n + 1)) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
have succ : HMul.hMul (α := M →ₗ[R] M) LinearMap.id LinearMap.id +
      LinearMap.id * HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
    (LinearMap.smulRight (f - g) x * LinearMap.id +
      LinearMap.smulRight (f - g) x *
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
Tactic: rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
-- 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
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
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this :
  Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0
⊢ HMul.hMul (α := M →ₗ[R] M) LinearMap.id LinearMap.id +
        LinearMap.id * HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x *
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
have succ : LinearMap.id ∘ₗ LinearMap.id +
      LinearMap.id ∘ₗ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
    HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x ∘ₗ LinearMap.id)
      (LinearMap.smulRight (f - g) x ∘ₗ
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
Tactic: simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
        add_assoc, Nat.cast_succ, add_smul, one_smul]