no goals
α✝ : Type ?u.258029
β : Type ?u.258032
γ : Type ?u.258035
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
a : α
f : α → ℝ≥0∞
x✝ : α
h : x✝ ≠ a
⊢ (⨆ (_ : a = x✝), f x✝) = 0
simp [h.symm]
no goals
α✝ : Type ?u.258029
β : Type ?u.258032
γ : Type ?u.258035
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
a : α
f : α → ℝ≥0∞
⊢ (⨆ (_ : a = a), f a) = f a
simp