infi_insert'

Stream: Is there code for X?

[Adam Topaz]

Do we have this variant of docs#infi_insert ?

import order.complete_lattice

open_locale classical

example {α β : Type*} [complete_lattice β] (a : α) (G : set α)
  (T : Π x (hx : x ∈ insert a G), β) : (⨅ x (hx : x ∈ insert a G), T x hx) =
  T a (set.mem_insert _ _) ⊓ ⨅ x (hx : x ∈ G), T x (set.mem_insert_of_mem _ hx) := sorry