-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- If an element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`,
and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
element of `p` by `a` lifts `a • x`.
-/
lemma lifts_smul {x : ⨂[R] i, s i} {p : FreeAddMonoid (R × Π i, s i)} (h : p ∈ lifts x) (a : R) :
    List.map (fun (y : R × Π i, s i) ↦ (a * y.1, y.2)) p ∈ lifts (a • x)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ (List.map ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) p).sum =
    (List.map ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum

Tactic:
congr 2

Result:
case e_a.e_f
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) =
    (fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : p ∈ x.lifts
a : R
⊢ List.map (fun y => (a * y.1, y.2)) p ∈ (a • x).lifts

Tactic:
rw [mem_lifts_iff] at h ⊢

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (List.map (fun y => (a * y.1, y.2)) p)).sum = a • x

Proof state:
case e_a.e_f
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) =
    (fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i

Tactic:
ext _

Result:
case e_a.e_f.h
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
x✝ : R × ((i : ι) → s i)
⊢ ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) x✝ =
    ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) x✝

Proof state:
case e_a.e_f.h
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
x✝ : R × ((i : ι) → s i)
⊢ ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) x✝ =
    ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) x✝

Tactic:
simp only [comp_apply, smul_smul]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (List.map (fun y => (a * y.1, y.2)) p)).sum = a • x

Tactic:
rw [← List.comp_map, ← h, List.smul_sum, ← List.comp_map]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
a : R
⊢ (List.map ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) p).sum =
    (List.map ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum