case empty
F : Type ?u.138129
α : Type u_2
β : Type ?u.138135
γ : Type ?u.138138
ι : Type u_1
κ : Type ?u.138144
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
⊢ a ⊓ sup ∅ f = sup ∅ fun i => a ⊓ f i

case cons
F : Type ?u.138129
α : Type u_2
β : Type ?u.138135
γ : Type ?u.138138
ι : Type u_1
κ : Type ?u.138144
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
i : ι
s : Finset ι
hi : ¬i ∈ s
h : a ⊓ sup s f = sup s fun i => a ⊓ f i
⊢ a ⊓ sup (cons i s hi) f = sup (cons i s hi) fun i => a ⊓ f i
F : Type ?u.138129
α : Type u_2
β : Type ?u.138135
γ : Type ?u.138138
ι : Type u_1
κ : Type ?u.138144
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ sup s f = sup s fun i => a ⊓ f i
induction' s using Finset.cons_induction with i s hi h
no goals
case empty
F : Type ?u.138129
α : Type u_2
β : Type ?u.138135
γ : Type ?u.138138
ι : Type u_1
κ : Type ?u.138144
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
⊢ a ⊓ sup ∅ f = sup ∅ fun i => a ⊓ f i
simp_rw [Finset.sup_empty, inf_bot_eq]
no goals
case cons
F : Type ?u.138129
α : Type u_2
β : Type ?u.138135
γ : Type ?u.138138
ι : Type u_1
κ : Type ?u.138144
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
i : ι
s : Finset ι
hi : ¬i ∈ s
h : a ⊓ sup s f = sup s fun i => a ⊓ f i
⊢ a ⊓ sup (cons i s hi) f = sup (cons i s hi) fun i => a ⊓ f i
rw [sup_cons, sup_cons, inf_sup_left, h]