α : Type ?u.847795
β : Type ?u.847798
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ (a - ⨅ (i : ι), f i) ≤ c ↔ (⨆ (i : ι), a - f i) ≤ c
α : Type ?u.847795
β : Type ?u.847798
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
⊢ (a - ⨅ (i : ι), f i) = ⨆ (i : ι), a - f i
refine' eq_of_forall_ge_iff fun c => _
α : Type ?u.847795
β : Type ?u.847798
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ (a ≤ ⨅ (i : ι), f i + c) ↔ (⨆ (i : ι), a - f i) ≤ c
α : Type ?u.847795
β : Type ?u.847798
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ (a - ⨅ (i : ι), f i) ≤ c ↔ (⨆ (i : ι), a - f i) ≤ c
rw [tsub_le_iff_right, add_comm, iInf_add]
no goals
α : Type ?u.847795
β : Type ?u.847798
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ (a ≤ ⨅ (i : ι), f i + c) ↔ (⨆ (i : ι), a - f i) ≤ c
simp [tsub_le_iff_right, sub_eq_add_neg, add_comm]