case h₀
F : Type ?u.200836
α : Type u_2
β : Type ?u.200842
γ : Type ?u.200845
ι : Type u_1
κ : Type ?u.200851
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
⊢ (inf {b} fun b => f b \ a) = inf {b} f \ a

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