ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<VAR>hn : 1 ≤ n<GOAL>Continuous fun x => fderiv 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<VAR>hn : 1 ≤ n<GOAL>Continuous fun p => (fderiv 𝕜 f p.1) p.2
<VAR>a : Ordinal.{u}<GOAL>IsOpen {a} ↔ ¬a.IsLimit
<VAR>a : Ordinal.{u_1}<GOAL>𝓝[>] a = ⊥
<VAR>a : Ordinal.{u_1}<GOAL>𝓝[<] a = 𝓝[≠] a
<VAR>a : Ordinal.{u_1}<GOAL>𝓝[≤] a = 𝓝 a
<VAR>a : Ordinal.{u}<VAR>h : a ≠ 0<GOAL>(𝓝 a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
<VAR>a : Ordinal.{u}<GOAL>𝓝 a = pure a ↔ ¬a.IsLimit
<VAR>s : Set Ordinal.{u}<GOAL>IsOpen s ↔ ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
<VAR>a : Ordinal.{u}<VAR>s : Set Ordinal.{u}<GOAL>[a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a, ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a].TFAE
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : IsClosed s<GOAL>a ∈ s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>a ∈ closure s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
<VAR>s : Set Ordinal.{u}<GOAL>IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → Ordinal.sup f ∈ s
<VAR>s : Set Ordinal.{u}<GOAL>IsClosed s ↔ ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
<VAR>f : Ordinal.{u} → Ordinal.{u}<GOAL>Ordinal.IsNormal f ↔ StrictMono f ∧ Continuous f
<VAR>s : Set Ordinal.{u}<VAR>hs : Set.Unbounded (fun x x_1 => x < x_1) s<GOAL>Ordinal.IsNormal (Ordinal.enumOrd s) ↔ IsClosed s
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<GOAL>Quiver.Hom.cast hu hv e = cast ⋯ e
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v : U<VAR>e : u ⟶ v<GOAL>Quiver.Hom.cast ⋯ ⋯ e = e
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' u'' v'' : U<VAR>e : u ⟶ v<VAR>hu : u = u'<VAR>hv : v = v'<VAR>hu' : u' = u''<VAR>hv' : v' = v''<GOAL>Quiver.Hom.cast hu' hv' (Quiver.Hom.cast hu hv e) = Quiver.Hom.cast ⋯ ⋯ e
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<GOAL>HEq (Quiver.Hom.cast hu hv e) e
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>Quiver.Hom.cast hu hv e = e' ↔ HEq e e'
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>e' = Quiver.Hom.cast hu hv e ↔ HEq e' e
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Quiver.Path u v<GOAL>Quiver.Path.cast hu hv p = cast ⋯ p
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v : U<VAR>p : Quiver.Path u v<GOAL>Quiver.Path.cast ⋯ ⋯ p = p
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' u'' v'' : U<VAR>p : Quiver.Path u v<VAR>hu : u = u'<VAR>hv : v = v'<VAR>hu' : u' = u''<VAR>hv' : v' = v''<GOAL>Quiver.Path.cast hu' hv' (Quiver.Path.cast hu hv p) = Quiver.Path.cast ⋯ ⋯ p
<VAR>U : Type u_1<VAR>Quiver U<VAR>u u' : U<VAR>hu : u = u'<GOAL>Quiver.Path.cast hu hu Quiver.Path.nil = Quiver.Path.nil
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Quiver.Path u v<GOAL>HEq (Quiver.Path.cast hu hv p) p
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Quiver.Path u v<VAR>p' : Quiver.Path u' v'<GOAL>Quiver.Path.cast hu hv p = p' ↔ HEq p p'
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Quiver.Path u v<VAR>p' : Quiver.Path u' v'<GOAL>p' = Quiver.Path.cast hu hv p ↔ HEq p' p
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v w u' w' : U<VAR>p : Quiver.Path u v<VAR>e : v ⟶ w<VAR>hu : u = u'<VAR>hw : w = w'<GOAL>Quiver.Path.cast hu hw (p.cons e) = (Quiver.Path.cast hu ⋯ p).cons (Quiver.Hom.cast ⋯ hw e)
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v v' w : U<VAR>p : Quiver.Path u v<VAR>p' : Quiver.Path u v'<VAR>e : v ⟶ w<VAR>e' : v' ⟶ w<VAR>h : p.cons e = p'.cons e'<GOAL>Quiver.Path.cast ⋯ ⋯ p = p'
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v v' w : U<VAR>p : Quiver.Path u v<VAR>p' : Quiver.Path u v'<VAR>e : v ⟶ w<VAR>e' : v' ⟶ w<VAR>h : p.cons e = p'.cons e'<GOAL>Quiver.Hom.cast ⋯ ⋯ e = e'
<VAR>U : Type u_1<VAR>Quiver U<VAR>u v : U<VAR>p : Quiver.Path u v<VAR>hzero : p.length = 0<GOAL>Quiver.Path.cast ⋯ ⋯ p = Quiver.Path.nil
<VAR>V : Type u_2<VAR>Quiver V<VAR>self : Quiver.HasInvolutiveReverse V<VAR>a b : V<VAR>f : a ⟶ b<GOAL>Quiver.reverse (Quiver.reverse f) = f
<VAR>V : Type u_2<VAR>Quiver V<VAR>h : Quiver.HasInvolutiveReverse V<VAR>a b : V<VAR>f : a ⟶ b<GOAL>Quiver.reverse (Quiver.reverse f) = f
<VAR>V : Type u_2<VAR>Quiver V<VAR>h : Quiver.HasInvolutiveReverse V<VAR>a b : V<VAR>f g : a ⟶ b<GOAL>Quiver.reverse f = Quiver.reverse g ↔ f = g
<VAR>V : Type u_2<VAR>Quiver V<VAR>h : Quiver.HasInvolutiveReverse V<VAR>a b : V<VAR>f : a ⟶ b<VAR>g : b ⟶ a<GOAL>f = Quiver.reverse g ↔ Quiver.reverse f = g
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>Quiver.HasReverse U<VAR>Quiver.HasReverse V<VAR>φ : U ⥤q V<VAR>self : φ.MapReverse<VAR>u v : U<VAR>e : u ⟶ v<GOAL>φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>Quiver.HasReverse U<VAR>Quiver.HasReverse V<VAR>φ : U ⥤q V<VAR>φ.MapReverse<VAR>u v : U<VAR>e : u ⟶ v<GOAL>φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
<VAR>V : Type u_2<VAR>Quiver V<VAR>a b : Quiver.Symmetrify V<VAR>e : a ⟶ b<GOAL>Quiver.reverse e = Sum.swap e
<VAR>V : Type u_2<VAR>Quiver V<VAR>Quiver.HasReverse V<VAR>a b : V<VAR>f : a ⟶ b<GOAL>f.toPath.reverse = (Quiver.reverse f).toPath
<VAR>V : Type u_2<VAR>Quiver V<VAR>Quiver.HasReverse V<VAR>a b c : V<VAR>p : Quiver.Path a b<VAR>q : Quiver.Path b c<GOAL>(p.comp q).reverse = q.reverse.comp p.reverse
<VAR>V : Type u_2<VAR>Quiver V<VAR>h : Quiver.HasInvolutiveReverse V<VAR>a b : V<VAR>p : Quiver.Path a b<GOAL>p.reverse.reverse = p
<VAR>V : Type u_2<VAR>Quiver V<VAR>V' : Type u_4<VAR>Quiver V'<VAR>Quiver.HasReverse V'<VAR>φ : V ⥤q V'<GOAL>Quiver.Symmetrify.of ⋙q Quiver.Symmetrify.lift φ = φ
<VAR>V : Type u_2<VAR>Quiver V<VAR>V' : Type u_4<VAR>Quiver V'<VAR>h : Quiver.HasInvolutiveReverse V'<VAR>φ : V ⥤q V'<VAR>X Y : Quiver.Symmetrify V<VAR>f : X ⟶ Y<GOAL>(Quiver.Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Quiver.Symmetrify.lift φ).map f)
<VAR>V : Type u_2<VAR>Quiver V<VAR>V' : Type u_4<VAR>Quiver V'<VAR>Quiver.HasReverse V'<VAR>φ : V ⥤q V'<VAR>Φ : Quiver.Symmetrify V ⥤q V'<VAR>hΦ : Quiver.Symmetrify.of ⋙q Φ = φ<VAR>hΦinv : ∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)<GOAL>Φ = Quiver.Symmetrify.lift φ
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>φ : U ⥤q V<GOAL>∀ {X Y : Quiver.Symmetrify U} (a : (X ⟶ Y) ⊕ (Y ⟶ X)), φ.symmetrify.map a = Sum.map φ.map φ.map a
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>φ : U ⥤q V<GOAL>∀ (a : U), φ.symmetrify.obj a = φ.obj a
<VAR>V : Type u_2<VAR>Quiver V<VAR>V' : Type u_4<VAR>σ : V → V'<VAR>Quiver.HasInvolutiveReverse V<VAR>X Y : V<VAR>f : X ⟶ Y<GOAL>Quiver.reverse ((Quiver.Push.of σ).map f) = (Quiver.Push.of σ).map (Quiver.reverse f)
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal op o ↔ Ordinal.Principal (Function.swap op) o
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.Principal op 0
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.Principal op 1 ↔ op 0 0 = 0
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<VAR>a o : Ordinal.{u_1}<VAR>hao : a < o<VAR>ho : Ordinal.Principal op o<VAR>n : ℕ<GOAL>(op a)^[n] a < o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>a o : Ordinal.{u}<VAR>hao : a < o<VAR>H : Ordinal.IsNormal (op a)<VAR>ho : Ordinal.Principal op o<VAR>ho' : o.IsLimit<GOAL>op a o = o
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<VAR>a o : Ordinal.{u_1}<VAR>hao : a < o<VAR>ho : Ordinal.Principal op o<GOAL>Ordinal.nfp (op a) a ≤ o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>Ordinal.Principal op (Ordinal.nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o)
<VAR>op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Set.Unbounded (fun x x_1 => x < x_1) {o | Ordinal.Principal op o}
<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) 1
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≤ 1<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) o
<VAR>o : Ordinal.{u_1}<VAR>ho₁ : 1 < o<VAR>ho : Ordinal.Principal (fun x x_1 => x + x_1) o<GOAL>o.IsLimit
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) o ↔ ∀ a < o, a + o = o
<VAR>a : Ordinal.{u_1}<VAR>ha : ¬Ordinal.Principal (fun x x_1 => x + x_1) a<GOAL>∃ b c, b < a ∧ c < a ∧ b + c = a
<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) a ↔ ∀ ⦃b c : Ordinal.{u_1}⦄, b < a → c < a → b + c ≠ a
<VAR>a : Ordinal.{u_1}<VAR>h : a < Ordinal.omega<GOAL>a + Ordinal.omega = Ordinal.omega
<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) Ordinal.omega
<VAR>a b : Ordinal.{u_1}<VAR>h : a < Ordinal.omega ^ b<GOAL>a + Ordinal.omega ^ b = Ordinal.omega ^ b
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) (Ordinal.omega ^ o)
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = Ordinal.omega ^ a
<VAR>a : Ordinal.{u_1}<VAR>ha : Ordinal.Principal (fun x x_1 => x + x_1) a<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) (a ^ b)
<VAR>a b c : Ordinal.{u_1}<VAR>h₁ : a < Ordinal.omega ^ b<VAR>h₂ : Ordinal.omega ^ b ≤ c<GOAL>a + c = c
<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{u}<VAR>hb₁ : b ≠ 1<VAR>hb : Ordinal.Principal (fun x x_1 => x + x_1) b<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) (a * b)
<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) 1
<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) 2
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≤ 2<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) o
<VAR>o : Ordinal.{u_1}<VAR>ho : Ordinal.Principal (fun x x_1 => x * x_1) o<VAR>ho₂ : o ≠ 2<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) o
<VAR>o : Ordinal.{u}<VAR>ho₂ : 2 < o<VAR>ho : Ordinal.Principal (fun x x_1 => x * x_1) o<GOAL>o.IsLimit
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) o ↔ ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) Ordinal.omega
<VAR>a : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>ha : a < Ordinal.omega<GOAL>a * Ordinal.omega = Ordinal.omega
<VAR>a b c : Ordinal.{u_1}<VAR>c0 : 0 < c<VAR>ha : a < Ordinal.omega ^ c<VAR>hb : b < Ordinal.omega<GOAL>a * b < Ordinal.omega ^ c
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h : a < Ordinal.omega ^ Ordinal.omega ^ b<GOAL>a * Ordinal.omega ^ Ordinal.omega ^ b = Ordinal.omega ^ Ordinal.omega ^ b
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) (Ordinal.omega ^ Ordinal.omega ^ o)
<VAR>o b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : Ordinal.Principal (fun x x_1 => x * x_1) (b ^ o)<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) o
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x * x_1) o ↔ o ≤ 2 ∨ ∃ a, o = Ordinal.omega ^ Ordinal.omega ^ a
<VAR>a : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>ha : a < Ordinal.omega<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.omega ∣ b → a * b = b
<VAR>a b : Ordinal.{u}<VAR>ha : a ≠ 0<VAR>hb : Ordinal.Principal (fun x x_1 => x * x_1) b<VAR>hb₂ : 2 < b<GOAL>a * b = b ^ Order.succ (Ordinal.log b a)
<GOAL>Ordinal.Principal (fun x x_1 => x ^ x_1) Ordinal.omega
<VAR>a : Ordinal.{u_1}<VAR>a1 : 1 < a<VAR>h : a < Ordinal.omega<GOAL>a ^ Ordinal.omega = Ordinal.omega
<VAR>p : Cardinal.{u_1} → Prop<VAR>c : Cardinal.{u_1}<VAR>h : ∀ (α : Type u_1), p (Cardinal.mk α)<GOAL>p c
<VAR>p : Cardinal.{u_1} → Cardinal.{u_2} → Prop<VAR>c₁ : Cardinal.{u_1}<VAR>c₂ : Cardinal.{u_2}<VAR>h : ∀ (α : Type u_1) (β : Type u_2), p (Cardinal.mk α) (Cardinal.mk β)<GOAL>p c₁ c₂
<VAR>p : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop<VAR>c₁ : Cardinal.{u_1}<VAR>c₂ : Cardinal.{u_2}<VAR>c₃ : Cardinal.{u_3}<VAR>h : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (Cardinal.mk α) (Cardinal.mk β) (Cardinal.mk γ)<GOAL>p c₁ c₂ c₃
<VAR>α β : Type u<GOAL>Cardinal.mk α = Cardinal.mk β ↔ Nonempty (α ≃ β)
<VAR>α : Type u<GOAL>⟦α⟧ = Cardinal.mk α
<VAR>c : Cardinal.{u_1}<GOAL>Cardinal.mk (Quotient.out c) = c
<VAR>α β : Type u<VAR>e : α ≃ β<GOAL>Cardinal.mk α = Cardinal.mk β
<VAR>f : Type u → Type v<VAR>hf : (α β : Type u) → α ≃ β → f α ≃ f β<VAR>α : Type u<GOAL>Cardinal.map f hf (Cardinal.mk α) = Cardinal.mk (f α)
<VAR>α : Type u<GOAL>Cardinal.mk (ULift.{v, u} α) = Cardinal.lift.{v, u} (Cardinal.mk α)
<GOAL>Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u}
<GOAL>Cardinal.lift.{max v u, u} = Cardinal.lift.{v, u}
<VAR>a : Cardinal.{max u v}<GOAL>Cardinal.lift.{u, max u v} a = a
<VAR>a : Cardinal.{u}<GOAL>Cardinal.lift.{u, u} a = a
<VAR>a : Cardinal.{u}<GOAL>Cardinal.lift.{0, u} a = a
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.lift.{w, max v u_1} (Cardinal.lift.{v, u_1} a) = Cardinal.lift.{max v w, u_1} a
<VAR>α β : Type u<GOAL>Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (α ↪ β)
<VAR>α β : Type u<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Cardinal.mk α ≤ Cardinal.mk β
<VAR>α β : Type u<VAR>f : α ↪ β<GOAL>Cardinal.mk α ≤ Cardinal.mk β
<VAR>α β : Type u<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Cardinal.mk β ≤ Cardinal.mk α
<VAR>c : Cardinal.{u}<VAR>α : Type u<GOAL>c ≤ Cardinal.mk α ↔ ∃ p, Cardinal.mk ↑p = c
<VAR>α : Type u<VAR>p : α → Prop<GOAL>Cardinal.mk (Subtype p) ≤ Cardinal.mk α
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑s ≤ Cardinal.mk α
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑(ULift.down ⁻¹' s) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
<VAR>c c' : Cardinal.{u_1}<GOAL>c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')
<VAR>α : Type v<VAR>β : Type w<GOAL>Cardinal.lift.{max u w, v} (Cardinal.mk α) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk β) ↔ Nonempty (α ↪ β)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ↪ β)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)
<VAR>a b : Cardinal.{v}<GOAL>Cardinal.lift.{u, v} a ≤ Cardinal.lift.{u, v} b ↔ a ≤ b
<GOAL>⇑Cardinal.liftOrderEmbedding = Cardinal.lift.{u, v}
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} a = Cardinal.lift.{v, u} b ↔ a = b
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} a < Cardinal.lift.{v, u} b ↔ a < b
<GOAL>StrictMono Cardinal.lift.{u_2, u_1}
<VAR>α : Type u<VAR>IsEmpty α<GOAL>Cardinal.mk α = 0
<GOAL>Cardinal.lift.{u_2, u_1} 0 = 0
<VAR>a : Cardinal.{v}<GOAL>Cardinal.lift.{u, v} a = 0 ↔ a = 0
<VAR>α : Type u<GOAL>Cardinal.mk α = 0 ↔ IsEmpty α
<VAR>α : Type u<GOAL>Cardinal.mk α ≠ 0 ↔ Nonempty α
<VAR>α : Type u<VAR>Nonempty α<GOAL>Cardinal.mk α ≠ 0
<VAR>α : Type u<VAR>Unique α<GOAL>Cardinal.mk α = 1
<VAR>α : Type u<GOAL>Cardinal.mk α ≤ 1 ↔ Subsingleton α
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑s ≤ 1 ↔ s.Subsingleton
<VAR>α β : Type u<GOAL>Cardinal.mk α + Cardinal.mk β = Cardinal.mk (α ⊕ β)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.mk (α ⊕ β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)
<VAR>α : Type u<GOAL>Cardinal.mk (Option α) = Cardinal.mk α + 1
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.mk (α ⊕' β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)
<VAR>α : Type u<VAR>h : Fintype α<GOAL>Cardinal.mk α = ↑(Fintype.card α)
<VAR>n : ℕ<GOAL>↑(n + 1) = ↑n + 1
<VAR>α β : Type u<GOAL>Cardinal.mk α * Cardinal.mk β = Cardinal.mk (α × β)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.mk (α × β) = Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} (Cardinal.mk β)
<VAR>a b : Cardinal.{u}<GOAL>a * b = b * a
<VAR>α β : Type u<GOAL>Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)
<VAR>α : Type u<VAR>β : Type v<GOAL>Cardinal.mk (α → β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Cardinal.lift.{v, u} (Cardinal.mk α)
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} (a ^ b) = Cardinal.lift.{v, u} a ^ Cardinal.lift.{v, u} b
<VAR>a : Cardinal.{u_1}<GOAL>a ^ 0 = 1
<VAR>a : Cardinal.{u}<GOAL>a ^ 1 = a
<VAR>a b c : Cardinal.{u_1}<GOAL>a ^ (b + c) = a ^ b * a ^ c
<VAR>a : Cardinal.{u_1}<GOAL>1 ^ a = 1
<VAR>a : Cardinal.{u_1}<GOAL>a ≠ 0 → 0 ^ a = 0
<VAR>a : Cardinal.{u_1}<VAR>b : Cardinal.{u_1}<GOAL>a ≠ 0 → a ^ b ≠ 0
<VAR>a b c : Cardinal.{u_1}<GOAL>(a * b) ^ c = a ^ c * b ^ c
<VAR>a b c : Cardinal.{u_1}<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>a ^ ↑n = a ^ n
<GOAL>Cardinal.lift.{u_2, u_1} 1 = 1
<VAR>a : Cardinal.{v}<GOAL>Cardinal.lift.{u, v} a = 1 ↔ a = 1
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} (a + b) = Cardinal.lift.{v, u} a + Cardinal.lift.{v, u} b
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} (a * b) = Cardinal.lift.{v, u} a * Cardinal.lift.{v, u} b
<VAR>α : Type u<GOAL>Cardinal.mk (Set α) = 2 ^ Cardinal.mk α
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑(𝒫 s) = 2 ^ Cardinal.mk ↑s
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.lift.{v, u_1} (2 ^ a) = 2 ^ Cardinal.lift.{v, u_1} a
<VAR>a : Cardinal.{u_1}<GOAL>0 ≤ a
<VAR>a b c d : Cardinal.{u_1}<GOAL>a ≤ b → c ≤ d → a + c ≤ b + d
<VAR>c : Cardinal.{u}<GOAL>0 ^ c ≤ 1
<VAR>a b c : Cardinal.{u_1}<GOAL>a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c
<VAR>a : Cardinal.{u_1}<VAR>b : Cardinal.{u_1}<VAR>hb : 1 ≤ b<GOAL>a ≤ a ^ b
<VAR>a : Cardinal.{u}<GOAL>a < 2 ^ a
<VAR>α : Type u<GOAL>1 < Cardinal.mk α ↔ Nontrivial α
<VAR>a b c : Cardinal.{u_1}<VAR>h : b ≤ c<GOAL>a ^ b ≤ max (a ^ c) 1
<VAR>a b c : Cardinal.{u_1}<GOAL>a ≤ b → a ^ c ≤ b ^ c
<VAR>a : Cardinal.{u_1}<VAR>b : Cardinal.{u_1}<VAR>ha : 0 < a<GOAL>0 < a ^ b
<VAR>s : Set Cardinal.{u_1}<GOAL>sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0
<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{u_2}<GOAL>⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0
<VAR>c : Cardinal.{u_1}<GOAL>Order.succ c = sInf {c' | c < c'}
<VAR>c : Cardinal.{u_1}<GOAL>0 < Order.succ c
<VAR>c : Cardinal.{u_1}<GOAL>Order.succ c ≠ 0
<VAR>c : Cardinal.{u}<GOAL>c + 1 ≤ Order.succ c
<VAR>c : Cardinal.{u_1}<VAR>h : c.IsLimit<GOAL>c ≠ 0
<VAR>c : Cardinal.{u_1}<VAR>h : c.IsLimit<GOAL>Order.IsSuccLimit c
<VAR>x c : Cardinal.{u_1}<VAR>h : c.IsLimit<GOAL>x < c → Order.succ x < c
<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{max u_1 u_2}<VAR>i : ι<GOAL>f i ≤ Cardinal.sum f
<VAR>ι : Type u_2<VAR>f : ι → Type u_1<GOAL>Cardinal.mk ((i : ι) × f i) = Cardinal.sum fun i => Cardinal.mk (f i)
<VAR>ι : Type u<VAR>a : Cardinal.{v}<GOAL>(Cardinal.sum fun x => a) = Cardinal.lift.{v, u} (Cardinal.mk ι) * Cardinal.lift.{u, v} a
<VAR>ι : Type u<VAR>a : Cardinal.{u}<GOAL>(Cardinal.sum fun x => a) = Cardinal.mk ι * a
<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<GOAL>Cardinal.sum (f + g) = Cardinal.sum f + Cardinal.sum g
<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<GOAL>(Cardinal.sum fun i => f i + g i) = Cardinal.sum f + Cardinal.sum g
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<GOAL>Cardinal.lift.{w, max v u} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w, v} (f i)
<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i ≤ g i<GOAL>Cardinal.sum f ≤ Cardinal.sum g
<VAR>α β : Type u<VAR>c : Cardinal.{u}<VAR>f : α → β<VAR>hf : ∀ (b : β), Cardinal.mk ↑(f ⁻¹' {b}) ≤ c<GOAL>Cardinal.mk α ≤ Cardinal.mk β * c
<VAR>α : Type u<VAR>β : Type v<VAR>c : Cardinal.{max u v}<VAR>f : α → β<VAR>hf : ∀ (b : β), Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' {b})) ≤ c<GOAL>Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) * c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<GOAL>BddAbove (Set.range f)
<VAR>s : Set Cardinal.{u}<GOAL>BddAbove s ↔ Small.{u, u + 1} ↑s
<VAR>s : Set Cardinal.{u}<VAR>h : Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>f : Cardinal.{u} → Cardinal.{max u v}<VAR>s : Set Cardinal.{u}<VAR>hs : BddAbove s<GOAL>BddAbove (f '' s)
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (Set.range f)<VAR>g : Cardinal.{v} → Cardinal.{max v w}<GOAL>BddAbove (Set.range (g ∘ f))
<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{max u_1 u_2}<GOAL>iSup f ≤ Cardinal.sum f
<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<GOAL>Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * iSup f
<VAR>ι : Type u<VAR>f : ι → Cardinal.{u}<GOAL>Cardinal.sum f ≤ Cardinal.mk ι * iSup f
<VAR>f : ℕ → Cardinal.{u}<GOAL>Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1)
<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{u_2}<VAR>IsEmpty ι<GOAL>iSup f = 0
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>ω : Cardinal.{v}<VAR>hω : ¬Order.IsSuccLimit ω<VAR>h : ⨆ i, f i = ω<GOAL>∃ i, f i = ω
<VAR>ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (Set.range f)<VAR>ω : Cardinal.{v}<VAR>hω : ¬ω.IsLimit<VAR>h : ⨆ i, f i = ω<GOAL>∃ i, f i = ω
<VAR>α : Type u<VAR>Small.{v, u} α<GOAL>Cardinal.lift.{max u w, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)
<VAR>α : Type u<VAR>Small.{v, u} α<GOAL>Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{v, u} (Cardinal.mk α)
<VAR>α : Type (max u v)<VAR>Small.{v, max u v} α<GOAL>Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, max u v} α)) = Cardinal.mk α
<VAR>ι : Type u<VAR>α : ι → Type v<GOAL>Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun i => Cardinal.mk (α i)
<VAR>ι : Type u<VAR>a : Cardinal.{v}<GOAL>(Cardinal.prod fun x => a) = Cardinal.lift.{u, v} a ^ Cardinal.lift.{v, u} (Cardinal.mk ι)
<VAR>ι : Type u<VAR>a : Cardinal.{u}<GOAL>(Cardinal.prod fun x => a) = a ^ Cardinal.mk ι
<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i ≤ g i<GOAL>Cardinal.prod f ≤ Cardinal.prod g
<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{u}<GOAL>Cardinal.prod f = 0 ↔ ∃ i, f i = 0
<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{u_2}<GOAL>Cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
<VAR>ι : Type u<VAR>c : ι → Cardinal.{v}<GOAL>Cardinal.lift.{w, max v u} (Cardinal.prod c) = Cardinal.prod fun i => Cardinal.lift.{w, v} (c i)
<VAR>α : Type u<VAR>h : Fintype α<VAR>f : α → Cardinal.{v}<GOAL>Cardinal.prod f = Cardinal.lift.{u, v} (∏ i : α, f i)
<VAR>s : Set Cardinal.{v}<GOAL>Cardinal.lift.{u, v} (sInf s) = sInf (Cardinal.lift.{u, v} '' s)
<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{v}<GOAL>Cardinal.lift.{u, v} (iInf f) = ⨅ i, Cardinal.lift.{u, v} (f i)
<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{max u v}<GOAL>b ≤ Cardinal.lift.{v, u} a → ∃ a', Cardinal.lift.{v, u} a' = b
<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{max u v}<GOAL>b ≤ Cardinal.lift.{v, u} a ↔ ∃ a', Cardinal.lift.{v, u} a' = b ∧ a' ≤ a
<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{max u v}<GOAL>b < Cardinal.lift.{v, u} a ↔ ∃ a', Cardinal.lift.{v, u} a' = b ∧ a' < a
<VAR>a : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} (Order.succ a) = Order.succ (Cardinal.lift.{v, u} a)
<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{v}<GOAL>Cardinal.lift.{max v w, u} a = Cardinal.lift.{max u w, v} b ↔ Cardinal.lift.{v, u} a = Cardinal.lift.{u, v} b
<VAR>a b : Cardinal.{v}<GOAL>Cardinal.lift.{u, v} (min a b) = min (Cardinal.lift.{u, v} a) (Cardinal.lift.{u, v} b)
<VAR>a b : Cardinal.{v}<GOAL>Cardinal.lift.{u, v} (max a b) = max (Cardinal.lift.{u, v} a) (Cardinal.lift.{u, v} b)
<VAR>s : Set Cardinal.{u_1}<VAR>hs : BddAbove s<GOAL>Cardinal.lift.{u, u_1} (sSup s) = sSup (Cardinal.lift.{u, u_1} '' s)
<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (Set.range f)<GOAL>Cardinal.lift.{u, w} (iSup f) = ⨆ i, Cardinal.lift.{u, w} (f i)
<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>t : Cardinal.{max u w}<VAR>hf : BddAbove (Set.range f)<VAR>w : ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t<GOAL>Cardinal.lift.{u, w} (iSup f) ≤ t