ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>h : s.Nonempty<VAR>f : β → α<GOAL>↑(s.sup f) = s.sup (WithBot.some ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<GOAL>s.inf' H f = s.inf f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Finset β<VAR>h : s.Nonempty<VAR>f : β → α<GOAL>↑(s.inf f) = s.inf (WithTop.some ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>C : β → Type u_7<VAR>(b : β) → SemilatticeSup (C b)<VAR>(b : β) → OrderBot (C b)<VAR>s : Finset α<VAR>f : α → (b : β) → C b<VAR>b : β<GOAL>s.sup f b = s.sup fun a => f a b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>C : β → Type u_7<VAR>(b : β) → SemilatticeInf (C b)<VAR>(b : β) → OrderTop (C b)<VAR>s : Finset α<VAR>f : α → (b : β) → C b<VAR>b : β<GOAL>s.inf f b = s.inf fun a => f a b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>C : β → Type u_7<VAR>(b : β) → SemilatticeSup (C b)<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>f : α → (b : β) → C b<VAR>b : β<GOAL>s.sup' H f b = s.sup' H fun a => f a b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>C : β → Type u_7<VAR>(b : β) → SemilatticeInf (C b)<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>f : α → (b : β) → C b<VAR>b : β<GOAL>s.inf' H f b = s.inf' H fun a => f a b
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>SemilatticeSup α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<GOAL>OrderDual.toDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.toDual ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>SemilatticeInf α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<GOAL>OrderDual.toDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.toDual ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>SemilatticeInf α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → αᵒᵈ<GOAL>OrderDual.ofDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.ofDual ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>SemilatticeSup α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → αᵒᵈ<GOAL>OrderDual.ofDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.ofDual ∘ f)
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a ⊓ s.sup' hs f = s.sup' hs fun i => a ⊓ f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DistribLattice α<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' ⋯ fun i => f i.1 ⊓ g i.2
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a ⊔ s.inf' hs f = s.inf' hs fun i => a ⊔ f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>DistribLattice α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.inf' hs f ⊔ a = s.inf' hs fun i => f i ⊔ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DistribLattice α<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' ⋯ fun i => f i.1 ⊔ g i.2
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a < s.sup' H f ↔ ∃ b ∈ s, a < f b
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.sup' H f < a ↔ ∀ i ∈ s, f i < a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.inf' H f ≤ a ↔ ∃ i ∈ s, f i ≤ a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.inf' H f < a ↔ ∃ i ∈ s, f i < a
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a < s.inf' H f ↔ ∀ i ∈ s, a < f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<GOAL>∃ i ∈ s, s.sup' H f = f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<GOAL>∃ i ∈ s, s.inf' H f = f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset ι<VAR>h : s.Nonempty<VAR>f : ι → α<GOAL>∃ i ∈ s, s.sup f = f i
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset ι<VAR>h : s.Nonempty<VAR>f : ι → α<GOAL>∃ i ∈ s, s.inf f = f i
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.max = s.sup WithBot.some
<VAR>α : Type u_2<VAR>LinearOrder α<GOAL>∅.max = ⊥
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).max = max (↑a) s.max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>{a}.max = ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, s.max = ↑b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∃ a, s.max = ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.max = ⊥ ↔ s = ∅
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a : α<GOAL>s.max = ↑a → a ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>as : a ∈ s<GOAL>↑a ≤ s.max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>h : s.max < ↑a<GOAL>a ∉ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a b : α<VAR>h₁ : a ∈ s<VAR>h₂ : s.max = ↑b<GOAL>a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a b : α<VAR>h₁ : b < a<VAR>h₂ : s.max = ↑b<GOAL>a ∉ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>st : s ⊆ t<GOAL>s.max ≤ t.max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>M : WithBot α<VAR>s : Finset α<VAR>st : ∀ a ∈ s, ↑a ≤ M<GOAL>s.max ≤ M
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>m : WithBot α<VAR>s : Finset α<GOAL>s.max ≤ m ↔ ∀ a ∈ s, ↑a ≤ m
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>OrderTop α<VAR>s : Finset α<GOAL>s.max = ⊤ ↔ ⊤ ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.min = s.inf WithTop.some
<VAR>α : Type u_2<VAR>LinearOrder α<GOAL>∅.min = ⊤
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).min = min (↑a) s.min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>{a}.min = ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, s.min = ↑b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∃ a, s.min = ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.min = ⊤ ↔ s = ∅
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a : α<GOAL>s.min = ↑a → a ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>as : a ∈ s<GOAL>s.min ≤ ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>h : ↑a < s.min<GOAL>a ∉ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a b : α<VAR>h₁ : b ∈ s<VAR>h₂ : s.min = ↑a<GOAL>a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>a b : α<VAR>h₁ : a < b<VAR>h₂ : s.min = ↑b<GOAL>a ∉ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>st : s ⊆ t<GOAL>t.min ≤ s.min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>m : WithTop α<VAR>s : Finset α<VAR>st : ∀ a ∈ s, m ≤ ↑a<GOAL>m ≤ s.min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>m : WithTop α<VAR>s : Finset α<GOAL>m ≤ s.min ↔ ∀ a ∈ s, m ≤ ↑a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>OrderBot α<VAR>s : Finset α<GOAL>s.min = ⊥ ↔ ⊥ ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>s.min' H ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>x : α<VAR>H2 : x ∈ s<GOAL>s.min' ⋯ ≤ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<VAR>H2 : ∀ y ∈ s, x ≤ y<GOAL>x ≤ s.min' H
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsLeast (↑s) (s.min' H)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>{a}.min' ⋯ = a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>s.max' H ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>x : α<VAR>H2 : x ∈ s<GOAL>x ≤ s.max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<VAR>H2 : ∀ y ∈ s, y ≤ x<GOAL>s.max' H ≤ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsGreatest (↑s) (s.max' H)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.max' H < x ↔ ∀ y ∈ s, y < x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>x < s.min' H ↔ ∀ y ∈ s, x < y
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>s.max' H = s.sup' H id
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>s.min' H = s.inf' H id
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>{a}.max' ⋯ = a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>i j : α<VAR>H1 : i ∈ s<VAR>H2 : j ∈ s<VAR>H3 : i ≠ j<GOAL>s.min' ⋯ < s.max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>h₂ : 1 < s.card<GOAL>s.min' ⋯ < s.max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset αᵒᵈ<GOAL>WithTop.map (⇑OrderDual.ofDual) s.min = (Finset.image (⇑OrderDual.ofDual) s).max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset αᵒᵈ<GOAL>WithBot.map (⇑OrderDual.ofDual) s.max = (Finset.image (⇑OrderDual.ofDual) s).min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>WithTop.map (⇑OrderDual.toDual) s.min = (Finset.image (⇑OrderDual.toDual) s).max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>WithBot.map (⇑OrderDual.toDual) s.max = (Finset.image (⇑OrderDual.toDual) s).min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>OrderDual.ofDual (s.min' hs) = (Finset.image (⇑OrderDual.ofDual) s).max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>OrderDual.ofDual (s.max' hs) = (Finset.image (⇑OrderDual.ofDual) s).min' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>OrderDual.toDual (s.min' hs) = (Finset.image (⇑OrderDual.toDual) s).max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>OrderDual.toDual (s.max' hs) = (Finset.image (⇑OrderDual.toDual) s).min' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>H : s.Nonempty<VAR>hst : s ⊆ t<GOAL>s.max' H ≤ t.max' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>H : s.Nonempty<VAR>hst : s ⊆ t<GOAL>t.min' ⋯ ≤ s.min' H
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>(insert a s).max' ⋯ = max (s.max' H) a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>(insert a s).min' ⋯ = min (s.min' H) a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>DecidableEq α<VAR>a : α<VAR>ha : a ∈ s.erase (s.max' H)<GOAL>a < s.max' H
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>DecidableEq α<VAR>a : α<VAR>ha : a ∈ s.erase (s.min' H)<GOAL>s.min' H < a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : (Finset.image f s).Nonempty<GOAL>(Finset.image f s).max' h = f (s.max' ⋯)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>f (s.max' h) = (Finset.image f s).max' ⋯
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : (Finset.image f s).Nonempty<GOAL>(Finset.image f s).min' h = f (s.min' ⋯)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>f (s.min' h) = (Finset.image f s).min' ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>↑(s.max' hs) = s.max
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>↑(s.min' hs) = s.min
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.max ∈ Finset.image WithBot.some s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.min ∈ Finset.image WithTop.some s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.max ∈ insert ⊥ (Finset.image WithBot.some s)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Finset α<GOAL>s.min ∈ insert ⊤ (Finset.image WithTop.some s)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<VAR>s0 : (s.erase x).Nonempty<GOAL>(s.erase x).max' s0 ≠ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<VAR>s0 : (s.erase x).Nonempty<GOAL>(s.erase x).min' s0 ≠ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<GOAL>(s.erase x).max ≠ ↑x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<GOAL>(s.erase x).min ≠ ↑x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<VAR>h : ∃ y ∈ s, x < y<GOAL>∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x : α<VAR>s : Finset α<VAR>h : ∃ y ∈ s, y < x<GOAL>∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y<GOAL>s.card ≤ t.card + 1
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y<GOAL>s.card ≤ (t \ s).card + 1
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DecidableEq α<VAR>p : Finset α → Prop<VAR>s : Finset α<VAR>h0 : p ∅<VAR>step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)<GOAL>p s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DecidableEq α<VAR>p : Finset α → Prop<VAR>s : Finset α<VAR>h0 : p ∅<VAR>step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → p s → p (insert a s)<GOAL>p s
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>DecidableEq ι<VAR>f : ι → α<VAR>p : Finset ι → Prop<VAR>s : Finset ι<VAR>h0 : p ∅<VAR>step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)<GOAL>p s
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>LinearOrder α<VAR>DecidableEq ι<VAR>f : ι → α<VAR>p : Finset ι → Prop<VAR>s : Finset ι<VAR>h0 : p ∅<VAR>step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)<GOAL>p s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>s : Finset β<VAR>f : β → α<VAR>h : s.Nonempty<GOAL>∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>s : Finset β<VAR>f : β → α<VAR>h : s.Nonempty<GOAL>∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>IsGLB (↑s) i ↔ IsLeast (↑s) i
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>IsLUB (↑s) i ↔ IsGreatest (↑s) i
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>his : IsGLB (↑s) i<VAR>hs : s.Nonempty<GOAL>i ∈ s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>his : IsLUB (↑s) i<VAR>hs : s.Nonempty<GOAL>i ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → Multiset β<VAR>g : β → α<VAR>hg : Function.Injective g<GOAL>Multiset.map g (s.sup f) = s.sup (Multiset.map g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>b : β<GOAL>Multiset.count b (s.sup f) = s.sup fun a => Multiset.count b (f a)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>x : β<GOAL>x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>x : β<GOAL>x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<GOAL>s.sup t = s.biUnion t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>s : Finset β<VAR>f : β → α<GOAL>(s.sup fun b => {f b}) = Finset.image f s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.sup singleton = s
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>CompleteLattice α<VAR>s : ι → α<GOAL>⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i
<VAR>α : Type u_2<VAR>ι' : Sort u_7<VAR>CompleteLattice α<VAR>s : ι' → α<GOAL>⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>CompleteLattice α<VAR>s : ι → α<GOAL>⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i
<VAR>α : Type u_2<VAR>ι' : Sort u_7<VAR>CompleteLattice α<VAR>s : ι' → α<GOAL>⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i.down
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>s : ι → Set α<GOAL>⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i
<VAR>α : Type u_2<VAR>ι' : Sort u_7<VAR>s : ι' → Set α<GOAL>⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i.down
<VAR>α : Type u_2<VAR>ι : Type u_5<VAR>s : ι → Set α<GOAL>⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i
<VAR>α : Type u_2<VAR>ι' : Sort u_7<VAR>s : ι' → Set α<GOAL>⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i.down
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s<GOAL>s ∈ maximals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t<GOAL>s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet β<VAR>f : α → β<VAR>s : Finset α<GOAL>⨆ x ∈ ↑s, f x = ⨆ x ∈ s, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet β<VAR>f : α → β<VAR>s : Finset α<GOAL>⨅ x ∈ ↑s, f x = ⨅ x ∈ s, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>a : α<VAR>s : α → β<GOAL>⨆ x ∈ {a}, s x = s a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>a : α<VAR>s : α → β<GOAL>⨅ x ∈ {a}, s x = s a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>o : Option α<VAR>f : α → β<GOAL>⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>o : Option α<VAR>f : α → β<GOAL>⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<GOAL>⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<GOAL>⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → β<GOAL>⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → β<GOAL>⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>f : γ → α<VAR>g : α → β<VAR>s : Finset γ<GOAL>⨆ x ∈ Finset.image f s, g x = ⨆ y ∈ s, g (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>f : γ → α<VAR>g : α → β<VAR>s : Finset γ<GOAL>⨅ x ∈ Finset.image f s, g x = ⨅ y ∈ s, g (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<GOAL>⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<GOAL>⨅ i ∈ insert x t, Function.update f x s i = s ⊓ ⨅ i ∈ t, f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>f : α → β<GOAL>⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>f : α → β<GOAL>⨅ y ∈ s.biUnion t, f y = ⨅ x ∈ s, ⨅ y ∈ t x, f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Finset α<VAR>t : α → Set β<GOAL>⋃ x ∈ ↑s, t x = ⋃ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Finset α<VAR>t : α → Set β<GOAL>⋂ x ∈ ↑s, t x = ⋂ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>a : α<VAR>s : α → Set β<GOAL>⋃ x ∈ {a}, s x = s a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>a : α<VAR>s : α → Set β<GOAL>⋂ x ∈ {a}, s x = s a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>s : Finset β<GOAL>⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>o : Option α<VAR>f : α → Set β<GOAL>⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>o : Option α<VAR>f : α → Set β<GOAL>⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Finset α<VAR>f : α → Set β<VAR>x : α<VAR>h : x ∈ s<GOAL>f x ⊆ ⋃ y ∈ s, f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>s t : Finset α<VAR>u : α → Set β<GOAL>⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>s t : Finset α<VAR>u : α → Set β<GOAL>⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → Set β<GOAL>⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → Set β<GOAL>⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq α<VAR>f : γ → α<VAR>g : α → Set β<VAR>s : Finset γ<GOAL>⋃ x ∈ Finset.image f s, g x = ⋃ y ∈ s, g (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq α<VAR>f : γ → α<VAR>g : α → Set β<VAR>s : Finset γ<GOAL>⋂ x ∈ Finset.image f s, g x = ⋂ y ∈ s, g (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → Set β<VAR>s : Set β<VAR>hx : x ∉ t<GOAL>⋃ i ∈ insert x t, Function.update f x s i = s ∪ ⋃ i ∈ t, f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → Set β<VAR>s : Set β<VAR>hx : x ∉ t<GOAL>⋂ i ∈ insert x t, Function.update f x s i = s ∩ ⋂ i ∈ t, f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>f : α → Set β<GOAL>⋃ y ∈ s.biUnion t, f y = ⋃ x ∈ s, ⋃ y ∈ t x, f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>f : α → Set β<GOAL>⋂ y ∈ s.biUnion t, f y = ⋂ x ∈ s, ⋂ y ∈ t x, f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>I : Set α<VAR>N : Matroid β<GOAL>(N.comap f).Indep I ↔ N.Indep (f '' I) ∧ Set.InjOn f I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>N : Matroid β<VAR>f : α → β<GOAL>(N.comap f).E = f ⁻¹' N.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>I : Set α<VAR>N : Matroid β<GOAL>(N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬Set.InjOn f I
<VAR>β : Type u_2<VAR>N : Matroid β<GOAL>N.comap id = N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>I : Set α<VAR>N : Matroid β<VAR>hf : Set.InjOn f (f ⁻¹' N.E)<GOAL>(N.comap f).Indep I ↔ N.Indep (f '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(Matroid.emptyOn β).comap f = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E : Set β<GOAL>(Matroid.loopyOn E).comap f = Matroid.loopyOn (f ⁻¹' E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>I X : Set α<GOAL>(N.comap f).Basis I X ↔ N.Basis (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>B : Set α<GOAL>(N.comap f).Base B ↔ N.Basis (f '' B) (f '' (f ⁻¹' N.E)) ∧ Set.InjOn f B ∧ B ⊆ f ⁻¹' N.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>I X : Set α<GOAL>(N.comap f).Basis' I X ↔ N.Basis' (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>N : Matroid β<VAR>f : α → β<GOAL>N.comapOn (f ⁻¹' N.E) f = N.comap f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E I : Set α<GOAL>(N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ Set.InjOn f I ∧ I ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E : Set α<GOAL>(N.comapOn E f).E = E