-- Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
theorem projectiveSeminormAux_smul (p : FreeAddMonoid (𝕜 × Π i, E i)) (a : 𝕜) :
    projectiveSeminormAux (List.map (fun (y : 𝕜 × Π i, E i) ↦ (a * y.1, y.2)) p) =
    ‖a‖ * projectiveSeminormAux p

Proof state:
case e_a.e_f
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) =
    (fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖

Tactic:
ext x

Result:
case e_a.e_f.h
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
x : 𝕜 × ((i : ι) → E i)
⊢ ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) x =
    ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) x

Proof state:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ (List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum =
    (List.map ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum

Tactic:
congr 2

Result:
case e_a.e_f
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) =
    (fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖

Proof state:
case e_a.e_f.h
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
x : 𝕜 × ((i : ι) → E i)
⊢ ‖a‖ * ‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖ = ‖a‖ * (‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ projectiveSeminormAux (List.map (fun y => (a * y.1, y.2)) p) = ‖a‖ * projectiveSeminormAux p

Tactic:
simp only [projectiveSeminormAux, Function.comp_apply, Multiset.map_coe, List.map_map,
  Multiset.sum_coe]

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ (List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum =
    ‖a‖ * (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum

Proof state:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ (List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum =
    ‖a‖ * (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum

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

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
⊢ (List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum =
    (List.map ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum

Proof state:
case e_a.e_f.h
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
x : 𝕜 × ((i : ι) → E i)
⊢ ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) x =
    ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) x

Tactic:
simp only [Function.comp_apply, norm_mul, smul_eq_mul]

Result:
case e_a.e_f.h
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : 𝕜
x : 𝕜 × ((i : ι) → E i)
⊢ ‖a‖ * ‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖ = ‖a‖ * (‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖)