ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>h : r ↪r s<GOAL>Ordinal.type r ≤ Ordinal.type s
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.type r < Ordinal.type s ↔ Nonempty (r ≺i s)
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>h : r ≺i s<GOAL>Ordinal.type r < Ordinal.type s
<VAR>o : Ordinal.{u_3}<GOAL>0 ≤ o
<VAR>o : Ordinal.{u_3}<GOAL>o ≤ 0 ↔ o = 0
<VAR>o : Ordinal.{u_3}<GOAL>0 < o ↔ o ≠ 0
<VAR>o : Ordinal.{u_3}<GOAL>¬o < 0
<VAR>a : Ordinal.{u_3}<GOAL>a = 0 ∨ 0 < a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>a : α<GOAL>Ordinal.typein r a < Ordinal.type r
<VAR>o : Ordinal.{u_3}<VAR>i : (Quotient.out o).α<GOAL>Ordinal.typein (fun x x_1 => x < x_1) i < o
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≺i s<GOAL>Ordinal.typein s f.top = Ordinal.type r
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≼i s<VAR>a : α<GOAL>Ordinal.typein s (f a) = Ordinal.typein r a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>a b : α<GOAL>Ordinal.typein r a < Ordinal.typein r b ↔ r a b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>o : Ordinal.{u}<VAR>h : o < Ordinal.type r<GOAL>∃ a, Ordinal.typein r a = o
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>Function.Injective (Ordinal.typein r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>a b : α<GOAL>Ordinal.typein r a = Ordinal.typein r b ↔ a = b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>⇑(Ordinal.typein.principalSeg r).toRelEmbedding = Ordinal.typein r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>o : Ordinal.{u}<VAR>h : o < Ordinal.type r<GOAL>Ordinal.typein r (Ordinal.enum r o h) = o
<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : s ≺i r<VAR>h : Ordinal.type s < Ordinal.type r<GOAL>Ordinal.enum r (Ordinal.type s) h = f.top
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>a : α<GOAL>Ordinal.enum r (Ordinal.typein r a) ⋯ = a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>o₁ o₂ : Ordinal.{u}<VAR>h₁ : o₁ < Ordinal.type r<VAR>h₂ : o₂ < Ordinal.type r<GOAL>r (Ordinal.enum r o₁ h₁) (Ordinal.enum r o₂ h₂) ↔ o₁ < o₂
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>hr : o < Ordinal.type r<VAR>hs : o < Ordinal.type s<GOAL>f (Ordinal.enum r o hr) = Ordinal.enum s o hs
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>hr : o < Ordinal.type r<GOAL>f (Ordinal.enum r o hr) = Ordinal.enum s o ⋯
<VAR>p : Ordinal.{u} → Prop<VAR>i : Ordinal.{u}<VAR>h : ∀ (j : Ordinal.{u}), (∀ k < j, p k) → p j<GOAL>p i
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>(Ordinal.type r).card = #α
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>x : α<GOAL>#{ y // r y x } = (Ordinal.typein r x).card
<VAR>o₁ o₂ : Ordinal.{u_3}<GOAL>o₁ ≤ o₂ → o₁.card ≤ o₂.card
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>Ordinal.type (ULift.down ⁻¹'o r) = Ordinal.lift.{v, u} (Ordinal.type r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>(Ordinal.type fun x y => r x.down y.down) = Ordinal.lift.{v, u} (Ordinal.type r)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≃r s<GOAL>Ordinal.lift.{v, u} (Ordinal.type r) = Ordinal.lift.{u, v} (Ordinal.type s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : β ≃ α<GOAL>Ordinal.lift.{u, v} (Ordinal.type (⇑f ⁻¹'o r)) = Ordinal.lift.{v, u} (Ordinal.type r)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : β ≃ α<GOAL>Ordinal.lift.{u, v} (Ordinal.type fun x y => r (f x) (f y)) = Ordinal.lift.{v, u} (Ordinal.type r)
<GOAL>Ordinal.lift.{max u v, u} = Ordinal.lift.{v, u}
<GOAL>Ordinal.lift.{max v u, u} = Ordinal.lift.{v, u}
<VAR>a : Ordinal.{max u_3 u_4}<GOAL>Ordinal.lift.{u_3, max u_3 u_4} a = a
<VAR>a : Ordinal.{u}<GOAL>Ordinal.lift.{u, u} a = a
<VAR>a : Ordinal.{u}<GOAL>Ordinal.lift.{0, u} a = a
<VAR>a : Ordinal.{u_3}<GOAL>Ordinal.lift.{w, max v u_3} (Ordinal.lift.{v, u_3} a) = Ordinal.lift.{max v w, u_3} a
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.lift.{max v w, u} (Ordinal.type r) ≤ Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≼i s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.lift.{max v w, u} (Ordinal.type r) = Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≃r s)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.lift.{max v w, u} (Ordinal.type r) < Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≺i s)
<VAR>a b : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} a ≤ Ordinal.lift.{u, v} b ↔ a ≤ b
<VAR>a b : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} a = Ordinal.lift.{u, v} b ↔ a = b
<VAR>a b : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} b ↔ a < b
<GOAL>Ordinal.lift.{u_4, u_3} 0 = 0
<GOAL>Ordinal.lift.{u_4, u_3} 1 = 1
<VAR>a : Ordinal.{v}<GOAL>Cardinal.lift.{u, v} a.card = (Ordinal.lift.{u, v} a).card
<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<GOAL>∃ a', Ordinal.lift.{v, u} a' = b
<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b ≤ Ordinal.lift.{v, u} a<GOAL>∃ a', Ordinal.lift.{v, u} a' = b
<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{max u v}<GOAL>b ≤ Ordinal.lift.{v, u} a ↔ ∃ a', Ordinal.lift.{v, u} a' = b ∧ a' ≤ a
<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{max u v}<GOAL>b < Ordinal.lift.{v, u} a ↔ ∃ a', Ordinal.lift.{v, u} a' = b ∧ a' < a
<GOAL>⇑Ordinal.lift.initialSeg = Ordinal.lift.{v, u}
<GOAL>(Ordinal.type fun x x_1 => x < x_1) = Ordinal.omega
<GOAL>Ordinal.lift.{u_3, u_4} Ordinal.omega = Ordinal.omega
<VAR>o₁ o₂ : Ordinal.{u_3}<GOAL>(o₁ + o₂).card = o₁.card + o₂.card
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.type (Sum.Lex r s) = Ordinal.type r + Ordinal.type s
<VAR>n : ℕ<GOAL>(↑n).card = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).card = OfNat.ofNat n
<VAR>a b : Ordinal.{u_3}<GOAL>a ≤ a + b
<VAR>a b : Ordinal.{u_3}<GOAL>a ≤ b + a
<VAR>a : Ordinal.{u_3}<GOAL>max 0 a = a
<VAR>a : Ordinal.{u_3}<GOAL>max a 0 = a
<VAR>a b : Ordinal.{u_3}<GOAL>max a b = 0 ↔ a = 0 ∧ b = 0
<VAR>a b : Ordinal.{u_3}<GOAL>a + 1 ≤ b ↔ a < b
<VAR>o : Ordinal.{u_3}<GOAL>o + 1 = Order.succ o
<VAR>o₁ o₂ : Ordinal.{u_3}<GOAL>o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)
<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o ↔ 0 < o
<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o ↔ o ≠ 0
<VAR>o : Ordinal.{u_3}<GOAL>0 < Order.succ o
<VAR>o : Ordinal.{u_3}<GOAL>Order.succ o ≠ 0
<VAR>a : Ordinal.{u_3}<GOAL>a < 1 ↔ a = 0
<VAR>a : Ordinal.{u_3}<GOAL>a ≤ 1 ↔ a = 0 ∨ a = 1
<VAR>o : Ordinal.{u_3}<GOAL>(Order.succ o).card = o.card + 1
<VAR>x : (Quotient.out 1).α<GOAL>x = Ordinal.enum (fun x x_1 => x < x_1) 0 ⋯
<VAR>x : (Quotient.out 1).α<GOAL>Ordinal.typein (fun x x_1 => x < x_1) x = 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>x x' : α<GOAL>Ordinal.typein r x ≤ Ordinal.typein r x' ↔ ¬r x' x
<VAR>o : Ordinal.{u_3}<VAR>x x' : (Quotient.out o).α<GOAL>Ordinal.typein (fun x x_1 => x < x_1) x ≤ Ordinal.typein (fun x x_1 => x < x_1) x' ↔ x ≤ x'
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>o o' : Ordinal.{u}<VAR>ho : o < Ordinal.type r<VAR>ho' : o' < Ordinal.type r<GOAL>¬r (Ordinal.enum r o' ho') (Ordinal.enum r o ho) ↔ o ≤ o'
<VAR>a : Ordinal.{u_3}<VAR>o o' : Ordinal.{u_3}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>ho' : o' < Ordinal.type fun x x_1 => x < x_1<GOAL>Ordinal.enum (fun x x_1 => x < x_1) o ho ≤ Ordinal.enum (fun x x_1 => x < x_1) o' ho' ↔ o ≤ o'
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>h0 : 0 < Ordinal.type r<VAR>a : α<GOAL>¬r a (Ordinal.enum r 0 h0)
<VAR>o : Ordinal.{u_3}<VAR>h0 : 0 < o<VAR>a : (Quotient.out o).α<GOAL>Ordinal.enum (fun x x_1 => x < x_1) 0 ⋯ ≤ a
<VAR>o : Ordinal.{u_3}<VAR>a : (Quotient.out (Order.succ o)).α<GOAL>a ≤ Ordinal.enum (fun x x_1 => x < x_1) o ⋯
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>o₁ o₂ : Ordinal.{u}<VAR>h₁ : o₁ < Ordinal.type r<VAR>h₂ : o₂ < Ordinal.type r<GOAL>Ordinal.enum r o₁ h₁ = Ordinal.enum r o₂ h₂ ↔ o₁ = o₂
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>x : α<GOAL>↑((Ordinal.enumIso r).symm x) = Ordinal.typein r x
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>x : ↑fun x => x < Ordinal.type r<GOAL>(Ordinal.enumIso r) x = Ordinal.enum r ↑x ⋯
<VAR>o : Ordinal.{u_3}<VAR>x : ↑(Set.Iio o)<GOAL>o.enumIsoOut x = Ordinal.enum (fun x x_1 => x < x_1) ↑x ⋯
<VAR>o : Ordinal.{u_3}<VAR>x : (Quotient.out o).α<GOAL>↑((RelIso.symm o.enumIsoOut) x) = Ordinal.typein (fun x x_1 => x < x_1) x
<VAR>o : Ordinal.{u_3}<VAR>ho : 0 < o<GOAL>Ordinal.enum (fun x x_1 => x < x_1) 0 ⋯ = ⊥
<GOAL>Ordinal.univ.{u, u + 1} = Ordinal.type fun x x_1 => x < x_1
<GOAL>Ordinal.lift.{w, max (u + 1) v} Ordinal.univ.{u, v} = Ordinal.univ.{u, max v w}
<GOAL>Ordinal.univ.{u, max (u + 1) v} = Ordinal.univ.{u, v}
<GOAL>⇑Ordinal.lift.principalSeg.toRelEmbedding = Ordinal.lift.{max (u + 1) v, u}
<GOAL>Ordinal.lift.principalSeg.top = Ordinal.univ.{u, v}
<GOAL>Ordinal.lift.principalSeg.top = Ordinal.type fun x x_1 => x < x_1
<VAR>o : Ordinal.{u_3}<GOAL>#(Quotient.out o).α = o.card
<VAR>α : Type u<GOAL>(#α).ord = ⨅ r, Ordinal.type ↑r
<VAR>α : Type u_3<GOAL>∃ r, ∃ (wo : IsWellOrder α r), (#α).ord = Ordinal.type r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h : IsWellOrder α r<GOAL>(#α).ord ≤ Ordinal.type r
<VAR>c : Cardinal.{u_3}<VAR>o : Ordinal.{u_3}<GOAL>c.ord ≤ o ↔ c ≤ o.card
<VAR>c : Cardinal.{u_3}<VAR>o : Ordinal.{u_3}<GOAL>o < c.ord ↔ o.card < c
<VAR>c : Cardinal.{u_3}<GOAL>c.ord.card = c
<VAR>o : Ordinal.{u_3}<GOAL>o.card.ord ≤ o
<VAR>o : Ordinal.{u_3}<GOAL>o < (Order.succ o.card).ord
<VAR>o : Ordinal.{u_3}<VAR>c : Cardinal.{u_3}<GOAL>o.card ≤ c ↔ o < (Order.succ c).ord
<VAR>o : Ordinal.{u_3}<VAR>c : Cardinal.{u_3}<VAR>ho : o ≤ c.ord<GOAL>o.card ≤ c
<VAR>c₁ c₂ : Cardinal.{u_3}<GOAL>c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂
<VAR>c₁ c₂ : Cardinal.{u_3}<GOAL>c₁.ord < c₂.ord ↔ c₁ < c₂
<VAR>n : ℕ<GOAL>(↑n).ord = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).ord = OfNat.ofNat n
<VAR>c : Cardinal.{v}<GOAL>Ordinal.lift.{u, v} c.ord = (Cardinal.lift.{u, v} c).ord
<VAR>c : Cardinal.{u_3}<GOAL>#(Quotient.out c.ord).α = c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>x : α<VAR>h : (#α).ord = Ordinal.type r<GOAL>(Ordinal.typein r x).card < #α
<VAR>c : Cardinal.{u_3}<VAR>x : (Quotient.out c.ord).α<GOAL>(Ordinal.typein (fun x x_1 => x < x_1) x).card < c
<VAR>c : Cardinal.{u_3}<VAR>i : (Quotient.out c.ord).α<GOAL>#↑(Set.Iio i) < c
<GOAL>Cardinal.univ.{u, u + 1} = #Ordinal.{u}
<GOAL>Cardinal.lift.{w, max (u + 1) v} Cardinal.univ.{u, v} = Cardinal.univ.{u, max v w}
<GOAL>Cardinal.univ.{u, max (u + 1) v} = Cardinal.univ.{u, v}
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{u + 1, u} c < Cardinal.univ.{u, u + 1}
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
<GOAL>Cardinal.univ.{u, v}.ord = Ordinal.univ.{u, v}
<VAR>c : Cardinal.{u + 1}<GOAL>c < Cardinal.univ.{u, u + 1} ↔ ∃ c', c = Cardinal.lift.{u + 1, u} c'
<VAR>c : Cardinal.{max (u + 1) v}<GOAL>c < Cardinal.univ.{u, v} ↔ ∃ c', c = Cardinal.lift.{max (u + 1) v, u} c'
<VAR>α : Type u<GOAL>Small.{v, u} α ↔ Cardinal.lift.{v + 1, u} #α < Cardinal.univ.{v, max u (v + 1)}
<GOAL>Ordinal.univ.{u, v}.card = Cardinal.univ.{u, v}
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>↑n ≤ o.card ↔ ↑n ≤ o
<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o.card ↔ 1 ≤ o
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≤ o.card ↔ OfNat.ofNat n ≤ o
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>↑n < o.card ↔ ↑n < o
<VAR>o : Ordinal.{u_3}<GOAL>0 < o.card ↔ 0 < o
<VAR>o : Ordinal.{u_3}<GOAL>1 < o.card ↔ 1 < o
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n < o.card ↔ OfNat.ofNat n < o
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>o.card < ↑n ↔ o < ↑n
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>o.card < OfNat.ofNat n ↔ o < OfNat.ofNat n
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>o.card ≤ ↑n ↔ o ≤ ↑n
<VAR>o : Ordinal.{u_3}<GOAL>o.card ≤ 1 ↔ o ≤ 1
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>o.card ≤ OfNat.ofNat n ↔ o ≤ OfNat.ofNat n
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>o.card = ↑n ↔ o = ↑n
<VAR>o : Ordinal.{u_3}<GOAL>o.card = 0 ↔ o = 0
<VAR>o : Ordinal.{u_3}<GOAL>o.card = 1 ↔ o = 1
<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>o.card = OfNat.ofNat n ↔ o = OfNat.ofNat n
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>Fintype α<GOAL>Ordinal.type r = ↑(Fintype.card α)
<VAR>n : ℕ<GOAL>(Ordinal.type fun x x_1 => x < x_1) = ↑n
<VAR>α : Type u<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>l m : List α<VAR>o : Ordinal.{u}<VAR>hl : List.Sorted (fun x x_1 => x > x_1) l<VAR>hm : List.Sorted (fun x x_1 => x > x_1) m<VAR>hmltl : m < l<VAR>hlt : ∀ i ∈ l, Ordinal.typein (fun x x_1 => x < x_1) i < o<VAR>i : α<GOAL>i ∈ m → Ordinal.typein (fun x x_1 => x < x_1) i < o
<VAR>self : YoungDiagram<GOAL>IsLowerSet ↑self.cells
<VAR>μ : YoungDiagram<VAR>c : ℕ × ℕ<GOAL>c ∈ μ.cells ↔ c ∈ μ
<VAR>c : ℕ × ℕ<VAR>cells : Finset (ℕ × ℕ)<VAR>isLowerSet : IsLowerSet ↑cells<GOAL>c ∈ { cells := cells, isLowerSet := isLowerSet } ↔ c ∈ cells
<VAR>μ : YoungDiagram<VAR>i1 i2 j1 j2 : ℕ<VAR>hi : i1 ≤ i2<VAR>hj : j1 ≤ j2<VAR>hcell : (i2, j2) ∈ μ<GOAL>(i1, j1) ∈ μ
<VAR>μ ν : YoungDiagram<GOAL>μ.cells ⊆ ν.cells ↔ μ ≤ ν
<VAR>μ ν : YoungDiagram<GOAL>μ.cells ⊂ ν.cells ↔ μ < ν
<VAR>μ ν : YoungDiagram<GOAL>(μ ⊔ ν).cells = μ.cells ∪ ν.cells
<VAR>μ ν : YoungDiagram<GOAL>↑(μ ⊔ ν) = ↑μ ∪ ↑ν
<VAR>μ ν : YoungDiagram<VAR>x : ℕ × ℕ<GOAL>x ∈ μ ⊔ ν ↔ x ∈ μ ∨ x ∈ ν
<VAR>μ ν : YoungDiagram<GOAL>(μ ⊓ ν).cells = μ.cells ∩ ν.cells
<VAR>μ ν : YoungDiagram<GOAL>↑(μ ⊓ ν) = ↑μ ∩ ↑ν
<VAR>μ ν : YoungDiagram<VAR>x : ℕ × ℕ<GOAL>x ∈ μ ⊓ ν ↔ x ∈ μ ∧ x ∈ ν
<VAR>x : ℕ × ℕ<GOAL>x ∉ ⊥
<VAR>μ : YoungDiagram<VAR>c : ℕ × ℕ<GOAL>c ∈ μ.transpose ↔ c.swap ∈ μ
<VAR>μ : YoungDiagram<GOAL>μ.transpose.transpose = μ
<VAR>μ ν : YoungDiagram<GOAL>μ.transpose = ν ↔ μ = ν.transpose
<VAR>μ ν : YoungDiagram<VAR>h_le : μ.transpose ≤ ν<GOAL>μ ≤ ν.transpose
<VAR>μ ν : YoungDiagram<GOAL>μ.transpose ≤ ν.transpose ↔ μ ≤ ν
<VAR>μ ν : YoungDiagram<VAR>h_le : μ ≤ ν<GOAL>μ.transpose ≤ ν.transpose
<VAR>μ : YoungDiagram<GOAL>(RelIso.symm YoungDiagram.transposeOrderIso) μ = μ.transpose
<VAR>μ : YoungDiagram<GOAL>YoungDiagram.transposeOrderIso μ = μ.transpose
<VAR>μ : YoungDiagram<VAR>i : ℕ<VAR>c : ℕ × ℕ<GOAL>c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ μ.row i ↔ (i, j) ∈ μ
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ μ ↔ j < μ.rowLen i
<VAR>μ : YoungDiagram<VAR>i : ℕ<GOAL>μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)
<VAR>μ : YoungDiagram<VAR>j : ℕ<VAR>c : ℕ × ℕ<GOAL>c ∈ μ.col j ↔ c ∈ μ ∧ c.2 = j
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ μ.col j ↔ (i, j) ∈ μ
<VAR>μ : YoungDiagram<VAR>j : ℕ<GOAL>μ.transpose.colLen j = μ.rowLen j
<VAR>μ : YoungDiagram<VAR>i : ℕ<GOAL>μ.transpose.rowLen i = μ.colLen i
<VAR>μ : YoungDiagram<VAR>j : ℕ<GOAL>μ.col j = Finset.range (μ.colLen j) ×ˢ {j}
<VAR>μ : YoungDiagram<VAR>j : ℕ<GOAL>μ.colLen j = (μ.col j).card
<VAR>μ : YoungDiagram<GOAL>List.Sorted (fun x x_1 => x ≥ x_1) μ.rowLens
<VAR>w : List ℕ<VAR>c : ℕ × ℕ<GOAL>c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ (h : c.1 < w.length), c.2 < w.get ⟨c.1, h⟩
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>c : ℕ × ℕ<GOAL>c ∈ YoungDiagram.ofRowLens w hw ↔ ∃ (h : c.1 < w.length), c.2 < w.get ⟨c.1, h⟩
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>hpos : ∀ x ∈ w, 0 < x<GOAL>(YoungDiagram.ofRowLens w hw).rowLens.length = w.length
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>i : Fin w.length<GOAL>(YoungDiagram.ofRowLens w hw).rowLen ↑i = w.get i
<VAR>μ : YoungDiagram<GOAL>YoungDiagram.ofRowLens μ.rowLens ⋯ = μ
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>hpos : ∀ x ∈ w, 0 < x<GOAL>(YoungDiagram.ofRowLens w hw).rowLens = w
<VAR>μ : YoungDiagram<GOAL>↑(YoungDiagram.equivListRowLens μ) = μ.rowLens
<VAR>ww : { w // List.Sorted (fun x x_1 => x ≥ x_1) w ∧ ∀ x ∈ w, 0 < x }<GOAL>YoungDiagram.equivListRowLens.symm ww = YoungDiagram.ofRowLens ↑ww ⋯
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<GOAL>DevosMulRel x y ↔ (x.1 * x.2).card < (y.1 * y.2).card ∨ (x.1 * x.2).card = (y.1 * y.2).card ∧ y.1.card + y.2.card < x.1.card + x.2.card ∨ (x.1 * x.2).card = (y.1 * y.2).card ∧ x.1.card + x.2.card = y.1.card + y.2.card ∧ x.1.card < y.1.card
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<GOAL>DevosAddRel x y ↔ (x.1 + x.2).card < (y.1 + y.2).card ∨ (x.1 + x.2).card = (y.1 + y.2).card ∧ y.1.card + y.2.card < x.1.card + x.2.card ∨ (x.1 + x.2).card = (y.1 + y.2).card ∧ x.1.card + x.2.card = y.1.card + y.2.card ∧ x.1.card < y.1.card
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<VAR>mul : (x.1 + x.2).card ≤ (y.1 + y.2).card<VAR>hadd : y.1.card + y.2.card < x.1.card + x.2.card<GOAL>DevosAddRel x y
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<VAR>mul : (x.1 * x.2).card ≤ (y.1 * y.2).card<VAR>hadd : y.1.card + y.2.card < x.1.card + x.2.card<GOAL>DevosMulRel x y
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<VAR>mul : (x.1 * x.2).card ≤ (y.1 * y.2).card<VAR>hadd : y.1.card + y.2.card ≤ x.1.card + x.2.card<VAR>hone : x.1.card < y.1.card<GOAL>DevosMulRel x y
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<VAR>x y : Finset α × Finset α<VAR>mul : (x.1 + x.2).card ≤ (y.1 + y.2).card<VAR>hadd : y.1.card + y.2.card ≤ x.1.card + x.2.card<VAR>hone : x.1.card < y.1.card<GOAL>DevosAddRel x y
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<GOAL>{x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosAddRel
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<GOAL>{x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosMulRel
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>min (Monoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>min (AddMonoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s + t).card
<VAR>α : Type u_1<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : AddMonoid.IsTorsionFree α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s + t).card
<VAR>α : Type u_1<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Monoid.IsTorsionFree α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s * t).card
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s t : Finset (ZMod p)<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>min p (s.card + t.card - 1) ≤ (s + t).card
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddSemigroup α<VAR>IsCancelAdd α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s + t).card
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Semigroup α<VAR>IsCancelMul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s * t).card
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>self : G.Dart<GOAL>G.Adj self.toProd.1 self.toProd.2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d₁ d₂ : G.Dart<GOAL>d₁ = d₂ ↔ d₁.toProd = d₂.toProd
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d₁ d₂ : G.Dart<VAR>h : d₁.toProd = d₂.toProd<GOAL>d₁ = d₂
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>Function.Injective SimpleGraph.Dart.toProd
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>p : V × V<VAR>h : G.Adj p.1 p.2<GOAL>{ toProd := p, adj := h }.edge = Sym2.mk p
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<GOAL>d.edge ∈ G.edgeSet
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<GOAL>d.symm.toProd = d.swap
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>p : V × V<VAR>h : G.Adj p.1 p.2<GOAL>{ toProd := p, adj := h }.symm = { toProd := p.swap, adj := ⋯ }
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<GOAL>d.symm.edge = d.edge
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>SimpleGraph.Dart.edge ∘ SimpleGraph.Dart.symm = SimpleGraph.Dart.edge
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<GOAL>d.symm.symm = d
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>Function.Involutive SimpleGraph.Dart.symm
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<GOAL>d.symm ≠ d
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d₁ d₂ : G.Dart<GOAL>d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<VAR>p : V × V<GOAL>d.edge = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = p.swap
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>d : G.Dart<VAR>u v : V<GOAL>d.edge = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>w : ↑(G.neighborSet v)<GOAL>(G.dartOfNeighborSet v w).toProd = (v, ↑w)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<GOAL>Function.Injective (G.dartOfNeighborSet v)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑(∂ 𝒜).card / ↑((Fintype.card α).choose (r - 1))
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ Finset.falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>Set.Sized k ↑(Finset.falling k 𝒜)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜 # k ⊆ Finset.falling k 𝒜
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>Finset.falling 0 𝒜 ⊆ {∅}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜 # k ∪ ∂ (Finset.falling (k + 1) 𝒜) = Finset.falling k 𝒜
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<GOAL>Disjoint (𝒜 # m) (∂ (Finset.falling n 𝒜))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<VAR>hk : k ≤ Fintype.card α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<GOAL>∑ r ∈ Finset.range (k + 1), ↑(𝒜 # (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(Finset.falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<GOAL>∑ r ∈ Finset.range (Fintype.card α + 1), ↑(𝒜 # r).card / ↑((Fintype.card α).choose r) ≤ 1
<VAR>α : Type u_2<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<GOAL>𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Partition<GOAL>Setoid.IsPartition self.parts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Partition<VAR>s : Set V<GOAL>s ∈ self.parts → IsAntichain G.Adj s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v w : V<VAR>h : G.Adj v w<GOAL>P.partOfVertex v ≠ P.partOfVertex w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>Fintype ↑P.parts<GOAL>G.Colorable (Fintype.card ↑P.parts)