-- Mathlib/Tactic/Module.lean
theorem eval_smul [AddCommMonoid M] [Semiring R] [Module R M] {l : NF R M} {x : M} (h : x = l.eval)
    (r : R) : (r • l).eval = r • x

Proof state:
case e_a.e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) = (fun x => r • x) ∘ fun x => x.1 • x.2

Tactic:
ext p

Result:
case e_a.e_f.h
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
p : R × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) p = ((fun x => r • x) ∘ fun x => x.1 • x.2) p

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h : x = l.eval
r : R
⊢ (r • l).eval = r • x

Tactic:
unfold NF.eval at h ⊢

Result:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        (r • l)).sum =
    r • x

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) l).sum = (map ((fun x => r • x) ∘ fun x => x.1 • x.2) l).sum

Tactic:
congr

Result:
case e_a.e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) = (fun x => r • x) ∘ fun x => x.1 • x.2

Proof state:
case e_a.e_f.h
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
p : R × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) p = ((fun x => r • x) ∘ fun x => x.1 • x.2) p

Tactic:
simp [mul_smul]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        (r • l)).sum =
    r • x

Tactic:
simp only [h, smul_sum, map_map, NF.smul_apply]

Result:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => (r * x.1, x.2)) l).sum = (map ((fun x => r • x) ∘ fun x => x.1 • x.2) l).sum