α : Type ?u.140110
β : Type ?u.140113
γ : Type ?u.140116
a✝ b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
q : ι' → Prop
hp : ∃ i, p i
hq : ∃ j, q j
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a
⊢ (⨆ (i : ι) (_ : p i) (i_1 : ι') (_ : q i_1), f i + g i_1) ≤ a
α : Type ?u.140110
β : Type ?u.140113
γ : Type ?u.140116
a✝ b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
q : ι' → Prop
hp : ∃ i, p i
hq : ∃ j, q j
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a
⊢ ((⨆ (i : ι) (_ : p i), f i) + ⨆ (j : ι') (_ : q j), g j) ≤ a
simp_rw [biSup_add' hp, add_biSup' hq]
no goals
α : Type ?u.140110
β : Type ?u.140113
γ : Type ?u.140116
a✝ b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
q : ι' → Prop
hp : ∃ i, p i
hq : ∃ j, q j
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a
⊢ (⨆ (i : ι) (_ : p i) (i_1 : ι') (_ : q i_1), f i + g i_1) ≤ a
exact iSup₂_le fun i hi => iSup₂_le (h i hi)