F : Type ?u.139618
α : Type u_2
β : Type ?u.139624
γ : Type ?u.139627
ι : Type u_1
κ : Type ?u.139633
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ (sup s fun i => a ⊓ f i) = sup s fun i => f i ⊓ a
F : Type ?u.139618
α : Type u_2
β : Type ?u.139624
γ : Type ?u.139627
ι : Type u_1
κ : Type ?u.139633
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ sup s f ⊓ a = sup s fun i => f i ⊓ a
rw [_root_.inf_comm, s.sup_inf_distrib_left]
no goals
F : Type ?u.139618
α : Type u_2
β : Type ?u.139624
γ : Type ?u.139627
ι : Type u_1
κ : Type ?u.139633
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ (sup s fun i => a ⊓ f i) = sup s fun i => f i ⊓ a
simp_rw [_root_.inf_comm]