no goals
ι : Type ?u.428568
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
x : α
hx : x ∈ s
⊢ (fun x hx => { val := x, property := hx }) x hx ∈ univ
simp
ι : Type ?u.428568
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
a : α
ha : a ∈ s
⊢ (if hx : p a then f a hx else g a hx) = f a (_ : p a)
ι : Type ?u.428568
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
a : α
ha : a ∈ s
⊢ (if hx : p a then f a hx else g a hx) =
    f ↑((fun x hx => { val := x, property := hx }) a ha) (_ : p ↑((fun x hx => { val := x, property := hx }) a ha))
dsimp
no goals
ι : Type ?u.428568
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
a : α
ha : a ∈ s
⊢ (if hx : p a then f a hx else g a hx) = f a (_ : p a)
rw [dif_pos]
no goals
ι : Type ?u.428568
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
b : { x // x ∈ s }
_hb : b ∈ univ
⊢ b = (fun x hx => { val := x, property := hx }) ↑b (_ : ↑b ∈ s)
simp