awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
refine_1 : ∀ (i : ℕ), HSMul.hSMul (β := M) (r ^ i) 0 = 0
⊢ (Finsupp.sum (s • m) fun (i : ℕ) (m : M) ↦ r ^ i • m) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)
have refine_2 : (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) =
  HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)
Tactic: refine (Finsupp.sum_smul_index' ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)
have refine_2 : Eq (α := M) (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) (Finsupp.sum m fun (a : ℕ) (b : M) ↦ s • r ^ a • b)
Tactic: simp_rw [RingHom.id_apply, Finsupp.smul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ Eq (α := M) (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) (Finsupp.sum m fun (a : ℕ) (b : M) ↦ s • r ^ a • b)
have refine_2 : Eq.{u_2 + 1} (α := ℕ → M → M) (fun (i : ℕ) (c : M) ↦ r ^ i • s • c) fun (a : ℕ) (b : M) ↦ s • r ^ a • b
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ Eq.{u_2 + 1} (α := ℕ → M → M) (fun (i : ℕ) (c : M) ↦ r ^ i • s • c) fun (a : ℕ) (b : M) ↦ s • r ^ a • b
have refine_2 : ∀ (i : ℕ) (c : M), r ^ i • s • c = s • r ^ i • c
Tactic: ext i c
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
i : ℕ
c : M
⊢ r ^ i • s • c = s • r ^ i • c
have refine_2 : s • r ^ i • c = s • r ^ i • c
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
⊢ (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
have zero : (eval r : (a : PolynomialModule R M) → M) 0 =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
zero :
  (eval r : (a : PolynomialModule R M) → M) 0 =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
have zero₁ : 0 = HSMul.hSMul (β := M) (Polynomial.eval r p) 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
zero :
  (eval r : (a : PolynomialModule R M) → M) 0 =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
zero₁ : 0 = HSMul.hSMul (β := M) (Polynomial.eval r p) 0
⊢ (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
have zero₂ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add : (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add₁ : HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
    ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add₂ : HAdd.hAdd (β := M) (HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
    ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₂ :
  HAdd.hAdd (β := M) (HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add₃ : HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₂ :
  HAdd.hAdd (β := M) (HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₃ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add₄ : HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
  Polynomial.eval r p •
    HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) f : M)
      ((eval r : (a : PolynomialModule R M) → M) g : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  (eval r : (a : PolynomialModule R M) → M) (p • f) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M) (p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₂ :
  HAdd.hAdd (β := M) (HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₃ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₄ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    Polynomial.eval r p •
      HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) f : M)
        ((eval r : (a : PolynomialModule R M) → M) g : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
have add₅ : HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
p q : R[X]
e₁ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) q
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r q)
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) (p + q)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single : (eval r : (a : PolynomialModule R M) → M)
    (HSMul.hSMul (β := PolynomialModule R M) p
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) +
      HSMul.hSMul (β := PolynomialModule R M) q
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
  HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
    ((eval r : (a : PolynomialModule R M) → M)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
Tactic: rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
p q : R[X]
e₁ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) q
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r q)
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
single :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) +
        HSMul.hSMul (β := PolynomialModule R M) q
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) (p + q)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single₁ : HAdd.hAdd (α := M) (β := M)
    ((eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) p
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
      M)
    ((eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) q
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
      M) =
  HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
    ((eval r : (a : PolynomialModule R M) → M)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
Tactic: rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
n : ℕ
a : R
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial n : (a : R) → R[X]) a : R[X])
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r ((monomial n : (a : R) → R[X]) a))
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single : r ^ (n + i) • a • m = (a * r ^ n) • r ^ i • m
Tactic: simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single : ∀ (p q : R[X])
  (e₁ :
    (eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) p
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
      HSMul.hSMul (β := M) (Polynomial.eval r p)
        ((eval r : (a : PolynomialModule R M) → M)
            ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          M))
  (e₂ :
    (eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) q
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
      HSMul.hSMul (β := M) (Polynomial.eval r q)
        ((eval r : (a : PolynomialModule R M) → M)
            ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          M)),
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) (p + q)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
Tactic: induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
Cleared hypotheses: p