case refine'_1
F : Type ?u.198274
α : Type u_2
β : Type ?u.198280
γ : Type ?u.198283
ι : Type u_1
κ : Type ?u.198289
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
⊢ (sup ∅ fun b => a \ f b) = a \ inf ∅ f

case refine'_2
F : Type ?u.198274
α : Type u_2
β : Type ?u.198280
γ : Type ?u.198283
ι : Type u_1
κ : Type ?u.198289
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
x✝ : ¬b ∈ t
h : (sup t fun b => a \ f b) = a \ inf t f
⊢ (sup (cons b t x✝) fun b => a \ f b) = a \ inf (cons b t x✝) f
F : Type ?u.198274
α : Type u_2
β : Type ?u.198280
γ : Type ?u.198283
ι : Type u_1
κ : Type ?u.198289
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
⊢ (sup s fun b => a \ f b) = a \ inf s f
refine' Finset.cons_induction_on s _ fun b t _ h => _
no goals
case refine'_1
F : Type ?u.198274
α : Type u_2
β : Type ?u.198280
γ : Type ?u.198283
ι : Type u_1
κ : Type ?u.198289
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
⊢ (sup ∅ fun b => a \ f b) = a \ inf ∅ f
rw [sup_empty, inf_empty, sdiff_top]
no goals
case refine'_2
F : Type ?u.198274
α : Type u_2
β : Type ?u.198280
γ : Type ?u.198283
ι : Type u_1
κ : Type ?u.198289
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
x✝ : ¬b ∈ t
h : (sup t fun b => a \ f b) = a \ inf t f
⊢ (sup (cons b t x✝) fun b => a \ f b) = a \ inf (cons b t x✝) f
rw [sup_cons, inf_cons, h, sdiff_inf]