ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>r r' : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>IsWellOrder ι r'<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').bsup (Ordinal.bfamilyOfFamily' r' f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type WellOrderingRel).bsup (Ordinal.bfamilyOfFamily f) = Ordinal.sup f
<VAR>o₁ o₂ : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}<VAR>ho : o₁ = o₂<GOAL>o₁.bsup f = o₂.bsup fun a h => f a ⋯
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → o.bsup f ≤ a
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<VAR>i : Ordinal.{u_4}<VAR>h : i < o<GOAL>f i h ≤ o.bsup f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi
<VAR>f : Ordinal.{max u v} → Ordinal.{max u w}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u}<VAR>g : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o ≠ 0 → f (o.bsup g) = o.bsup fun a h => f (g a h)
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (h : i < o), f i h ≠ o.bsup f) ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f<VAR>a : Ordinal.{max u v}<GOAL>a < o.bsup f → Order.succ a < o.bsup f
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<GOAL>o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha'<VAR>ho : ∀ a < o, Order.succ a < o<VAR>i : Ordinal.{u_4}<VAR>h : i < o<GOAL>f i h < o.bsup f
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < Order.succ o → Ordinal.{max u_4 u_5}<VAR>hf : ∀ {i j : Ordinal.{u_4}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj<GOAL>(Order.succ o).bsup f = f o ⋯
<VAR>f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}<GOAL>Ordinal.bsup 0 f = 0
<VAR>o : Ordinal.{u}<VAR>ho : o ≠ 0<VAR>a : Ordinal.{max u v}<GOAL>(o.bsup fun x x => a) = a
<VAR>f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}<GOAL>Ordinal.bsup 1 f = f 0 ⋯
<VAR>o : Ordinal.{u}<VAR>o' : Ordinal.{v}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}<VAR>g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}<VAR>h : o.brange f ⊆ o'.brange g<GOAL>o.bsup f ≤ o'.bsup g
<VAR>o : Ordinal.{u}<VAR>o' : Ordinal.{v}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}<VAR>g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}<VAR>h : o.brange f = o'.brange g<GOAL>o.bsup f = o'.bsup g
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup (Order.succ ∘ f) = Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<GOAL>Ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a
<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>a : Ordinal.{max u_5 u_4}<GOAL>(∀ (i : ι), f i < a) → Ordinal.lsub f ≤ a
<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>i : ι<GOAL>f i < Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<GOAL>a < Ordinal.lsub f ↔ ∃ i, a ≤ f i
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup f ≤ Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.lsub f ≤ Order.succ (Ordinal.sup f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup f = Ordinal.lsub f ∨ Order.succ (Ordinal.sup f) = Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Order.succ (Ordinal.sup f) ≤ Ordinal.lsub f ↔ ∃ i, f i = Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Order.succ (Ordinal.sup f) = Ordinal.lsub f ↔ ∃ i, f i = Ordinal.sup f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.sup f = Ordinal.lsub f ↔ ∀ (i : ι), f i < Ordinal.sup f
<VAR>ι : Type u_4<VAR>h : IsEmpty ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>Ordinal.lsub f = 0
<VAR>ι : Type u<VAR>h : Nonempty ι<VAR>f : ι → Ordinal.{max u v}<GOAL>0 < Ordinal.lsub f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.lsub f = 0 ↔ IsEmpty ι
<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>o : Ordinal.{max u_5 u_4}<GOAL>(Ordinal.lsub fun x => o) = Order.succ o
<VAR>ι : Type u_4<VAR>Unique ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>Ordinal.lsub f = Order.succ (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.lsub f ≤ Ordinal.lsub 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.lsub f = Ordinal.lsub g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>Ordinal.lsub f = max (Ordinal.lsub fun a => f (Sum.inl a)) (Ordinal.lsub fun b => f (Sum.inr b))
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.lsub f ∉ Set.range f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(Set.range f)ᶜ.Nonempty
<VAR>o : Ordinal.{u}<GOAL>Ordinal.lsub (Ordinal.typein fun x x_1 => x < x_1) = o
<VAR>o : Ordinal.{u}<VAR>ho : ∀ a < o, Order.succ a < o<GOAL>Ordinal.sup (Ordinal.typein fun x x_1 => x < x_1) = o
<VAR>o : Ordinal.{u}<GOAL>Ordinal.sup (Ordinal.typein fun x x_1 => x < x_1) = o
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>(o.bsup fun a ha => Order.succ (f a ha)) = o.blsub f
<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 → Ordinal.{max u v}<GOAL>Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = o.blsub 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.lsub (Ordinal.familyOfBFamily' r ho f) = Ordinal.lsub (Ordinal.familyOfBFamily' r' ho' f)
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Ordinal.lsub (o.familyOfBFamily f) = o.blsub f
<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f
<VAR>ι : Type u<VAR>r r' : ι → ι → Prop<VAR>IsWellOrder ι r<VAR>IsWellOrder ι r'<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').blsub (Ordinal.bfamilyOfFamily' r' f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(Ordinal.type WellOrderingRel).blsub (Ordinal.bfamilyOfFamily f) = Ordinal.lsub f
<VAR>o₁ o₂ : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}<VAR>ho : o₁ = o₂<GOAL>o₁.blsub f = o₂.blsub fun a h => f a ⋯
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a
<VAR>o : Ordinal.{u_4}<VAR>f : (b : Ordinal.{u_4}) → b < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_4 u_5}<GOAL>(∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a) → o.blsub f ≤ a
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<VAR>i : Ordinal.{u_4}<VAR>h : i < o<GOAL>f i h < o.blsub f
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f ≤ o.blsub f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.blsub f ≤ Order.succ (o.bsup f)
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f = o.blsub f ∨ Order.succ (o.bsup f) = o.blsub f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>Order.succ (o.bsup f) = o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, Order.succ a < o.blsub f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f = o.blsub f ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ⋯<GOAL>o.bsup f = o.blsub f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < Order.succ o → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj<GOAL>(Order.succ o).blsub f = Order.succ (f o ⋯)
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<GOAL>o.blsub f = 0 ↔ o = 0
<VAR>f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}<GOAL>Ordinal.blsub 0 f = 0
<VAR>o : Ordinal.{u_4}<VAR>ho : 0 < o<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<GOAL>0 < o.blsub f
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : (a : Ordinal.{u}) → a < Ordinal.type r → Ordinal.{max u v}<GOAL>(Ordinal.type r).blsub f = Ordinal.lsub fun a => f (Ordinal.typein r a) ⋯
<VAR>o : Ordinal.{u}<VAR>ho : o ≠ 0<VAR>a : Ordinal.{max u v}<GOAL>(o.blsub fun x x => a) = Order.succ a
<VAR>f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}<GOAL>Ordinal.blsub 1 f = Order.succ (f 0 ⋯)
<VAR>o : Ordinal.{u}<GOAL>(o.blsub fun x x_1 => x) = o
<VAR>o : Ordinal.{u}<GOAL>(∀ a < o, Order.succ a < o) → (o.bsup fun x x_1 => x) = o
<VAR>o : Ordinal.{u}<GOAL>((Order.succ o).bsup fun x x_1 => x) = o
<VAR>o : Ordinal.{u}<VAR>o' : Ordinal.{v}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}<VAR>g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}<VAR>h : o.brange f ⊆ o'.brange g<GOAL>o.blsub f ≤ o'.blsub g
<VAR>o : Ordinal.{u}<VAR>o' : Ordinal.{v}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}<VAR>g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}<VAR>h : {o_1 | ∃ i, ∃ (hi : i < o), f i hi = o_1} = {o | ∃ i, ∃ (hi : i < o'), g i hi = o}<GOAL>o.blsub f = o'.blsub g
<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<GOAL>(o'.bsup fun a ha => f (g a ha) ⋯) = o.bsup f
<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<GOAL>(o'.blsub fun a ha => f (g a ha) ⋯) = o.blsub f
<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u}<VAR>h : o.IsLimit<GOAL>(o.bsup fun x x_1 => f x) = f o
<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u}<VAR>h : o.IsLimit<GOAL>(o.blsub fun x x_1 => f x) = f o
<VAR>f : Ordinal.{u} → Ordinal.{max u v}<GOAL>Ordinal.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
<VAR>f : Ordinal.{u} → Ordinal.{max u v}<GOAL>Ordinal.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o
<VAR>f g : Ordinal.{u} → Ordinal.{u}<VAR>hf : Ordinal.IsNormal f<VAR>hg : Ordinal.IsNormal g<GOAL>f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)
<VAR>o₁ : Ordinal.{u_4}<VAR>o₂ : Ordinal.{u_5}<VAR>op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6}<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_5}<VAR>ha : a < o₁<VAR>hb : b < o₂<GOAL>op ha hb < o₁.blsub₂ o₂ fun {a} => op
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.mex f ∉ Set.range f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>H : ∀ b < a, ∃ i, f i = b<GOAL>a ≤ Ordinal.mex f
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>i : ι<GOAL>f i ≠ Ordinal.mex f
<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>a : Ordinal.{max u_5 u_4}<VAR>ha : ∀ (i : ι), f i ≠ a<GOAL>Ordinal.mex f ≤ a
<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>a : Ordinal.{max u_4 u_5}<VAR>ha : a < Ordinal.mex f<GOAL>∃ i, f i = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>Ordinal.mex f ≤ Ordinal.lsub f
<VAR>α β : Type u<VAR>f : α → Ordinal.{max u v}<VAR>g : β → Ordinal.{max u v}<VAR>h : Set.range f ⊆ Set.range g<GOAL>Ordinal.mex f ≤ Ordinal.mex g
<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<GOAL>Ordinal.mex f < (Order.succ #ι).ord
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<GOAL>o.bmex f ∉ o.brange f
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_4 u_5}<VAR>H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b<GOAL>a ≤ o.bmex f
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi ≠ o.bmex f
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_4 u_5}<VAR>ha : ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi ≠ a<GOAL>o.bmex f ≤ a
<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_5 u_4}<VAR>ha : a < o.bmex f<GOAL>∃ i, ∃ (hi : i < o), f i hi = a
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bmex f ≤ o.blsub f
<VAR>o o' : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>g : (a : Ordinal.{u}) → a < o' → Ordinal.{max u v}<VAR>h : o.brange f ⊆ o'.brange g<GOAL>o.bmex f ≤ o'.bmex g
<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>o.bmex f < (Order.succ o.card).ord
<VAR>α : Type u<VAR>f : α → Ordinal.{u}<GOAL>¬Function.Surjective f
<VAR>α : Type u<VAR>f : Ordinal.{u} → α<GOAL>¬Function.Injective f
<VAR>α : Type v<VAR>Small.{u, v} α<VAR>f : α → Ordinal.{u}<GOAL>¬Function.Surjective f
<VAR>α : Type v<VAR>Small.{u, v} α<VAR>f : Ordinal.{u} → α<GOAL>¬Function.Injective f
<GOAL>¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}
<VAR>S : Set Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>Ordinal.enumOrd S o = sInf (S ∩ Set.Ici (o.blsub fun a x => Ordinal.enumOrd S a))
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>a : Ordinal.{u}<GOAL>(S ∩ Set.Ici a).Nonempty
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>Ordinal.enumOrd S o ∈ S ∩ Set.Ici (o.blsub fun c x => Ordinal.enumOrd S c)
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>Ordinal.enumOrd S o ∈ S
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>(o.blsub fun c x => Ordinal.enumOrd S c) ≤ Ordinal.enumOrd S o
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<GOAL>StrictMono (Ordinal.enumOrd S)
<VAR>S : Set Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>Ordinal.enumOrd S o = sInf (S ∩ {b | ∀ c < o, Ordinal.enumOrd S c < b})
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>{x | x ∈ S ∧ ∀ c < o, Ordinal.enumOrd S c < x}.Nonempty
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<GOAL>Ordinal.enumOrd (Set.range f) = f
<VAR>S : Set Ordinal.{u}<GOAL>Ordinal.enumOrd S 0 = sInf S
<VAR>S : Set Ordinal.{u}<VAR>a b : Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>ha : a ∈ S<VAR>hb : Ordinal.enumOrd S b < a<GOAL>Ordinal.enumOrd S (Order.succ b) ≤ a
<VAR>S T : Set Ordinal.{u_1}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>hST : S ⊆ T<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.enumOrd T a ≤ Ordinal.enumOrd S a
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<VAR>s : Ordinal.{u}<GOAL>s ∈ S → ∃ a, Ordinal.enumOrd S a = s
<VAR>S : Set Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<GOAL>Set.range (Ordinal.enumOrd S) = S
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hS : Set.Unbounded (fun x x_1 => x < x_1) S<GOAL>StrictMono f ∧ Set.range f = S ↔ f = Ordinal.enumOrd S
<VAR>m : ℕ<GOAL>1 + ↑m = ↑(Order.succ m)
<VAR>m : ℕ<VAR>m.AtLeastTwo<GOAL>1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)
<VAR>n : ℕ<GOAL>↑n = 0 ↔ n = 0
<VAR>n : ℕ<GOAL>↑n ≠ 0 ↔ n ≠ 0
<VAR>n : ℕ<GOAL>0 < ↑n ↔ 0 < n
<VAR>n : ℕ<GOAL>Ordinal.lift.{u, v} ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Ordinal.lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n
<VAR>o : Ordinal.{u_1}<GOAL>ω ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o
<VAR>o : Ordinal.{u_1}<VAR>h : o.IsLimit<VAR>n : ℕ<GOAL>↑n < o
<VAR>o : Ordinal.{u_1}<VAR>h : o.IsLimit<GOAL>ω ≤ o
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * Order.succ c' = a * Order.succ c' + b<GOAL>(a + b) * c = a * c
<VAR>a b : Ordinal.{u_1}<VAR>c : Ordinal.{u_1}<VAR>ba : b + a = a<GOAL>(a + b) * Order.succ c = a * Order.succ c + b
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<GOAL>(a + b) * c = a * c
<VAR>a b c : Ordinal.{u_1}<VAR>hb : 0 < b<VAR>h : ∀ d < b, a + d < c<GOAL>a + b ≤ c
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : Ordinal.IsNormal f<GOAL>Ordinal.sup (f ∘ Nat.cast) = f ω
<VAR>o : Ordinal.{u_1}<GOAL>(Ordinal.sup fun n => o + ↑n) = o + ω
<VAR>o : Ordinal.{u_1}<GOAL>(Ordinal.sup fun n => o * ↑n) = o * ω
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>h : Acc r a<GOAL>h.rank = Ordinal.sup fun b => Order.succ ⋯.rank
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>hb : Acc r b<VAR>h : r a b<GOAL>⋯.rank < hb.rank
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>hwf : WellFounded r<GOAL>hwf.rank a = Ordinal.sup fun b => Order.succ (hwf.rank ↑b)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>hwf : WellFounded r<VAR>h : r a b<GOAL>hwf.rank a < hwf.rank b
<VAR>α : Type u<VAR>Preorder α<VAR>WellFoundedLT α<GOAL>StrictMono ⋯.rank
<VAR>α : Type u<VAR>Preorder α<VAR>WellFoundedGT α<GOAL>StrictAnti ⋯.rank
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>AddMonoidWithOne R<GOAL>(SimpleGraph.degMatrix R G).IsSymm
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>AddGroupWithOne R<GOAL>(SimpleGraph.lapMatrix R G).IsSymm
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>NonAssocSemiring R<VAR>v : V<VAR>vec : V → R<GOAL>(SimpleGraph.degMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>NonAssocRing R<VAR>v : V<VAR>vec : V → R<GOAL>(SimpleGraph.lapMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Ring R<GOAL>(SimpleGraph.lapMatrix R G *ᵥ fun x => 1) = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>CommRing R<VAR>x : V → R<GOAL>x ⬝ᵥ SimpleGraph.degMatrix R G *ᵥ x = ∑ i : V, ↑(G.degree i) * x i * x i
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>AddCommMonoidWithOne R<VAR>i : V<GOAL>↑(G.degree i) = ∑ j : V, if G.Adj i j then 1 else 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Field R<VAR>CharZero R<VAR>x : V → R<GOAL>(((Matrix.toLinearMap₂' R) (SimpleGraph.lapMatrix R G)) x) x = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>LinearOrderedField R<VAR>StarRing R<VAR>TrivialStar R<GOAL>(SimpleGraph.lapMatrix R G).PosSemidef
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>LinearOrderedField R<VAR>x : V → R<GOAL>(((Matrix.toLinearMap₂' R) (SimpleGraph.lapMatrix R G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(((Matrix.toLinearMap₂' ℝ) (SimpleGraph.lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>DecidableEq G.ConnectedComponent<VAR>c : G.ConnectedComponent<GOAL>(fun i => if G.connectedComponentMk i = c then 1 else 0) ∈ LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G))
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>DecidableEq G.ConnectedComponent<GOAL>LinearIndependent ℝ G.lapMatrix_ker_basis_aux
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>DecidableEq G.ConnectedComponent<GOAL>⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<GOAL>Fintype.card G.ConnectedComponent = FiniteDimensional.finrank ℝ ↥(LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulDysonETransform e x).1 = x.1 ∪ e • x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addDysonETransform e x).2 = x.2 ∩ (-e +ᵥ x.1)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addDysonETransform e x).1 = x.1 ∪ (e +ᵥ x.2)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulDysonETransform e x).2 = x.2 ∩ e⁻¹ • x.1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulDysonETransform e x).1 * (Finset.mulDysonETransform e x).2 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addDysonETransform e x).1 + (Finset.addDysonETransform e x).2 ⊆ x.1 + x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulDysonETransform e x).1.card + (Finset.mulDysonETransform e x).2.card = x.1.card + x.2.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addDysonETransform e x).1.card + (Finset.addDysonETransform e x).2.card = x.1.card + x.2.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.addDysonETransform e (Finset.addDysonETransform e x) = Finset.addDysonETransform e x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.mulDysonETransform e (Finset.mulDysonETransform e x) = Finset.mulDysonETransform e x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>e • (Finset.mulDysonETransform e x).2 ⊆ (Finset.mulDysonETransform e x).1