case intro
α : Type ?u.628429
E : α → Type ?u.628434
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i => ‖OfNat.ofNat 1 i‖) i ≤ 1
α : Type ?u.628429
E : α → Type ?u.628434
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
⊢ 1 ∈ upperBounds (Set.range fun i => ‖OfNat.ofNat 1 i‖)
rintro i ⟨i, rfl⟩
no goals
case intro
α : Type ?u.628429
E : α → Type ?u.628434
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i => ‖OfNat.ofNat 1 i‖) i ≤ 1
exact norm_one.le