ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ∑ x ∈ s, w x<GOAL>∃ y ∈ t, b ≤ ∑ x ∈ Finset.filter (fun x => f x = y) s, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : ∑ x ∈ s, w x ≤ t.card • b<GOAL>∃ y ∈ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ y ∉ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x ≤ 0<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ∑ x ∈ s, w x<GOAL>∃ y ∈ t, b ≤ ∑ x ∈ Finset.filter (fun x => f x = y) s, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ y ∉ t, 0 ≤ ∑ x ∈ Finset.filter (fun x => f x = y) s, w x<VAR>ht : t.Nonempty<VAR>hb : ∑ x ∈ s, w x ≤ t.card • b<GOAL>∃ y ∈ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.card • b < ↑s.card<GOAL>∃ y ∈ t, b < ↑(Finset.filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>hn : t.card * n < s.card<GOAL>∃ y ∈ t, n < (Finset.filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>ht : ↑s.card < t.card • b<GOAL>∃ y ∈ t, ↑(Finset.filter (fun x => f x = y) s).card < b
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>n : ℕ<VAR>hn : s.card < t.card * n<GOAL>∃ y ∈ t, (Finset.filter (fun x => f x = y) s).card < n
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ↑s.card<GOAL>∃ y ∈ t, b ≤ ↑(Finset.filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hn : t.card * n ≤ s.card<GOAL>∃ y ∈ t, n ≤ (Finset.filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>ht : t.Nonempty<VAR>hb : ↑s.card ≤ t.card • b<GOAL>∃ y ∈ t, ↑(Finset.filter (fun x => f x = y) s).card ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>n : ℕ<VAR>ht : t.Nonempty<VAR>hn : s.card ≤ t.card * n<GOAL>∃ y ∈ t, (Finset.filter (fun x => f x = y) s).card ≤ n
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hb : Fintype.card β • b < ∑ x : α, w x<GOAL>∃ y, b < ∑ x ∈ Finset.filter (fun x => f x = y) Finset.univ, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>Nonempty β<VAR>hb : Fintype.card β • b ≤ ∑ x : α, w x<GOAL>∃ y, b ≤ ∑ x ∈ Finset.filter (fun x => f x = y) Finset.univ, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hb : ∑ x : α, w x < Fintype.card β • b<GOAL>∃ y, ∑ x ∈ Finset.filter (fun x => f x = y) Finset.univ, w x < b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>Nonempty β<VAR>hb : ∑ x : α, w x ≤ Fintype.card β • b<GOAL>∃ y, ∑ x ∈ Finset.filter (fun x => f x = y) Finset.univ, w x ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>hb : Fintype.card β • b < ↑(Fintype.card α)<GOAL>∃ y, b < ↑(Finset.filter (fun x => f x = y) Finset.univ).card
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>n : ℕ<VAR>hn : Fintype.card β * n < Fintype.card α<GOAL>∃ y, n < (Finset.filter (fun x => f x = y) Finset.univ).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>hb : ↑(Fintype.card α) < Fintype.card β • b<GOAL>∃ y, ↑(Finset.filter (fun x => f x = y) Finset.univ).card < b
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>n : ℕ<VAR>hn : Fintype.card α < Fintype.card β * n<GOAL>∃ y, (Finset.filter (fun x => f x = y) Finset.univ).card < n
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>Nonempty β<VAR>hb : Fintype.card β • b ≤ ↑(Fintype.card α)<GOAL>∃ y, b ≤ ↑(Finset.filter (fun x => f x = y) Finset.univ).card
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>n : ℕ<VAR>Nonempty β<VAR>hn : Fintype.card β * n ≤ Fintype.card α<GOAL>∃ y, n ≤ (Finset.filter (fun x => f x = y) Finset.univ).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>b : M<VAR>LinearOrderedCommSemiring M<VAR>Nonempty β<VAR>hb : ↑(Fintype.card α) ≤ Fintype.card β • b<GOAL>∃ y, ↑(Finset.filter (fun x => f x = y) Finset.univ).card ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>n : ℕ<VAR>Nonempty β<VAR>hn : Fintype.card α ≤ Fintype.card β * n<GOAL>∃ y, (Finset.filter (fun x => f x = y) Finset.univ).card ≤ n
<VAR>s : Set ℕ<VAR>hs : s.Infinite<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>∃ m ∈ s, ∃ n ∈ s, m < n ∧ m ≡ n [MOD k]
<VAR>a b : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} (a + b) = Ordinal.lift.{u, v} a + Ordinal.lift.{u, v} b
<VAR>a : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} (Order.succ a) = Order.succ (Ordinal.lift.{u, v} a)
<VAR>a : Ordinal.{u_4}<VAR>b c : Ordinal.{u_4}<GOAL>a + b = a + c ↔ b = c
<VAR>a : Ordinal.{u_4}<VAR>b c : Ordinal.{u_4}<GOAL>a + b < a + c ↔ b < c
<VAR>a b : Ordinal.{u_4}<VAR>n : ℕ<GOAL>a + ↑n ≤ b + ↑n ↔ a ≤ b
<VAR>a b : Ordinal.{u_4}<VAR>n : ℕ<GOAL>a + ↑n = b + ↑n ↔ a = b
<VAR>a b : Ordinal.{u_4}<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>a b : Ordinal.{u_4}<VAR>h : a + b = 0<GOAL>a = 0
<VAR>a b : Ordinal.{u_4}<VAR>h : a + b = 0<GOAL>b = 0
<VAR>o : Ordinal.{u_4}<GOAL>(Order.succ o).pred = o
<VAR>o : Ordinal.{u_4}<GOAL>o.pred ≤ o
<VAR>o : Ordinal.{u_4}<GOAL>o.pred = o ↔ ¬∃ a, o = Order.succ a
<VAR>o : Ordinal.{u_4}<GOAL>o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ Order.succ a
<VAR>o : Ordinal.{u_4}<GOAL>o.pred < o ↔ ∃ a, o = Order.succ a
<VAR>o : Ordinal.{u_4}<GOAL>Order.succ o.pred = o ↔ ∃ a, o = Order.succ a
<VAR>o b : Ordinal.{u_4}<VAR>h : ¬∃ a, o = Order.succ a<GOAL>Order.succ b < o ↔ b < o
<VAR>a b : Ordinal.{u_4}<GOAL>a < b.pred ↔ Order.succ a < b
<VAR>a b : Ordinal.{u_4}<GOAL>a.pred ≤ b ↔ a ≤ Order.succ b
<VAR>o : Ordinal.{v}<GOAL>(∃ a, Ordinal.lift.{u, v} o = Order.succ a) ↔ ∃ a, o = Order.succ a
<VAR>o : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} o.pred = (Ordinal.lift.{u, v} o).pred
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>Order.IsSuccLimit o
<VAR>o a : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>a < o → Order.succ a < o
<VAR>o : Ordinal.{u_4}<GOAL>¬(Order.succ o).IsLimit
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>¬∃ a, o = Order.succ a
<VAR>o a : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>Order.succ a < o ↔ a < o
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_4}<GOAL>o ≤ Order.succ a ↔ o ≤ a
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_4}<GOAL>o ≤ a ↔ ∀ x < o, x ≤ a
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_4}<GOAL>a < o ↔ ∃ x < o, a < x
<VAR>o : Ordinal.{v}<GOAL>(Ordinal.lift.{u, v} o).IsLimit ↔ o.IsLimit
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>0 < o
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>1 < o
<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>n : ℕ<GOAL>↑n < o
<VAR>o : Ordinal.{u_4}<GOAL>o = 0 ∨ (∃ a, o = Order.succ a) ∨ o.IsLimit
<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<GOAL>Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁
<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>o : Ordinal.{u_4}<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<GOAL>(Order.succ o).limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃)
<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>o : Ordinal.{u_4}<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (Order.succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<VAR>h : o.IsLimit<GOAL>o.limitRecOn H₁ H₂ H₃ = H₃ o h fun x _h => x.limitRecOn H₁ H₂ H₃
<VAR>o : Ordinal.{u_4}<GOAL>Ordinal.enum (fun x x_1 => x < x_1) o ⋯ = ⊤
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>h : ∀ a < Ordinal.type r, Order.succ a < Ordinal.type r<VAR>x : α<GOAL>∃ y, r x y
<VAR>o : Ordinal.{u_4}<VAR>ho : ∀ a < o, Order.succ a < o<GOAL>NoMaxOrder (Quotient.out o).α
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>hr : (Ordinal.type r).IsLimit<VAR>x : α<GOAL>Set.Bounded r {x}
<VAR>o : Ordinal.{u}<GOAL>Ordinal.type (Subrel (fun x x_1 => x < x_1) {o' | o' < o}) = Ordinal.lift.{u + 1, u} o
<VAR>o : Ordinal.{u}<GOAL>#↑{o' | o' < o} = Cardinal.lift.{u + 1, u} o.card
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u_4}<GOAL>o.IsLimit → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_5}<GOAL>a < f o ↔ ∃ b < o, a < f b
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<GOAL>StrictMono f
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<GOAL>Monotone f
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<GOAL>Ordinal.IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), o.IsLimit → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_4}<GOAL>f a < f b ↔ a < b
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_4}<GOAL>f a ≤ f b ↔ a ≤ b
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_4}<GOAL>f a = f b ↔ a = b
<VAR>f : Ordinal.{u_4} → Ordinal.{u_4}<VAR>H : Ordinal.IsNormal f<VAR>a : Ordinal.{u_4}<GOAL>a ≤ f a
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>o : Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>p : Set Ordinal.{u_4}<VAR>p0 : p.Nonempty<VAR>b : Ordinal.{u_4}<VAR>H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o<GOAL>f b ≤ o ↔ ∀ a ∈ p, f a ≤ o
<VAR>α : Type u_1<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>o : Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>p : Set α<VAR>p0 : p.Nonempty<VAR>g : α → Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o<GOAL>f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>g : Ordinal.{u_6} → Ordinal.{u_4}<VAR>H₁ : Ordinal.IsNormal f<VAR>H₂ : Ordinal.IsNormal g<GOAL>Ordinal.IsNormal (f ∘ g)
<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u_4}<VAR>l : o.IsLimit<GOAL>(f o).IsLimit
<VAR>f : Ordinal.{u_4} → Ordinal.{u_4}<VAR>H : Ordinal.IsNormal f<VAR>a : Ordinal.{u_4}<GOAL>f a ≤ a ↔ f a = a
<VAR>a b c : Ordinal.{u_4}<VAR>h : b.IsLimit<GOAL>a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c
<VAR>a : Ordinal.{u_4}<GOAL>Ordinal.IsNormal fun x => a + x
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<GOAL>b.IsLimit → (a + b).IsLimit
<VAR>a b : Ordinal.{u_4}<GOAL>{o | a ≤ b + o}.Nonempty
<VAR>a b : Ordinal.{u_4}<GOAL>a ≤ b + (a - b)
<VAR>a b c : Ordinal.{u_4}<GOAL>a - b ≤ c ↔ a ≤ b + c
<VAR>a b c : Ordinal.{u_4}<GOAL>a < b - c ↔ c + a < b
<VAR>a b : Ordinal.{u_4}<GOAL>a + b - a = b
<VAR>a b c : Ordinal.{u_4}<VAR>h : a + b = c<GOAL>c - a = b
<VAR>a b : Ordinal.{u_4}<GOAL>a - b ≤ a
<VAR>a b : Ordinal.{u_4}<VAR>h : b ≤ a<GOAL>b + (a - b) = a
<VAR>a b c : Ordinal.{u_4}<VAR>h : b ≤ a<GOAL>c ≤ a - b ↔ b + c ≤ a
<VAR>a b c : Ordinal.{u_4}<VAR>h : b ≤ a<GOAL>a - b < c ↔ a < b + c
<VAR>a : Ordinal.{u_4}<GOAL>a - 0 = a
<VAR>a : Ordinal.{u_4}<GOAL>0 - a = 0
<VAR>a : Ordinal.{u_4}<GOAL>a - a = 0
<VAR>a b : Ordinal.{u_4}<GOAL>a - b = 0 ↔ a ≤ b
<VAR>a b c : Ordinal.{u_4}<GOAL>a - b - c = a - (b + c)
<VAR>a b c : Ordinal.{u_4}<GOAL>a + b - (a + c) = b - c
<VAR>a b : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>h : b < a<GOAL>(a - b).IsLimit
<VAR>o : Ordinal.{u_4}<VAR>h : ω ≤ o<GOAL>1 + o = o
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<GOAL>Ordinal.type (Prod.Lex s r) = Ordinal.type r * Ordinal.type s
<VAR>a b : Ordinal.{u_4}<GOAL>a * b = 0 ↔ a = 0 ∨ b = 0
<VAR>a b : Ordinal.{v}<GOAL>Ordinal.lift.{u, v} (a * b) = Ordinal.lift.{u, v} a * Ordinal.lift.{u, v} b
<VAR>a b : Ordinal.{u_4}<GOAL>(a * b).card = a.card * b.card
<VAR>a b : Ordinal.{u_4}<GOAL>a * Order.succ b = a * b + a
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a ≤ a * b
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a ≤ b * a
<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (Ordinal.type s).IsLimit<VAR>H : ∀ b' < Ordinal.type s, Ordinal.type r * b' ≤ c<VAR>l : c < Ordinal.type r * Ordinal.type s<GOAL>False
<VAR>a b c : Ordinal.{u_4}<VAR>h : b.IsLimit<GOAL>a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c
<VAR>a : Ordinal.{u_4}<VAR>h : 0 < a<GOAL>Ordinal.IsNormal fun x => a * x
<VAR>a b c : Ordinal.{u_4}<VAR>h : c.IsLimit<GOAL>a < b * c ↔ ∃ c' < c, a < b * c'
<VAR>a b c : Ordinal.{u_4}<VAR>a0 : 0 < a<GOAL>a * b < a * c ↔ b < c
<VAR>a b c : Ordinal.{u_4}<VAR>a0 : 0 < a<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>a b c : Ordinal.{u_4}<VAR>h : a < b<VAR>c0 : 0 < c<GOAL>c * a < c * b
<VAR>a b : Ordinal.{u_4}<VAR>h₁ : 0 < a<VAR>h₂ : 0 < b<GOAL>0 < a * b
<VAR>a b : Ordinal.{u_4}<GOAL>a ≠ 0 → b ≠ 0 → a * b ≠ 0
<VAR>a b c : Ordinal.{u_4}<VAR>h : c * a ≤ c * b<VAR>h0 : 0 < c<GOAL>a ≤ b
<VAR>a b c : Ordinal.{u_4}<VAR>a0 : 0 < a<GOAL>a * b = a * c ↔ b = c
<VAR>a b : Ordinal.{u_4}<VAR>a0 : 0 < a<GOAL>b.IsLimit → (a * b).IsLimit
<VAR>a b : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>b0 : 0 < b<GOAL>(a * b).IsLimit
<VAR>n : ℕ<VAR>a : Ordinal.{u_4}<GOAL>n • a = a * ↑n
<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>{o | a < b * Order.succ o}.Nonempty
<VAR>a : Ordinal.{u_4}<GOAL>a / 0 = 0
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a / b = sInf {o | a < b * Order.succ o}
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a < b * Order.succ (a / b)
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a < b * (a / b) + b
<VAR>a b c : Ordinal.{u_4}<VAR>b0 : b ≠ 0<GOAL>a / b ≤ c ↔ a < b * Order.succ c
<VAR>a b c : Ordinal.{u_4}<VAR>h : c ≠ 0<GOAL>a < b / c ↔ c * Order.succ a ≤ b
<VAR>b c : Ordinal.{u_4}<VAR>h : c ≠ 0<GOAL>0 < b / c ↔ c ≤ b
<VAR>a b c : Ordinal.{u_4}<VAR>c0 : c ≠ 0<GOAL>a ≤ b / c ↔ c * a ≤ b
<VAR>a b c : Ordinal.{u_4}<VAR>b0 : b ≠ 0<GOAL>a / b < c ↔ a < b * c
<VAR>a b c : Ordinal.{u_4}<VAR>h : a ≤ b * c<GOAL>a / b ≤ c
<VAR>a b c : Ordinal.{u_4}<GOAL>a < b / c → c * a < b
<VAR>a : Ordinal.{u_4}<GOAL>0 / a = 0
<VAR>a b : Ordinal.{u_4}<GOAL>b * (a / b) ≤ a
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>c : Ordinal.{u_4}<GOAL>(b * a + c) / b = a + c / b
<VAR>a b : Ordinal.{u_4}<VAR>h : a < b<GOAL>a / b = 0
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<GOAL>b * a / b = a
<VAR>a : Ordinal.{u_4}<GOAL>a / 1 = a
<VAR>a : Ordinal.{u_4}<VAR>h : a ≠ 0<GOAL>a / a = 1
<VAR>a b c : Ordinal.{u_4}<GOAL>a * (b - c) = a * b - a * c
<VAR>a b : Ordinal.{u_4}<GOAL>(a + b).IsLimit ↔ b.IsLimit ∨ b = 0 ∧ a.IsLimit
<VAR>a b c : Ordinal.{u_4}<GOAL>a ∣ b → (a ∣ b + c ↔ a ∣ c)
<VAR>a b : Ordinal.{u_4}<GOAL>a ≠ 0 → a ∣ b → a * (b / a) = b
<VAR>a b : Ordinal.{u_4}<GOAL>b ≠ 0 → a ∣ b → a ≤ b
<VAR>a b : Ordinal.{u_4}<VAR>h₁ : a ∣ b<VAR>h₂ : b ∣ a<GOAL>a = b
<VAR>a b : Ordinal.{u_4}<GOAL>a % b = a - b * (a / b)
<VAR>a b : Ordinal.{u_4}<GOAL>a % b ≤ a
<VAR>a : Ordinal.{u_4}<GOAL>a % 0 = a
<VAR>a b : Ordinal.{u_4}<VAR>h : a < b<GOAL>a % b = a
<VAR>b : Ordinal.{u_4}<GOAL>0 % b = 0
<VAR>a b : Ordinal.{u_4}<GOAL>b * (a / b) + a % b = a
<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a % b < b
<VAR>a : Ordinal.{u_4}<GOAL>a % a = 0
<VAR>a : Ordinal.{u_4}<GOAL>a % 1 = 0
<VAR>a b : Ordinal.{u_4}<VAR>H : a % b = 0<GOAL>b ∣ a
<VAR>a b : Ordinal.{u_4}<VAR>H : b ∣ a<GOAL>a % b = 0
<VAR>a b : Ordinal.{u_4}<GOAL>b ∣ a ↔ a % b = 0
<VAR>x y z : Ordinal.{u_4}<GOAL>(x * y + z) % x = z % x
<VAR>x y : Ordinal.{u_4}<GOAL>x * y % x = 0
<VAR>a : Ordinal.{u_4}<VAR>b c : Ordinal.{u_4}<VAR>h : c ∣ b<GOAL>a % b % c = a % c
<VAR>a b : Ordinal.{u_4}<GOAL>a % b % b = a % b
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>f : ι → α<VAR>i : ι<GOAL>Ordinal.bfamilyOfFamily' r f (Ordinal.typein r i) ⋯ = f i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α<VAR>i : ι<GOAL>Ordinal.bfamilyOfFamily f (Ordinal.typein WellOrderingRel i) ⋯ = f i
<VAR>α : Type u_1<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>o : Ordinal.{u}<VAR>ho : Ordinal.type r = o<VAR>f : (a : Ordinal.{u}) → a < o → α<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>Ordinal.familyOfBFamily' r ho f (Ordinal.enum r i ⋯) = f i hi
<VAR>α : Type u_1<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → α<VAR>i : Ordinal.{u_4}<VAR>hi : i < o<GOAL>o.familyOfBFamily f (Ordinal.enum (fun x x_1 => x < x_1) i ⋯) = f i hi
<VAR>α : Type u_1<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → α<VAR>a : α<GOAL>a ∈ o.brange f ↔ ∃ i, ∃ (hi : i < o), f i hi = a
<VAR>α : Type u_1<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → α<VAR>i : Ordinal.{u_4}<VAR>hi : i < o<GOAL>f i hi ∈ o.brange f
<VAR>α : Type u_1<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>o : Ordinal.{u}<VAR>ho : Ordinal.type r = o<VAR>f : (a : Ordinal.{u}) → a < o → α<GOAL>Set.range (Ordinal.familyOfBFamily' r ho f) = o.brange f
<VAR>α : Type u_1<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → α<GOAL>Set.range (o.familyOfBFamily f) = o.brange f
<VAR>α : Type u_1<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>f : ι → α<GOAL>(Ordinal.type r).brange (Ordinal.bfamilyOfFamily' r f) = Set.range f
<VAR>α : Type u_1<VAR>ι : Type u<VAR>f : ι → α<GOAL>(Ordinal.type WellOrderingRel).brange (Ordinal.bfamilyOfFamily f) = Set.range f
<VAR>α : Type u_1<VAR>o : Ordinal.{u_4}<VAR>ho : o ≠ 0<VAR>c : α<GOAL>(o.brange fun x x => c) = {c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>f : ι → α<VAR>g : α → β<GOAL>(fun i hi => g (Ordinal.bfamilyOfFamily' r f i hi)) = Ordinal.bfamilyOfFamily' r (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u<VAR>f : ι → α<VAR>g : α → β<GOAL>(fun i hi => g (Ordinal.bfamilyOfFamily f i hi)) = Ordinal.bfamilyOfFamily (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>o : Ordinal.{u}<VAR>ho : Ordinal.type r = o<VAR>f : (a : Ordinal.{u}) → a < o → α<VAR>g : α → β<GOAL>g ∘ Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun i hi => g (f i hi)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → α<VAR>g : α → β<GOAL>g ∘ o.familyOfBFamily f = o.familyOfBFamily fun i hi => g (f i hi)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>sSup (Set.range f) = Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>BddAbove (Set.range f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>i : ι<GOAL>f i ≤ Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>Ordinal.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i ≤ a) → Ordinal.sup f ≤ a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < Ordinal.sup f ↔ ∃ i, a < f i
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(∀ (i : ι), f i ≠ Ordinal.sup f) ↔ ∀ (i : ι), f i < Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ (i : ι), f i ≠ Ordinal.sup f<VAR>a : Ordinal.{max u v}<VAR>hao : a < Ordinal.sup f<GOAL>Order.succ a < Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>f : Ordinal.{max u v} → Ordinal.{max u w}<VAR>H : Ordinal.IsNormal f<VAR>ι : Type u<VAR>g : ι → Ordinal.{max u v}<VAR>Nonempty ι<GOAL>f (Ordinal.sup g) = Ordinal.sup (f ∘ g)
<VAR>ι : Type u_4<VAR>IsEmpty ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>Ordinal.sup f = 0
<VAR>ι : Type u_4<VAR>_hι : Nonempty ι<VAR>o : Ordinal.{max u_5 u_4}<GOAL>(Ordinal.sup fun x => o) = o
<VAR>ι : Type u_4<VAR>Unique ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>Ordinal.sup f = f default
<VAR>ι : Type u<VAR>ι' : Type v<VAR>f : ι → Ordinal.{max (max u v) w}<VAR>g : ι' → Ordinal.{max (max u v) w}<VAR>h : Set.range f ⊆ Set.range g<GOAL>Ordinal.sup f ≤ Ordinal.sup g
<VAR>ι : Type u<VAR>ι' : Type v<VAR>f : ι → Ordinal.{max (max u v) w}<VAR>g : ι' → Ordinal.{max (max u v) w}<VAR>h : Set.range f = Set.range g<GOAL>Ordinal.sup f = Ordinal.sup g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>Ordinal.sup f = max (Ordinal.sup fun a => f (Sum.inl a)) (Ordinal.sup fun b => f (Sum.inr b))
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : β → α<VAR>h : Ordinal.type r ≤ Ordinal.sup (Ordinal.typein r ∘ f)<GOAL>Set.Unbounded r (Set.range f)
<VAR>s : Set Ordinal.{u}<VAR>hs : Small.{u, u + 1} ↑s<VAR>a : Ordinal.{u}<VAR>ha : a ∈ s<GOAL>a ≤ Ordinal.sup fun x => ↑((equivShrink ↑s).symm x)
<VAR>s : Set Ordinal.{u}<GOAL>BddAbove s ↔ Small.{u, u + 1} ↑s
<VAR>s : Set Ordinal.{u}<VAR>h : Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>s : Set Ordinal.{u}<VAR>hs : Small.{u, u + 1} ↑s<GOAL>(Ordinal.sup fun x => ↑((equivShrink ↑s).symm x)) = sSup s
<VAR>s : Set Cardinal.{u}<VAR>hs : BddAbove s<GOAL>(sSup s).ord = sSup (Cardinal.ord '' s)
<VAR>ι : Sort u_4<VAR>f : ι → Cardinal.{u_5}<VAR>hf : BddAbove (Set.range f)<GOAL>(iSup f).ord = ⨆ i, (f i).ord
<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>IsWellOrder ι r<VAR>IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : Ordinal.type r = o<VAR>ho' : Ordinal.type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Ordinal.sup (Ordinal.familyOfBFamily' r ho f) ≤ Ordinal.sup (Ordinal.familyOfBFamily' r' ho' f)
<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>IsWellOrder ι r<VAR>IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : Ordinal.type r = o<VAR>ho' : Ordinal.type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = Ordinal.sup (Ordinal.familyOfBFamily' r' ho' f)
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Ordinal.sup (o.familyOfBFamily f) = o.bsup f
<VAR>o : Ordinal.{u}<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>ho : Ordinal.type r = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Ordinal.sup (Ordinal.familyOfBFamily' r ho f) = o.bsup f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>sSup (o.brange f) = o.bsup f
<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = Ordinal.sup f