ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α ≃ β') ≤ #(α ↪ β')
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α ↪ β') ≤ #(α → β')
<VAR>α : Type u<VAR>Infinite α<GOAL>#(Equiv.Perm α) = #α ^ #α
<VAR>α : Type u<VAR>Infinite α<GOAL>#(Equiv.Perm α) = 2 ^ #α
<VAR>α : Type u<VAR>β' : Type v<VAR>Infinite α<VAR>leq : Cardinal.lift.{v, u} #α = Cardinal.lift.{u, v} #β'<GOAL>#(α ≃ β') = #(α → β')
<VAR>α β : Type u<VAR>Infinite α<VAR>eq : #α = #β<GOAL>#(α ≃ β) = #(α → β)
<VAR>α : Type u<VAR>β' : Type v<VAR>Infinite α<VAR>leq : Cardinal.lift.{v, u} #α = Cardinal.lift.{u, v} #β'<GOAL>#(α ≃ β') = 2 ^ Cardinal.lift.{v, u} #α
<VAR>α β : Type u<VAR>Infinite α<VAR>eq : #α = #β<GOAL>#(α ≃ β) = 2 ^ #α
<VAR>α : Type u<VAR>β' : Type v<VAR>Infinite α<VAR>lle : Cardinal.lift.{u, v} #β' ≤ Cardinal.lift.{v, u} #α<GOAL>#(β' ↪ α) = #(β' → α)
<VAR>α β : Type u<VAR>Infinite α<VAR>le : #β ≤ #α<GOAL>#(β ↪ α) = #(β → α)
<VAR>α : Type u<VAR>β' : Type v<VAR>Infinite α<VAR>lle : Cardinal.lift.{u, v} #β' ≤ Cardinal.lift.{v, u} #α<GOAL>#↑{f | Function.Surjective f} = #(α → β')
<VAR>α β : Type u<VAR>Infinite α<VAR>le : #β ≤ #α<GOAL>#↑{f | Function.Surjective f} = #(α → β)
<VAR>α : Type u<VAR>Infinite α<GOAL>#(List α) = #α
<VAR>α : Type u<VAR>Countable α<VAR>Nonempty α<GOAL>#(List α) = ℵ₀
<VAR>α : Type u<VAR>Nonempty α<GOAL>#(List α) = max #α ℵ₀
<VAR>α : Type u<VAR>Infinite α<GOAL>#(Finset α) = #α
<VAR>α : Type u<VAR>β : Type v<VAR>Infinite α<VAR>Zero β<VAR>Nontrivial β<GOAL>#(α →₀ β) = max (Cardinal.lift.{v, u} #α) (Cardinal.lift.{u, v} #β)
<VAR>α β : Type u<VAR>Infinite α<VAR>Zero β<VAR>Nontrivial β<GOAL>#(α →₀ β) = max #α #β
<VAR>α : Type u<VAR>β : Type v<VAR>Nonempty α<VAR>Zero β<VAR>Infinite β<GOAL>#(α →₀ β) = max (Cardinal.lift.{v, u} #α) (Cardinal.lift.{u, v} #β)
<VAR>α β : Type u<VAR>Nonempty α<VAR>Zero β<VAR>Infinite β<GOAL>#(α →₀ β) = max #α #β
<VAR>α : Type u<VAR>Nonempty α<GOAL>#(α →₀ ℕ) = max #α ℵ₀
<VAR>α : Type u<VAR>Nonempty α<GOAL>#(Multiset α) = max #α ℵ₀
<VAR>α : Type u<VAR>Infinite α<GOAL>#(Multiset α) = #α
<VAR>α : Type u<VAR>IsEmpty α<GOAL>#(Multiset α) = 1
<VAR>α : Type u<VAR>Countable α<VAR>Nonempty α<GOAL>#(Multiset α) = ℵ₀
<VAR>α : Type u<VAR>Infinite α<VAR>c : Cardinal.{u}<GOAL>#{ t // #↑t ≤ c } ≤ #α ^ c
<VAR>α : Type u_1<VAR>Infinite α<VAR>s : Set α<VAR>h2 : #↑s < #α<GOAL>#↑sᶜ = #α
<VAR>α : Type u_1<VAR>Infinite α<VAR>s : Finset α<GOAL>#↑(↑s)ᶜ = #α
<VAR>α : Type u_1<VAR>Infinite α<VAR>s t : Set α<VAR>hs : #↑s < #α<VAR>ht : #↑t < #α<GOAL>#↑sᶜ = #↑tᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>Finite α<VAR>s : Set α<VAR>t : Set β<VAR>h1 : Cardinal.lift.{max v w, u} #α = Cardinal.lift.{max u w, v} #β<VAR>h2 : Cardinal.lift.{max v w, u} #↑s = Cardinal.lift.{max u w, v} #↑t<GOAL>Cardinal.lift.{max v w, u} #↑sᶜ = Cardinal.lift.{max u w, v} #↑tᶜ
<VAR>α β : Type u<VAR>Finite α<VAR>s : Set α<VAR>t : Set β<VAR>h1 : #α = #β<VAR>h : #↑s = #↑t<GOAL>#↑sᶜ = #↑tᶜ
<VAR>α : Type u<VAR>Finite α<VAR>s t : Set α<VAR>h : #↑s = #↑t<GOAL>#↑sᶜ = #↑tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (↑sᶜ ≃ ↑(Set.range ⇑f)ᶜ)<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (α ≃ β)<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>hs : #↑s < #α<VAR>h : Nonempty (α ≃ β)<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<GOAL>Surreal.Multiplication.P3 x₁ x₂ y₁ y₂ ↔ Surreal.Multiplication.P3 y₁ y₂ x₁ x₂
<VAR>x₁ x₂ x₃ y₁ y₂ : SetTheory.PGame<VAR>h₁ : Surreal.Multiplication.P3 x₁ x₂ y₁ y₂<VAR>h₂ : Surreal.Multiplication.P3 x₂ x₃ y₁ y₂<GOAL>Surreal.Multiplication.P3 x₁ x₃ y₁ y₂
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<GOAL>Surreal.Multiplication.P3 x₁ x₂ y₁ y₂ ↔ Surreal.Multiplication.P3 (-x₂) (-x₁) y₁ y₂
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P2 x₁ x₂ y ↔ Surreal.Multiplication.P2 (-x₂) (-x₁) y
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P2 x₁ x₂ y ↔ Surreal.Multiplication.P2 x₁ x₂ (-y)
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P4 x₁ x₂ y ↔ Surreal.Multiplication.P4 (-x₂) (-x₁) y
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P4 x₁ x₂ y ↔ Surreal.Multiplication.P4 x₁ x₂ (-y)
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P24 x₁ x₂ y ↔ Surreal.Multiplication.P24 (-x₂) (-x₁) y
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.P24 x₁ x₂ y ↔ Surreal.Multiplication.P24 x₁ x₂ (-y)
<VAR>x y : SetTheory.PGame<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧ ↔ Surreal.Multiplication.P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)
<VAR>x y : SetTheory.PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.mulOption y i j⟧ < ⟦x * y⟧ ↔ Surreal.Multiplication.P3 (x.moveLeft i) x (y.moveLeft j) y
<VAR>x₁ x₂ x₃ y₁ y₂ y₃ : SetTheory.PGame<VAR>he : x₁ ≈ x₃<VAR>h₁ : Surreal.Multiplication.P2 x₁ x₃ y₁<VAR>h₃ : Surreal.Multiplication.P2 x₁ x₃ y₃<VAR>h3 : Surreal.Multiplication.P3 x₁ x₂ y₂ y₃<GOAL>Surreal.Multiplication.P1 x₁ x₂ x₃ y₁ y₂ y₃
<VAR>x₁ x₂ x₃ y₁ y₂ y₃ : SetTheory.PGame<VAR>h₁ : Surreal.Multiplication.P3 x₃ x₂ y₂ y₃<VAR>h₂ : Surreal.Multiplication.P3 x₁ x₃ y₂ y₁<GOAL>Surreal.Multiplication.P1 x₁ x₂ x₃ y₁ y₂ y₃
<VAR>x y : SetTheory.PGame<GOAL>(Surreal.Multiplication.Args.P1 x y).Numeric ↔ x.Numeric ∧ y.Numeric
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>(Surreal.Multiplication.Args.P24 x₁ x₂ y).Numeric ↔ x₁.Numeric ∧ x₂.Numeric ∧ y.Numeric
<VAR>a' a : Surreal.Multiplication.Args<GOAL>Surreal.Multiplication.ArgsRel a' a → a.Numeric → a'.Numeric
<VAR>x y : SetTheory.PGame<GOAL>Surreal.Multiplication.IH1 x y → Surreal.Multiplication.IH1 (-x) y
<VAR>x y : SetTheory.PGame<GOAL>Surreal.Multiplication.IH1 x y → Surreal.Multiplication.IH1 x (-y)
<VAR>x x' y : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<VAR>h : x'.IsOption x<GOAL>(x' * y).Numeric
<VAR>x y y' : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<VAR>h : y'.IsOption y<GOAL>(x * y').Numeric
<VAR>x x' y y' : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<VAR>hx : x'.IsOption x<VAR>hy : y'.IsOption y<GOAL>(x' * y').Numeric
<VAR>x y : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<GOAL>Surreal.Multiplication.IH1 x y
<VAR>x y : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<GOAL>Surreal.Multiplication.IH1 y x
<VAR>x y : SetTheory.PGame<VAR>hy : y.Numeric<VAR>ihyx : Surreal.Multiplication.IH1 y x<VAR>i : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>Surreal.Multiplication.P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l)
<VAR>x y : SetTheory.PGame<VAR>ihxy : Surreal.Multiplication.IH1 x y<VAR>i j : x.LeftMoves<GOAL>Surreal.Multiplication.P24 (x.moveLeft i) (x.moveLeft j) y
<VAR>x y : SetTheory.PGame<VAR>hy : y.Numeric<VAR>ihxy : Surreal.Multiplication.IH1 x y<VAR>ihyx : Surreal.Multiplication.IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<VAR>h : x.moveLeft i < x.moveLeft j<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : Surreal.Multiplication.IH1 x y<VAR>ihyx : Surreal.Multiplication.IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>x y : SetTheory.PGame<VAR>ih : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P1 x y) → Surreal.Multiplication.P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>(x * y).Numeric
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>ih' : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P24 x₁ x₂ y) → Surreal.Multiplication.P124 a<GOAL>Surreal.Multiplication.IH24 x₁ x₂ y
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>ih' : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P24 x₁ x₂ y) → Surreal.Multiplication.P124 a<GOAL>Surreal.Multiplication.IH24 x₂ x₁ y
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>ih' : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P24 x₁ x₂ y) → Surreal.Multiplication.P124 a<GOAL>Surreal.Multiplication.IH4 x₁ x₂ y
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>ih' : ∀ (a : Surreal.Multiplication.Args), Surreal.Multiplication.ArgsRel a (Surreal.Multiplication.Args.P24 x₁ x₂ y) → Surreal.Multiplication.P124 a<GOAL>(x₁ * y).Numeric ∧ (x₂ * y).Numeric
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.IH24 x₁ x₂ y → Surreal.Multiplication.IH24 (-x₂) (-x₁) y ∧ Surreal.Multiplication.IH24 x₁ x₂ (-y)
<VAR>x₁ x₂ y : SetTheory.PGame<GOAL>Surreal.Multiplication.IH4 x₁ x₂ y → Surreal.Multiplication.IH4 (-x₂) (-x₁) y ∧ Surreal.Multiplication.IH4 x₁ x₂ (-y)
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hn : x₁.Numeric<VAR>h : Surreal.Multiplication.IH24 x₁ x₂ y<VAR>he : x₁ ≈ x₂<VAR>i : x₁.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x₁.mulOption y i j⟧ < ⟦x₂ * y⟧
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>h₁ : x₁.Numeric<VAR>h₂ : x₂.Numeric<VAR>h₁₂ : Surreal.Multiplication.IH24 x₁ x₂ y<VAR>h₂₁ : Surreal.Multiplication.IH24 x₂ x₁ y<VAR>he : x₁ ≈ x₂<GOAL>x₁ * y ≤ x₂ * y
<VAR>x y : SetTheory.PGame<VAR>hn : (x * y).Numeric<GOAL>(Surreal.Multiplication.MulOptionsLTMul x y ∧ Surreal.Multiplication.MulOptionsLTMul (-x) (-y)) ∧ Surreal.Multiplication.MulOptionsLTMul x (-y) ∧ Surreal.Multiplication.MulOptionsLTMul (-x) y
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>h24 : Surreal.Multiplication.IH24 x₁ x₂ y<VAR>h4 : Surreal.Multiplication.IH4 x₁ x₂ y<VAR>hl : Surreal.Multiplication.MulOptionsLTMul x₂ y<VAR>i : x₂.LeftMoves<VAR>j : y.LeftMoves<GOAL>Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ (y.moveLeft j) y
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<VAR>i : x₂.LeftMoves<VAR>h : Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hl : x₁ ≤ x₂.moveLeft i<GOAL>Surreal.Multiplication.P3 x₁ x₂ y₁ y₂
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<VAR>h : ∀ (i : x₂.LeftMoves), Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hs : ∀ (i : (-x₁).LeftMoves), Surreal.Multiplication.IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂<VAR>hl : x₁ < x₂<GOAL>Surreal.Multiplication.P3 x₁ x₂ y₁ y₂
<VAR>a : Surreal.Multiplication.Args<GOAL>a.Numeric → Surreal.Multiplication.P124 a
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>(x * y).Numeric
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx₁ : x₁.Numeric<VAR>hx₂ : x₂.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.Multiplication.P24 x₁ x₂ y
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx₁ : x₁.Numeric<VAR>hx₂ : x₂.Numeric<VAR>hy : y.Numeric<VAR>he : x₁ ≈ x₂<GOAL>x₁ * y ≈ x₂ * y
<VAR>x y₁ y₂ : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>he : y₁ ≈ y₂<GOAL>x * y₁ ≈ x * y₂
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<VAR>hx₁ : x₁.Numeric<VAR>hx₂ : x₂.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁ * y₁ ≈ x₂ * y₂
<VAR>x₁ x₂ y₁ y₂ : SetTheory.PGame<VAR>hx₁ : x₁.Numeric<VAR>hx₂ : x₂.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hx : x₁ < x₂<VAR>hy : y₁ < y₂<GOAL>Surreal.Multiplication.P3 x₁ x₂ y₁ y₂
<VAR>x₁ x₂ : SetTheory.PGame<VAR>hx₁ : x₁.Numeric<VAR>hx₂ : x₂.Numeric<VAR>hp₁ : 0 < x₁<VAR>hp₂ : 0 < x₂<GOAL>0 < x₁ * x₂
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>hs : s.Intersecting<GOAL>t.Intersecting
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>hs : s.Intersecting<GOAL>⊥ ∉ s
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>a : α<VAR>hs : s.Intersecting<VAR>ha : a ∈ s<GOAL>a ≠ ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<GOAL>∅.Intersecting
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a : α<GOAL>{a}.Intersecting ↔ a ≠ ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>a : α<VAR>hs : s.Intersecting<VAR>ha : a ≠ ⊥<VAR>h : ∀ b ∈ s, ¬Disjoint a b<GOAL>(insert a s).Intersecting
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).Intersecting ↔ s.Intersecting ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<GOAL>s.Intersecting ↔ (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.Intersecting ↔ s ≠ {⊥}
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.Intersecting ↔ s = ∅
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set α<VAR>hs : s.Intersecting<VAR>h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t<GOAL>IsUpperSet s
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<VAR>h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t<GOAL>IsUpperSet ↑s
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h𝒜 : 𝒜.Intersecting<VAR>s t : Set α<VAR>hs : s ∈ 𝒜<VAR>ht : t ∈ 𝒜<GOAL>∃ a ∈ s, a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Set (Finset α)<VAR>h𝒜 : 𝒜.Intersecting<VAR>s t : Finset α<VAR>hs : s ∈ 𝒜<VAR>ht : t ∈ 𝒜<GOAL>∃ a ∈ s, a ∈ t
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>s : Set α<VAR>hs : s.Intersecting<VAR>a : α<VAR>ha : a ∈ s<GOAL>aᶜ ∉ s
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>s : Set α<VAR>hs : s.Intersecting<VAR>a : α<VAR>ha : aᶜ ∈ s<GOAL>a ∉ s
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>Disjoint s (Finset.map { toFun := compl, inj' := ⋯ } s)
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>2 * s.card ≤ Fintype.card α
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>Nontrivial α<VAR>Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>(∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>Nontrivial α<VAR>Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : 𝒜.Shatters s<VAR>ha : a ∈ s<GOAL>∃ t ∈ 𝒜, s ∩ t = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>h : 𝒜 ⊆ ℬ<VAR>h𝒜 : 𝒜.Shatters s<GOAL>ℬ.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>h : t ⊆ s<VAR>hs : 𝒜.Shatters s<GOAL>𝒜.Shatters t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>h : 𝒜.Shatters s<GOAL>∃ t ∈ 𝒜, s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>h : ∀ t ⊆ s, t ∈ 𝒜<GOAL>𝒜.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>h : 𝒜.Shatters s<GOAL>𝒜.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.Shatters ∅ ↔ 𝒜.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>h : 𝒜.Shatters s<GOAL>t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>𝒜.Shatters s ↔ Finset.image (fun t => s ∩ t) 𝒜 = s.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>Fintype α<GOAL>Finset.univ.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<GOAL>𝒜.Shatters Finset.univ ↔ 𝒜 = Finset.univ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h : 𝒜 ⊆ ℬ<GOAL>𝒜.shatterer ⊆ ℬ.shatterer
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>h : IsLowerSet ↑𝒜<GOAL>𝒜 ⊆ 𝒜.shatterer
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>IsLowerSet ↑𝒜.shatterer
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.shatterer.shatterer = 𝒜.shatterer
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<VAR>a : α<VAR>h : ∀ t ∈ 𝒜, a ∉ t<VAR>ht : 𝒜.Shatters t<GOAL>a ∉ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : (𝓓 a 𝒜).Shatters s<GOAL>𝒜.Shatters s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hs : 𝒜.Shatters s<GOAL>s.card ≤ 𝒜.vcDim
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(𝓓 a 𝒜).vcDim ≤ 𝒜.vcDim
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<GOAL>𝒜.shatterer.card ≤ ∑ k ∈ Finset.Iic 𝒜.vcDim, (Fintype.card α).choose k
<VAR>n : ℕ<VAR>self : n.Partition<GOAL>self.parts.sum = n
<VAR>n : ℕ<VAR>self : n.Partition<VAR>i : ℕ<GOAL>i ∈ self.parts → 0 < i
<VAR>n : ℕ<VAR>c : Composition n<GOAL>(Nat.Partition.ofComposition n c).parts = ↑c.blocks
<VAR>n : ℕ<GOAL>Function.Surjective (Nat.Partition.ofComposition n)
<VAR>n : ℕ<VAR>l : Multiset ℕ<VAR>hl : l.sum = n<GOAL>(Nat.Partition.ofSums n l hl).parts = Multiset.filter (fun x => x ≠ 0) l
<VAR>l : Multiset ℕ<GOAL>(Nat.Partition.ofMultiset l).parts = Multiset.filter (fun x => ¬x = 0) l
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>DecidableEq σ<VAR>DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>Nat.Partition.ofSym (Sym.map (⇑e) s) = Nat.Partition.ofSym s
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(Nat.Partition.indiscrete n).parts = {n}
<VAR>p : Nat.Partition 0<GOAL>p.parts = 0
<VAR>p : Nat.Partition 1<GOAL>p.parts = {1}
<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>s : Sym σ 1<GOAL>Nat.Partition.ofSym s = Nat.Partition.indiscrete 1
<VAR>n : ℕ<VAR>l : Multiset ℕ<VAR>hl : l.sum = n<VAR>i : ℕ<VAR>hi : i ≠ 0<GOAL>Multiset.count i (Nat.Partition.ofSums n l hl).parts = Multiset.count i l
<VAR>n : ℕ<VAR>l : Multiset ℕ<VAR>hl : l.sum = n<GOAL>Multiset.count 0 (Nat.Partition.ofSums n l hl).parts = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>t : Finset β<VAR>a : α<VAR>DecidablePred (r a)<GOAL>Finset.bipartiteBelow (Function.swap r) t a = Finset.bipartiteAbove r t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>b : β<VAR>(a : α) → Decidable (r a b)<GOAL>Finset.bipartiteAbove (Function.swap r) s b = Finset.bipartiteBelow r s b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>b : β<VAR>(a : α) → Decidable (r a b)<GOAL>↑(Finset.bipartiteBelow r s b) = {a | a ∈ s ∧ r a b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>t : Finset β<VAR>a : α<VAR>DecidablePred (r a)<GOAL>↑(Finset.bipartiteAbove r t a) = {b | b ∈ t ∧ r a b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>b : β<VAR>(a : α) → Decidable (r a b)<VAR>a : α<GOAL>a ∈ Finset.bipartiteBelow r s b ↔ a ∈ s ∧ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>t : Finset β<VAR>a : α<VAR>DecidablePred (r a)<VAR>b : β<GOAL>b ∈ Finset.bipartiteAbove r t a ↔ b ∈ t ∧ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>(a : α) → (b : β) → Decidable (r a b)<GOAL>∑ a ∈ s, (Finset.bipartiteAbove r t a).card = ∑ b ∈ t, (Finset.bipartiteBelow r s b).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>m n : ℕ<VAR>(a : α) → (b : β) → Decidable (r a b)<VAR>hm : ∀ a ∈ s, m ≤ (Finset.bipartiteAbove r t a).card<VAR>hn : ∀ b ∈ t, (Finset.bipartiteBelow r s b).card ≤ n<GOAL>s.card * m ≤ t.card * n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>m n : ℕ<VAR>(a : α) → (b : β) → Decidable (r a b)<VAR>hn : ∀ b ∈ t, n ≤ (Finset.bipartiteBelow r s b).card<VAR>hm : ∀ a ∈ s, (Finset.bipartiteAbove r t a).card ≤ m<GOAL>t.card * n ≤ s.card * m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>m n : ℕ<VAR>(a : α) → (b : β) → Decidable (r a b)<VAR>hm : ∀ a ∈ s, (Finset.bipartiteAbove r t a).card = m<VAR>hn : ∀ b ∈ t, (Finset.bipartiteBelow r s b).card = n<GOAL>s.card * m = t.card * n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>hs : ∀ a ∈ s, ∃ b ∈ t, r a b<VAR>ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton<GOAL>s.card ≤ t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>ht : ∀ b ∈ t, ∃ a ∈ s, r a b<VAR>hs : ∀ a ∈ s, {b | b ∈ t ∧ r a b}.Subsingleton<GOAL>t.card ≤ s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>r : α → β → Prop<VAR>h₁ : Relator.LeftTotal r<VAR>h₂ : Relator.LeftUnique r<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>r : α → β → Prop<VAR>h₁ : Relator.RightTotal r<VAR>h₂ : Relator.RightUnique r<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>Nonempty α<VAR>s : Finset ι<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i ∈ s, (↑(f i)).Intersecting<GOAL>(s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)
<VAR>σ : Type u<GOAL>Nonempty (σ ↪ Cardinal.{u})
<VAR>self : WellOrder<GOAL>IsWellOrder self.α self.r
<VAR>o : WellOrder<GOAL>{ α := o.α, r := o.r, wo := ⋯ } = o
<VAR>w : WellOrder<GOAL>⟦w⟧ = Ordinal.type w.r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<GOAL>⟦{ α := α, r := r, wo := wo }⟧ = Ordinal.type r
<VAR>o : Ordinal.{u_3}<GOAL>Ordinal.type (Quotient.out o).r = o
<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 ≃r s)
<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>o : Ordinal.{u_3}<GOAL>(Ordinal.type fun x x_1 => x < x_1) = o
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>IsEmpty α<GOAL>Ordinal.type r = 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>Ordinal.type r = 0 ↔ IsEmpty α
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>Ordinal.type r ≠ 0 ↔ Nonempty α
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>h : Nonempty α<GOAL>Ordinal.type r ≠ 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>Unique α<GOAL>Ordinal.type r = 1
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<GOAL>Ordinal.type r = 1 ↔ Nonempty (Unique α)
<VAR>o : Ordinal.{u_3}<GOAL>IsEmpty (Quotient.out o).α ↔ o = 0
<VAR>o : Ordinal.{u_3}<VAR>h : IsEmpty (Quotient.out o).α<GOAL>o = 0
<VAR>o : Ordinal.{u_3}<GOAL>Nonempty (Quotient.out o).α ↔ o ≠ 0
<VAR>o : Ordinal.{u_3}<VAR>h : Nonempty (Quotient.out o).α<GOAL>o ≠ 0
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : β ≃ α<GOAL>Ordinal.type (⇑f ⁻¹'o r) = Ordinal.type r
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : β ≃ α<GOAL>(Ordinal.type fun x y => r (f x) (f y)) = Ordinal.type r
<VAR>C : Ordinal.{u_3} → Prop<VAR>o : Ordinal.{u_3}<VAR>H : ∀ (α : Type u_3) (r : α → α → Prop) [inst : IsWellOrder α r], C (Ordinal.type r)<GOAL>C o
<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<GOAL>Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ↪r 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