-- Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
theorem projectiveSeminormAux_add_le (p q : FreeAddMonoid (𝕜 × Π i, E i)) :
    projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q

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

Tactic:
erw [List.map_append]

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

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

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q

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

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

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

Tactic:
rw [List.sum_append]

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