case h₀
F : Type ?u.199570
α : Type u_2
β : Type ?u.199576
γ : Type ?u.199579
ι : Type u_1
κ : Type ?u.199585
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
⊢ (inf {b} fun b => a \ f b) = a \ sup {b} f

case h₁
F : Type ?u.199570
α : Type u_2
β : Type ?u.199576
γ : Type ?u.199579
ι : Type u_1
κ : Type ?u.199585
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
h✝ : ¬b ∈ t
hs✝ : Finset.Nonempty t
h : (inf t fun b => a \ f b) = a \ sup t f
⊢ (inf (cons b t h✝) fun b => a \ f b) = a \ sup (cons b t h✝) f
F : Type ?u.199570
α : Type u_2
β : Type ?u.199576
γ : Type ?u.199579
ι : Type u_1
κ : Type ?u.199585
inst✝ : BooleanAlgebra α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
a : α
⊢ (inf s fun b => a \ f b) = a \ sup s f
induction' hs using Finset.Nonempty.cons_induction with b b t _ _ h
no goals
case h₀
F : Type ?u.199570
α : Type u_2
β : Type ?u.199576
γ : Type ?u.199579
ι : Type u_1
κ : Type ?u.199585
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
⊢ (inf {b} fun b => a \ f b) = a \ sup {b} f
rw [sup_singleton, inf_singleton]
no goals
case h₁
F : Type ?u.199570
α : Type u_2
β : Type ?u.199576
γ : Type ?u.199579
ι : Type u_1
κ : Type ?u.199585
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
h✝ : ¬b ∈ t
hs✝ : Finset.Nonempty t
h : (inf t fun b => a \ f b) = a \ sup t f
⊢ (inf (cons b t h✝) fun b => a \ f b) = a \ sup (cons b t h✝) f
rw [sup_cons, inf_cons, h, sdiff_sup]