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

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

Tactic:
refine List.sum_nonneg ?_

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ ∀ x ∈ List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p, 0 ≤ 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 : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ p
h : ‖x‖ * ∏ x : ι, ‖m x‖ = a
⊢ 0 ≤ a

Tactic:
rw [← h]

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ p
h : ‖x‖ * ∏ x : ι, ‖m x‖ = a
⊢ 0 ≤ ‖x‖ * ∏ x : ι, ‖m 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 : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ p
h : ‖x‖ * ∏ x : ι, ‖m x‖ = a
⊢ 0 ≤ ‖x‖ * ∏ x : ι, ‖m x‖

Tactic:
exact mul_nonneg (norm_nonneg _) (Finset.prod_nonneg (fun _ _ ↦ norm_nonneg _))

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 : ℝ
⊢ ∀ (x : 𝕜) (x_1 : (i : ι) → E i), (x, x_1) ∈ p → ‖x‖ * ∏ x : ι, ‖x_1 x‖ = a → 0 ≤ a

Tactic:
intro x m _ h

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ p
h : ‖x‖ * ∏ x : ι, ‖m x‖ = a
⊢ 0 ≤ a

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

Tactic:
simp only [Multiset.map_coe, Multiset.mem_coe, List.mem_map, Prod.exists, forall_exists_index,
  and_imp]

Result:
ι : Type uι
inst✝² : Fintype ι
𝕜 : Type u𝕜
inst✝¹ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝ : (i : ι) → SeminormedAddCommGroup (E i)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
⊢ ∀ (x : 𝕜) (x_1 : (i : ι) → E i), (x, x_1) ∈ p → ‖x‖ * ∏ x : ι, ‖x_1 x‖ = a → 0 ≤ a

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

Tactic:
intro a

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

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

Tactic:
simp only [projectiveSeminormAux, Function.comp_apply]

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