ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type v<VAR>C : G.Coloring α<GOAL>C.toPartition.parts = C.colorClasses
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>default = G.selfColoring.toPartition
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<GOAL>G.Partitionable n ↔ G.Colorable n
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<GOAL>{c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}.Nonempty
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>S : Set α<VAR>h : ∀ (a : α), ∃ b ∈ S, r a b<GOAL>Order.cof r ≤ #↑S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>c : Cardinal.{u_1}<GOAL>c ≤ Order.cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl β s<VAR>f : r ≃r s<GOAL>Cardinal.lift.{max u v, u} (Order.cof r) ≤ Cardinal.lift.{max u v, v} (Order.cof s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl α r<VAR>IsRefl β s<VAR>f : r ≃r s<GOAL>Cardinal.lift.{max u v, u} (Order.cof r) = Cardinal.lift.{max u v, v} (Order.cof s)
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl β s<VAR>f : r ≃r s<GOAL>Order.cof r ≤ Order.cof s
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl α r<VAR>IsRefl β s<VAR>f : r ≃r s<GOAL>Order.cof r = Order.cof s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsIrrefl α r<GOAL>{c | ∃ S, Set.Unbounded r S ∧ #↑S = c}.Nonempty
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>(Ordinal.type r).cof = StrictOrder.cof r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>c : Cardinal.{u_1}<GOAL>c ≤ (Ordinal.type r).cof ↔ ∀ (S : Set α), Set.Unbounded r S → c ≤ #↑S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>S : Set α<VAR>h : Set.Unbounded r S<GOAL>(Ordinal.type r).cof ≤ #↑S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>S : Set α<GOAL>#↑S < (Ordinal.type r).cof → Set.Bounded r S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>∃ S, Set.Unbounded r S ∧ #↑S = (Ordinal.type r).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>∃ S, Set.Unbounded r S ∧ Ordinal.type (Subrel r S) = (Ordinal.type r).cof.ord
<VAR>o : Ordinal.{u}<GOAL>∃ ι f, Ordinal.lsub f = o ∧ #ι = o.card
<VAR>o : Ordinal.{u}<GOAL>{a | ∃ ι f, Ordinal.lsub f = o ∧ #ι = a}.Nonempty
<VAR>o : Ordinal.{u}<GOAL>o.cof = sInf {a | ∃ ι f, Ordinal.lsub f = o ∧ #ι = a}
<VAR>o : Ordinal.{v}<GOAL>Cardinal.lift.{u, v} o.cof = (Ordinal.lift.{u, v} o).cof
<VAR>o : Ordinal.{u_2}<GOAL>o.cof ≤ o.card
<VAR>c : Cardinal.{u_2}<GOAL>c.ord.cof ≤ c
<VAR>o : Ordinal.{u}<GOAL>o.cof.ord ≤ o
<VAR>o : Ordinal.{u}<GOAL>∃ ι f, Ordinal.lsub f = o ∧ #ι = o.cof
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<GOAL>(Ordinal.lsub f).cof ≤ #ι
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.lsub f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>o : Ordinal.{u}<VAR>a : Cardinal.{u}<GOAL>a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), Ordinal.lsub f = o → a ≤ #ι
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), f i < c<GOAL>Ordinal.lsub f < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hι : #ι < c.cof<GOAL>(∀ (i : ι), f i < c) → Ordinal.lsub f < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>H : ∀ (i : ι), f i < Ordinal.sup f<GOAL>(Ordinal.sup f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>H : ∀ (i : ι), f i < Ordinal.sup f<GOAL>(Ordinal.sup f).cof ≤ #ι
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), f i < c<GOAL>Ordinal.sup f < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hι : #ι < c.cof<GOAL>(∀ (i : ι), f i < c) → Ordinal.sup f < c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.ord.cof<VAR>hf : ∀ (i : ι), f i < c<GOAL>iSup f < c
<VAR>ι : Type u_2<VAR>f : ι → Cardinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hι : #ι < c.ord.cof<GOAL>(∀ (i : ι), f i < c) → iSup f < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{max u v}<VAR>ha : a < c<GOAL>Ordinal.nfpFamily f a < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{u}<GOAL>a < c → Ordinal.nfpFamily f a < c
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c<VAR>a : Ordinal.{max u v}<GOAL>a < c → o.nfpBFamily f a < c
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c<VAR>a : Ordinal.{u}<GOAL>a < c → o.nfpBFamily f a < c
<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>c : Ordinal.{u_2}<VAR>hc : ℵ₀ < c.cof<VAR>hf : ∀ i < c, f i < c<VAR>a : Ordinal.{u_2}<GOAL>a < c → Ordinal.nfp f a < c
<VAR>o : Ordinal.{u}<GOAL>∃ f, o.cof.ord.blsub f = o
<VAR>b : Ordinal.{u}<VAR>a : Cardinal.{u}<GOAL>a ≤ b.cof ↔ ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>(o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(o.blsub f).cof ≤ o.card
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>ho : Cardinal.lift.{v, u} o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c<GOAL>o.blsub f < c
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>ho : o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c<GOAL>o.blsub f < c
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f<GOAL>(o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>ho : Cardinal.lift.{v, u} o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c<GOAL>o.bsup f < c
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>ho : o.card < c.cof<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.bsup f < c
<VAR>o : Ordinal.{u_2}<GOAL>o.cof = 0 ↔ o = 0
<VAR>o : Ordinal.{u_2}<GOAL>o.cof ≠ 0 ↔ o ≠ 0
<VAR>o : Ordinal.{u_2}<GOAL>(Order.succ o).cof = 1
<VAR>o : Ordinal.{u}<GOAL>o.cof = 1 ↔ ∃ a, o = Order.succ a
<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>a.cof.ord = o
<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i j : Ordinal.{u}<VAR>hi : i < o<VAR>hj : j < o<GOAL>i < j → f i hi < f j hj
<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>o.blsub f = a
<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯
<VAR>o : Ordinal.{u}<VAR>h : o ≤ o.cof.ord<GOAL>o.IsFundamentalSequence o fun a x => a
<VAR>f : (b : Ordinal.{u_2}) → b < 0 → Ordinal.{u_2}<GOAL>Ordinal.IsFundamentalSequence 0 0 f
<VAR>o : Ordinal.{u}<GOAL>(Order.succ o).IsFundamentalSequence 1 fun x x => o
<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i j : Ordinal.{u}<VAR>hi : i < o<VAR>hj : j < o<VAR>hij : i ≤ j<GOAL>f i hi ≤ f j hj
<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<GOAL>a.IsFundamentalSequence o' fun i hi => f (g i hi) ⋯
<VAR>a : Ordinal.{u}<GOAL>∃ f, a.IsFundamentalSequence a.cof.ord f
<VAR>a : Ordinal.{u}<GOAL>a.cof.ord.cof = a.cof
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : Ordinal.IsNormal f<VAR>a o : Ordinal.{u}<VAR>ha : a.IsLimit<VAR>g : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hg : a.IsFundamentalSequence o g<GOAL>(f a).IsFundamentalSequence o fun b hb => f (g b hb)
<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : Ordinal.IsNormal f<VAR>a : Ordinal.{u_2}<VAR>ha : a.IsLimit<GOAL>(f a).cof = a.cof
<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : Ordinal.IsNormal f<VAR>a : Ordinal.{u_2}<GOAL>a.cof ≤ (f a).cof
<VAR>a b : Ordinal.{u_2}<GOAL>b ≠ 0 → (a + b).cof = b.cof
<VAR>o : Ordinal.{u_2}<GOAL>ℵ₀ ≤ o.cof ↔ o.IsLimit
<VAR>o : Ordinal.{u_2}<VAR>ho : o.IsLimit<GOAL>(Cardinal.aleph' o).ord.cof = o.cof
<VAR>o : Ordinal.{u_2}<VAR>ho : o.IsLimit<GOAL>(Cardinal.aleph o).ord.cof = o.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>h : (Ordinal.type r).IsLimit<GOAL>∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = (Ordinal.type r).cof
<GOAL>Ordinal.univ.{u, v}.cof = Cardinal.univ.{u, v}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Set.Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<GOAL>∃ x ∈ s, Set.Unbounded r x
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : β → Set α<VAR>h₁ : Set.Unbounded r (⋃ x, s x)<VAR>h₂ : #β < StrictOrder.cof r<GOAL>∃ x, Set.Unbounded r (s x)
<VAR>β α : Type u<VAR>f : β → α<VAR>h₁ : ℵ₀ ≤ #β<VAR>h₂ : #α < (#β).ord.cof<GOAL>∃ a, #↑(f ⁻¹' {a}) = #β
<VAR>β α : Type u<VAR>f : β → α<VAR>θ : Cardinal.{u}<VAR>hθ : θ ≤ #β<VAR>h₁ : ℵ₀ ≤ θ<VAR>h₂ : #α < θ.ord.cof<GOAL>∃ a, θ ≤ #↑(f ⁻¹' {a})
<VAR>β α : Type u<VAR>s : Set β<VAR>f : ↑s → α<VAR>θ : Cardinal.{u}<VAR>hθ : θ ≤ #↑s<VAR>h₁ : ℵ₀ ≤ θ<VAR>h₂ : #α < θ.ord.cof<GOAL>∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a
<VAR>c : Cardinal.{u_2}<VAR>h : c.IsStrongLimit<GOAL>c ≠ 0
<VAR>x c : Cardinal.{u_2}<VAR>h : c.IsStrongLimit<GOAL>x < c → 2 ^ x < c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsStrongLimit<GOAL>Order.IsSuccLimit c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsStrongLimit<GOAL>c.IsLimit
<VAR>o : Ordinal.{u_2}<VAR>H : Order.IsSuccLimit o<GOAL>(Cardinal.beth o).IsStrongLimit
<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>hr : (#α).ord = Ordinal.type r<GOAL>#{ s // Set.Bounded r s } = #α
<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>ℵ₀ ≤ c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>c.ord.cof = c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>0 < c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<VAR>n : ℕ<GOAL>↑n < c
<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>0 < c.ord
<VAR>o : Ordinal.{u_2}<VAR>h : o.IsLimit<GOAL>o.cof.IsRegular
<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<GOAL>(Order.succ c).IsRegular
<VAR>o : Ordinal.{u_2}<VAR>h : ω ≤ o<GOAL>(Cardinal.aleph' (Order.succ o)).IsRegular
<VAR>o : Ordinal.{u_2}<GOAL>(Cardinal.aleph (Order.succ o)).IsRegular
<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : ℵ₀ ≤ #α<GOAL>∃ a, #α < #↑(f ⁻¹' {a})
<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : Infinite α<GOAL>∃ a, Infinite ↑(f ⁻¹' {a})
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<GOAL>#β ≤ #↑(Set.range f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<GOAL>(∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord
<VAR>ι : Type (max u_2 u_3)<VAR>f : ι → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>(∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<GOAL>(∀ (i : ι), f i < c.ord) → Ordinal.sup f < c.ord
<VAR>ι : Type (max u_2 u_3)<VAR>f : ι → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>(∀ (i : ι), f i < c.ord) → Ordinal.sup f < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>ho : Cardinal.lift.{v, u} o.card < c<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord
<VAR>o : Ordinal.{max u_2 u_3}<VAR>f : (a : Ordinal.{max u_2 u_3}) → a < o → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>ho : o.card < c<GOAL>(∀ (i : Ordinal.{max u_2 u_3}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} o.card < c<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
<VAR>o : Ordinal.{max u_2 u_3}<VAR>f : (a : Ordinal.{max u_2 u_3}) → a < o → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>hι : o.card < c<GOAL>(∀ (i : Ordinal.{max u_2 u_3}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<GOAL>(∀ (i : ι), f i < c) → iSup f < c
<VAR>ι : Type u_2<VAR>f : ι → Cardinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>(∀ (i : ι), f i < c) → iSup f < c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<VAR>hf : ∀ (i : ι), f i < c<GOAL>Cardinal.sum f < c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>(∀ (i : ι), f i < c) → Cardinal.sum f < c
<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>h : #↑(⋃ i, t i) < c<VAR>i : ι<GOAL>#↑(t i) < c
<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>#↑(⋃ i, t i) < c ↔ ∀ (i : ι), #↑(t i) < c
<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c<VAR>a : α<VAR>ha : a ∈ s<GOAL>#↑(t a ha) < c
<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hs : #↑s < c<GOAL>#↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<VAR>ha : a < c.ord<GOAL>Ordinal.nfpFamily f a < c.ord
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>a : Ordinal.{u}<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<GOAL>a < c.ord → Ordinal.nfpFamily f a < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>ho : Cardinal.lift.{v, u} o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>a < c.ord → o.nfpBFamily f a < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>ho : o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{u}<GOAL>a < c.ord → o.nfpBFamily f a < c.ord
<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hc : c.IsRegular<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ i < c.ord, f i < c.ord<VAR>a : Ordinal.{u_2}<GOAL>a < c.ord → Ordinal.nfp f a < c.ord
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>a < c.ord → Ordinal.derivFamily f a < c.ord
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{u}<GOAL>a < c.ord → Ordinal.derivFamily f a < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : Cardinal.lift.{v, u} o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>a < c.ord → o.derivBFamily f a < c.ord
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{u}<GOAL>a < c.ord → o.derivBFamily f a < c.ord
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ i < c.ord, f i < c.ord<VAR>a : Ordinal.{u}<GOAL>a < c.ord → Ordinal.deriv f a < c.ord
<VAR>c : Cardinal.{u_2}<VAR>h₁ : ℵ₀ < c<VAR>h₂ : c ≤ c.ord.cof<VAR>h₃ : ∀ x < c, 2 ^ x < c<GOAL>c.IsInaccessible
<VAR>c : Cardinal.{u}<GOAL>ℵ₀ ≤ c → c < c ^ c.ord.cof
<VAR>a b : Cardinal.{u_2}<VAR>ha : ℵ₀ ≤ a<VAR>b1 : 1 < b<GOAL>a < (b ^ a).ord.cof
<VAR>α : Type u_2<VAR>Countable α<VAR>o : α → Ordinal.{max u_3 u_2}<VAR>ho : ∀ (n : α), o n < (Cardinal.aleph 1).ord<GOAL>Ordinal.sup o < (Cardinal.aleph 1).ord
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>∅.shadow = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>k : ℕ<GOAL>Finset.shadow^[k] ∅ = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>{∅}.shadow = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Monotone Finset.shadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<VAR>ha : a ∈ s<GOAL>s.erase a ∈ 𝒜.shadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.shadow ↔ ∃ a ∉ t, insert a t ∈ 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ u, u.card = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + k
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>Set.Sized (r - 1) ↑𝒜.shadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>Set.Sized (r - k) ↑(Finset.shadow^[k] 𝒜)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h : ∅ ∉ 𝒜<GOAL>Set.Sized r ↑𝒜.shadow ↔ Set.Sized (r + 1) ↑𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>hs : t ∈ 𝒜.shadow<GOAL>∃ s ∈ 𝒜, t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>∅.upShadow = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Monotone Finset.upShadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<VAR>ha : a ∉ s<GOAL>insert a s ∈ 𝒜.upShadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.upShadow ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ u, u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = k
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>k : ℕ<GOAL>t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + k
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>Set.Sized (r + 1) ↑𝒜.upShadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hs : s ∈ 𝒜.upShadow<GOAL>∃ t ∈ 𝒜, t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>k : ℕ<GOAL>s ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ t.card + k = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.compls.shadow = 𝒜.upShadow.compls
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.compls.upShadow = 𝒜.shadow.compls
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Zero R<VAR>One R<VAR>a : α<VAR>e : Sym2 α<GOAL>SimpleGraph.incMatrix R G a e = (G.incidenceSet a).indicator 1 e
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Zero R<VAR>One R<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>a : α<VAR>e : Sym2 α<GOAL>SimpleGraph.incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<GOAL>SimpleGraph.incMatrix R G a e * SimpleGraph.incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>hab : a ≠ b<VAR>h : ¬G.Adj a b<GOAL>SimpleGraph.incMatrix R G a e * SimpleGraph.incMatrix R G b e = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a : α<VAR>e : Sym2 α<VAR>h : e ∉ G.incidenceSet a<GOAL>SimpleGraph.incMatrix R G a e = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a : α<VAR>e : Sym2 α<VAR>h : e ∈ G.incidenceSet a<GOAL>SimpleGraph.incMatrix R G a e = 1
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a : α<VAR>e : Sym2 α<VAR>Nontrivial R<GOAL>SimpleGraph.incMatrix R G a e = 0 ↔ e ∉ G.incidenceSet a
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>MulZeroOneClass R<VAR>a : α<VAR>e : Sym2 α<VAR>Nontrivial R<GOAL>SimpleGraph.incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype (Sym2 α)<VAR>NonAssocSemiring R<VAR>a : α<VAR>Fintype ↑(G.neighborSet a)<GOAL>∑ e : Sym2 α, SimpleGraph.incMatrix R G a e = ↑(G.degree a)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype (Sym2 α)<VAR>NonAssocSemiring R<VAR>a : α<VAR>Fintype ↑(G.neighborSet a)<GOAL>(SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G)ᵀ) a a = ↑(G.degree a)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>NonAssocSemiring R<VAR>e : Sym2 α<VAR>Fintype α<GOAL>e ∈ G.edgeSet → ∑ a : α, SimpleGraph.incMatrix R G a e = 2
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>NonAssocSemiring R<VAR>e : Sym2 α<VAR>Fintype α<VAR>h : e ∉ G.edgeSet<GOAL>∑ a : α, SimpleGraph.incMatrix R G a e = 0