α : Type ?u.130531
β : Type ?u.130534
γ : Type ?u.130537
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
this : Nonempty { i // p i }
⊢ (⨆ (i : ι) (_ : p i), f i) + a = ⨆ (i : ι) (_ : p i), f i + a
α : Type ?u.130531
β : Type ?u.130534
γ : Type ?u.130537
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ (⨆ (i : ι) (_ : p i), f i) + a = ⨆ (i : ι) (_ : p i), f i + a
haveI : Nonempty { i // p i } := nonempty_subtype.2 h
no goals
α : Type ?u.130531
β : Type ?u.130534
γ : Type ?u.130537
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
this : Nonempty { i // p i }
⊢ (⨆ (i : ι) (_ : p i), f i) + a = ⨆ (i : ι) (_ : p i), f i + a
simp only [iSup_subtype', iSup_add]