ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.sup f = ⨆ a ∈ s, f a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>s : Finset α<GOAL>s.sup id = sSup ↑s
<VAR>α : Type u_2<VAR>s : Finset (Set α)<GOAL>s.sup id = ⋃₀ ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Finset α<VAR>f : α → Set β<GOAL>s.sup f = ⋃ x ∈ s, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.sup f = sSup (f '' ↑s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<GOAL>s.inf f = (Multiset.map f s.val).inf
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>f : β → α<GOAL>∅.inf f = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∉ s<GOAL>(Finset.cons b s h).inf f = f b ⊓ s.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).inf f = f b ⊓ s.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>g : β → α<GOAL>(Finset.image f s).inf g = s.inf (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<GOAL>(Finset.map f s).inf g = s.inf (g ∘ ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>f : β → α<VAR>b : β<GOAL>{b}.inf f = f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f g : β → α<GOAL>s.inf (f ⊓ g) = s.inf f ⊓ s.inf g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s₁ s₂ : Finset β<VAR>f g : β → α<VAR>hs : s₁ = s₂<VAR>hfg : ∀ a ∈ s₂, f a = g a<GOAL>s₁.inf f = s₂.inf g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>FunLike F α β<VAR>InfTopHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>g : ι → α<GOAL>f (s.inf g) = s.inf (⇑f ∘ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>a : α<GOAL>a ≤ s.inf fun x => a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>hb : b ∈ s<GOAL>s.inf f ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ s<VAR>h : f b ≤ a<GOAL>s.inf f ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>DecidableEq β<GOAL>(s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>f : β → α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>t : γ → Finset β<GOAL>(s.biUnion t).inf f = s.inf fun x => (t x).inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>h : s.Nonempty<VAR>c : α<GOAL>(s.inf fun x => c) = c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<GOAL>(s.inf fun x => ⊤) = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f g : β → α<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>(s.inf fun i => if p i then f i else g i) = (Finset.filter p s).inf f ⊓ (Finset.filter (fun i => ¬p i) s).inf g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f g : β → α<VAR>h : ∀ b ∈ s, f b ≤ g b<GOAL>s.inf f ≤ s.inf g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>h : s₁ ⊆ s₂<GOAL>s₂.inf f ≤ s₁.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β → γ → α<GOAL>(s.inf fun b => t.inf (f b)) = t.inf fun c => s.inf fun b => f b c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<GOAL>(s.attach.inf fun x => f ↑x) = s.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<GOAL>(s ×ˢ t).inf f = s.inf fun i => t.inf fun i' => f (i, i')
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<GOAL>(s ×ˢ t).inf f = t.inf fun i' => s.inf fun i => f (i, i')
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>OrderTop α<VAR>OrderTop β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(s.erase ⊤).inf id = s.inf id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>SemilatticeInf γ<VAR>OrderTop γ<VAR>s : Finset β<VAR>f : β → α<VAR>g : α → γ<VAR>g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y<VAR>top : g ⊤ = ⊤<GOAL>g (s.inf f) = s.inf (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>P : α → Prop<VAR>Ptop : P ⊤<VAR>Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)<VAR>t : Finset β<VAR>f : β → { x // P x }<GOAL>↑(t.inf f) = t.inf fun x => ↑(f x)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>l : List α<GOAL>List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l = l.toFinset.inf id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<VAR>p : α → Prop<VAR>ht : p ⊤<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>p (s.inf f)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Set α<VAR>w₁ : ⊤ ∈ s<VAR>w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s<VAR>ι : Type u_7<VAR>t : Finset ι<VAR>p : ι → α<VAR>h : ∀ i ∈ t, p i ∈ s<GOAL>t.inf p ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>f : β → α<VAR>S : Finset β<GOAL>S.inf f = ⊤ ↔ ∀ s ∈ S, f s = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<GOAL>OrderDual.toDual (s.sup f) = s.inf (⇑OrderDual.toDual ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → α<GOAL>OrderDual.toDual (s.inf f) = s.sup (⇑OrderDual.toDual ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>f : β → αᵒᵈ<GOAL>OrderDual.ofDual (s.sup f) = s.inf (⇑OrderDual.ofDual ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → αᵒᵈ<GOAL>OrderDual.ofDual (s.inf f) = s.sup (⇑OrderDual.ofDual ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊓ s.sup f = s.sup fun i => a ⊓ f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>s.sup f ⊓ a = s.sup fun i => f i ⊓ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊔ s.inf f = s.inf fun i => a ⊔ f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>s.inf f ⊔ a = s.inf fun i => f i ⊔ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderTop α<VAR>f : ι → α<VAR>s : Finset ι<VAR>a : α<GOAL>Codisjoint a (s.inf f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint a (f i)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>OrderTop α<VAR>f : ι → α<VAR>s : Finset ι<VAR>a : α<GOAL>Codisjoint (s.inf f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint (f i) a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DistribLattice α<VAR>OrderTop α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun i => f i.1 ⊔ g i.2
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq ι<VAR>κ : ι → Type u_7<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>(s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq ι<VAR>κ : ι → Type u_7<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>(s.sup fun i => (t i).inf (f i)) = (s.pi t).inf fun g => s.attach.sup fun i => f (↑i) (g ↑i ⋯)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup fun b => a \ f b) = a \ s.inf f
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.inf fun b => a \ f b) = a \ s.sup f
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.inf fun b => f b \ a) = s.inf f \ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(s.inf fun b => f b ⇨ a) = s.sup f ⇨ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup fun b => f b ⇨ a) = s.inf f ⇨ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup fun b => a ⇨ f b) = a ⇨ s.sup f
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(s.sup f)ᶜ = s.inf fun i => (f i)ᶜ
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>BooleanAlgebra α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(s.inf f)ᶜ = s.sup fun i => (f i)ᶜ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>g : α → β<VAR>mono_g : Monotone g<VAR>bot : g ⊥ = ⊥<GOAL>g (s.sup f) = s.sup (g ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<VAR>ha : ⊥ < a<GOAL>a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b
<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrder α<VAR>BoundedOrder α<VAR>Nontrivial α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrder α<VAR>BoundedOrder α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>a < s.sup f ↔ ∃ b ∈ s, a < f b
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<VAR>ha : ⊥ < a<GOAL>s.sup f < a ↔ ∀ b ∈ s, f b < a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>g : α → β<VAR>mono_g : Monotone g<VAR>top : g ⊤ = ⊤<GOAL>g (s.inf f) = s.inf (g ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<VAR>ha : a < ⊤<GOAL>s.inf f ≤ a ↔ ∃ b ∈ s, f b ≤ a
<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrder α<VAR>BoundedOrder α<VAR>Nontrivial α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥
<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrder α<VAR>BoundedOrder α<VAR>s : Finset ι<VAR>f : ι → α<VAR>h : s.Nonempty<GOAL>s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>s.inf f < a ↔ ∃ b ∈ s, f b < a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<VAR>ha : a < ⊤<GOAL>a < s.inf f ↔ ∀ b ∈ s, a < f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.inf f = ⨅ a ∈ s, f a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>s : Finset α<GOAL>s.inf id = sInf ↑s
<VAR>α : Type u_2<VAR>s : Finset (Set α)<GOAL>s.inf id = ⋂₀ ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Finset α<VAR>f : α → Set β<GOAL>s.inf f = ⋂ x ∈ s, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.inf f = sInf (f '' ↑s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∈ s<GOAL>∃ a, s.sup (WithBot.some ∘ f) = ↑a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<GOAL>↑(s.sup' H f) = s.sup (WithBot.some ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>b : β<VAR>hb : b ∉ s<GOAL>(Finset.cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).sup' ⋯ f = f b ⊔ s.sup' H f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>f : β → α<VAR>b : β<GOAL>{b}.sup' ⋯ f = f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∈ s<GOAL>f b ≤ s.sup' ⋯ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ s<VAR>h : a ≤ f b<GOAL>a ≤ s.sup' ⋯ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>a : α<GOAL>(s.sup' H fun x => a) = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>DecidableEq β<VAR>s₁ s₂ : Finset β<VAR>h₁ : s₁.Nonempty<VAR>h₂ : s₂.Nonempty<VAR>f : β → α<GOAL>(s₁ ∪ s₂).sup' ⋯ f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>f : β → α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>Hs : s.Nonempty<VAR>t : γ → Finset β<VAR>Ht : ∀ (b : γ), (t b).Nonempty<GOAL>(s.biUnion t).sup' ⋯ f = s.sup' Hs fun b => (t b).sup' ⋯ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>t : Finset γ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : β → γ → α<GOAL>(s.sup' hs fun b => t.sup' ht (f b)) = t.sup' ht fun c => s.sup' hs fun b => f b c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup' h f = s.sup' ⋯ fun i => t.sup' ⋯ fun i' => f (i, i')
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup' h f = t.sup' ⋯ fun i' => s.sup' ⋯ fun i => f (i, i')
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (Prod.map f g)
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hst : (s ×ˢ t).Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>p : α → Prop<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>p (s.sup' H f)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>w : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s<VAR>ι : Type u_7<VAR>t : Finset ι<VAR>H : t.Nonempty<VAR>p : ι → α<VAR>h : ∀ i ∈ t, p i ∈ s<GOAL>t.sup' H p ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>t : Finset β<VAR>f g : β → α<VAR>h₁ : s = t<VAR>h₂ : ∀ x ∈ s, f x = g x<GOAL>s.sup' H f = t.sup' ⋯ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup γ<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>g : α → γ<VAR>g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y<GOAL>g (s.sup' H f) = s.sup' H (g ∘ f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → α<GOAL>f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)
<VAR>β : Type u_3<VAR>α' : Type u_7<VAR>LinearOrderedAddCommMonoid β<VAR>s : Finset α'<VAR>hs : s.Nonempty<VAR>f : α' → β<VAR>n : ℕ<GOAL>(s.sup' hs fun a => n • f a) = n • s.sup' hs f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : (Finset.image f s).Nonempty<VAR>g : β → α<GOAL>(Finset.image f s).sup' hs g = s.sup' ⋯ (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : s.Nonempty<VAR>g : β → α<GOAL>s.sup' hs (g ∘ f) = (Finset.image f s).sup' ⋯ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : (Finset.map f s).Nonempty<GOAL>(Finset.map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : s.Nonempty<GOAL>s.sup' hs (g ∘ ⇑f) = (Finset.map f s).sup' ⋯ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>f : β → α<VAR>s₁ s₂ : Finset β<VAR>h : s₁ ⊆ s₂<VAR>h₁ : s₁.Nonempty<GOAL>s₁.sup' h₁ f ≤ s₂.sup' ⋯ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>f : β → α<VAR>s₁ s₂ : Finset β<VAR>h : s₁ ⊆ s₂<VAR>h₁ : s₁.Nonempty<VAR>h₂ : s₂.Nonempty<GOAL>s₁.sup' h₁ f ≤ s₂.sup' h₂ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∈ s<GOAL>∃ a, s.inf (WithTop.some ∘ f) = ↑a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<GOAL>↑(s.inf' H f) = s.inf (WithTop.some ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>b : β<VAR>hb : b ∉ s<GOAL>(Finset.cons b s hb).inf' ⋯ f = f b ⊓ s.inf' H f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).inf' ⋯ f = f b ⊓ s.inf' H f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>f : β → α<VAR>b : β<GOAL>{b}.inf' ⋯ f = f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<VAR>hs : ∀ b ∈ s, a ≤ f b<GOAL>a ≤ s.inf' H f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∈ s<GOAL>s.inf' ⋯ f ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ s<VAR>h : f b ≤ a<GOAL>s.inf' ⋯ f ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>a : α<GOAL>(s.inf' H fun x => a) = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>DecidableEq β<VAR>s₁ s₂ : Finset β<VAR>h₁ : s₁.Nonempty<VAR>h₂ : s₂.Nonempty<VAR>f : β → α<GOAL>(s₁ ∪ s₂).inf' ⋯ f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>f : β → α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>Hs : s.Nonempty<VAR>t : γ → Finset β<VAR>Ht : ∀ (b : γ), (t b).Nonempty<GOAL>(s.biUnion t).inf' ⋯ f = s.inf' Hs fun b => (t b).inf' ⋯ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>t : Finset γ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : β → γ → α<GOAL>(s.inf' hs fun b => t.inf' ht (f b)) = t.inf' ht fun c => s.inf' hs fun b => f b c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<GOAL>(s ×ˢ t).inf' h f = s.inf' ⋯ fun i => t.inf' ⋯ fun i' => f (i, i')
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<GOAL>(s ×ˢ t).inf' h f = t.inf' ⋯ fun i' => s.inf' ⋯ fun i => f (i, i')
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (Prod.map f g)
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hst : (s ×ˢ t).Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf γ<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>g : α → γ<VAR>g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y<GOAL>g (s.inf' H f) = s.inf' H (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>p : α → Prop<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>p (s.inf' H f)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>w : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s<VAR>ι : Type u_7<VAR>t : Finset ι<VAR>H : t.Nonempty<VAR>p : ι → α<VAR>h : ∀ i ∈ t, p i ∈ s<GOAL>t.inf' H p ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>t : Finset β<VAR>f g : β → α<VAR>h₁ : s = t<VAR>h₂ : ∀ x ∈ s, f x = g x<GOAL>s.inf' H f = t.inf' ⋯ g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → α<GOAL>f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)
<VAR>β : Type u_3<VAR>α' : Type u_7<VAR>LinearOrderedAddCommMonoid β<VAR>s : Finset α'<VAR>hs : s.Nonempty<VAR>f : α' → β<VAR>n : ℕ<GOAL>(s.inf' hs fun a => n • f a) = n • s.inf' hs f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : (Finset.image f s).Nonempty<VAR>g : β → α<GOAL>(Finset.image f s).inf' hs g = s.inf' ⋯ (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : s.Nonempty<VAR>g : β → α<GOAL>s.inf' hs (g ∘ f) = (Finset.image f s).inf' ⋯ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : (Finset.map f s).Nonempty<GOAL>(Finset.map f s).inf' hs g = s.inf' ⋯ (g ∘ ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeInf α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : s.Nonempty<GOAL>s.inf' hs (g ∘ ⇑f) = (Finset.map f s).inf' ⋯ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>f : β → α<VAR>s₁ s₂ : Finset β<VAR>h : s₁ ⊆ s₂<VAR>h₁ : s₁.Nonempty<GOAL>s₂.inf' ⋯ f ≤ s₁.inf' h₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>f : β → α<VAR>s₁ s₂ : Finset β<VAR>h : s₁ ⊆ s₂<VAR>h₁ : s₁.Nonempty<VAR>h₂ : s₂.Nonempty<GOAL>s₂.inf' h₂ f ≤ s₁.inf' h₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<GOAL>s.sup' H f = s.sup f